fix: catch 'none' exception in Real.sqrt positivity extension (#8014)

This example currently fails
```lean
example (x : ℝ) : 0 ≤ Real.sqrt x := by positivity
```
due to the exception being thrown here:
https://github.com/leanprover-community/mathlib4/blob/b56efa53d7479fda9740f364170cbaef34699dee/Mathlib/Tactic/Positivity/Core.lean#L304

It should succeed, because the junk value used for `sqrt` of a negative number is non-negative.

This PR fixes it by catching the exception, a pattern used elsewhere:
https://github.com/leanprover-community/mathlib4/blob/b56efa53d7479fda9740f364170cbaef34699dee/Mathlib/Tactic/Positivity/Core.lean#L325

Mathlib/Data/Real/Sqrt.lean

@@ -380,7 +380,7 @@ def evalSqrt : PositivityExt where eval {_ _} _zα _pα e := do
   let (.app _ (a : Q(Real))) ← whnfR e | throwError "not Real.sqrt"
   let zα' ← synthInstanceQ (q(Zero Real) : Q(Type))
   let pα' ← synthInstanceQ (q(PartialOrder Real) : Q(Type))
-  let ra ← core zα' pα' a
+  let ra ← catchNone <| core zα' pα' a
   assertInstancesCommute
   match ra with
   | .positive pa => pure (.positive (q(Real.sqrt_pos_of_pos $pa) : Expr))

test/positivity.lean

@@ -216,6 +216,7 @@ example {a : ℤ} (ha : 1 < a) : 0 < |(3:ℤ) + a| := by positivity
 
 example : 0 < NNReal.sqrt 5 := by positivity
 example : 0 ≤ Real.sqrt (-5) := by positivity
+example (x : ℝ) : 0 ≤ Real.sqrt x := by positivity
 example : 0 < Real.sqrt 5 := by positivity
 
 example {a : ℝ} (_ha : 0 ≤ a) : 0 ≤ Real.sqrt a := by positivity