perf(Data.Real.Sqrt): make Real.sqrt irreducible (#25856)

We try to see what happens if we make Real.sqrt irreducible.

There are cases where this makes unification very significantly faster, compare [#mathlib4 > Coercion triggers timeout @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Coercion.20triggers.20timeout/near/517177117).

(Migrated manually from #24752)

Author: MichaelStollBayreuth

Mathlib/Data/Real/Sqrt.lean

@@ -64,7 +64,6 @@ lemma sqrt_le_iff_le_sq : sqrt x ≤ y ↔ x ≤ y ^ 2 := sqrt.to_galoisConnecti
 
 lemma le_sqrt_iff_sq_le : x ≤ sqrt y ↔ x ^ 2 ≤ y := (sqrt.symm.to_galoisConnection _ _).symm
 
-
 @[simp] lemma sqrt_eq_zero : sqrt x = 0 ↔ x = 0 := by simp [sqrt_eq_iff_eq_sq]
 
 @[simp] lemma sqrt_eq_one : sqrt x = 1 ↔ x = 1 := by simp [sqrt_eq_iff_eq_sq]
@@ -107,7 +106,7 @@ namespace Real
 /-- The square root of a real number. This returns 0 for negative inputs.
 
 This has notation `√x`. Note that `√x⁻¹` is parsed as `√(x⁻¹)`. -/
-noncomputable def sqrt (x : ℝ) : ℝ :=
+@[irreducible] noncomputable def sqrt (x : ℝ) : ℝ :=
   NNReal.sqrt (Real.toNNReal x)
 
 -- TODO: replace this with a typeclass
@@ -121,12 +120,15 @@ theorem coe_sqrt {x : ℝ≥0} : (NNReal.sqrt x : ℝ) = √(x : ℝ) := by
   rw [Real.sqrt, Real.toNNReal_coe]
 
 @[continuity]
-theorem continuous_sqrt : Continuous (√· : ℝ → ℝ) :=
-  NNReal.continuous_coe.comp <| NNReal.continuous_sqrt.comp continuous_real_toNNReal
+theorem continuous_sqrt : Continuous (√· : ℝ → ℝ) := by
+  unfold sqrt
+  exact NNReal.continuous_coe.comp <| NNReal.continuous_sqrt.comp continuous_real_toNNReal
 
 theorem sqrt_eq_zero_of_nonpos (h : x ≤ 0) : sqrt x = 0 := by simp [sqrt, Real.toNNReal_eq_zero.2 h]
 
-@[simp] theorem sqrt_nonneg (x : ℝ) : 0 ≤ √x := NNReal.coe_nonneg _
+@[simp] theorem sqrt_nonneg (x : ℝ) : 0 ≤ √x := by
+  unfold sqrt
+  exact NNReal.coe_nonneg _
 
 @[simp]
 theorem mul_self_sqrt (h : 0 ≤ x) : √x * √x = x := by