move lemmas above variables

Author: dupuisf

Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/ConjSqrt.lean

@@ -40,6 +40,19 @@ noncomputable def conjSqrt (c : A) : A →L[ℝ] A where
 
 lemma conjSqrt_apply {c a : A} : conjSqrt c a = sqrt c * a * sqrt c := rfl
 
+lemma conjSqrt_of_not_nonneg {c a : A} (hc : ¬0 ≤ c) : conjSqrt c a = 0 := by
+  simp [conjSqrt_apply, sqrt_of_not_nonneg hc]
+
+lemma conjSqrt_monotone {c : A} : Monotone (conjSqrt c) := by
+  intro a b hab
+  by_cases hc : 0 ≤ c
+  · exact IsSelfAdjoint.conjugate_le_conjugate hab (by cfc_tac)
+  · simp [conjSqrt_of_not_nonneg hc]
+
+@[gcongr]
+lemma conjSqrt_le_conjSqrt {c a b : A} (h : a ≤ b) : conjSqrt c a ≤ conjSqrt c b :=
+  conjSqrt_monotone h
+
 variable [IsSemitopologicalRing A] [T2Space A]
 
 @[grind =]
@@ -80,22 +93,6 @@ lemma conjSqrt_ringInverse_self (c : A) (hc : IsStrictlyPositive c := by cfc_tac
     conjSqrt c⁻¹ʳ c = 1 := by
   grind [conjSqrt_one c]
 
-omit [IsSemitopologicalRing A] [T2Space A] in
-lemma conjSqrt_of_not_nonneg {c a : A} (hc : ¬0 ≤ c) : conjSqrt c a = 0 := by
-  simp [conjSqrt_apply, sqrt_of_not_nonneg hc]
-
-omit [IsSemitopologicalRing A] [T2Space A] in
-lemma conjSqrt_monotone {c : A} : Monotone (conjSqrt c) := by
-  intro a b hab
-  by_cases hc : 0 ≤ c
-  · exact IsSelfAdjoint.conjugate_le_conjugate hab (by cfc_tac)
-  · simp [conjSqrt_of_not_nonneg hc]
-
-omit [IsSemitopologicalRing A] [T2Space A] in
-@[gcongr]
-lemma conjSqrt_le_conjSqrt {c a b : A} (h : a ≤ b) : conjSqrt c a ≤ conjSqrt c b :=
-  conjSqrt_monotone h
-
 end ConjSqrt
 
 end CFC