diff --git a/Mathlib/Algebra/Star/Order.lean b/Mathlib/Algebra/Star/Order.lean
index 1901866d9a169..56b9e87725a42 100644
--- a/Mathlib/Algebra/Star/Order.lean
+++ b/Mathlib/Algebra/Star/Order.lean
@@ -20,7 +20,7 @@ literature (see the seminal paper [*The positive cone in Banach algebras*][kelle
 In order to accommodate `NonUnitalSemiring R`, we actually don't characterize nonnegativity, but
 rather the entire `≤` relation with `StarOrderedRing.le_iff`. However, notice that when `R` is a
 `NonUnitalRing`, these are equivalent (see `StarOrderedRing.nonneg_iff` and
-`StarOrderedRing.ofNonnegIff`).
+`StarOrderedRing.of_nonneg_iff`).
 
 It is important to note that while a `StarOrderedRing` is an `OrderedAddCommMonoid` it is often
 *not* an `OrderedSemiring`.
@@ -45,7 +45,7 @@ variable {R : Type u}
 constitute precisely the `AddSubmonoid` generated by elements of the form `star s * s`.
 
 If you are working with a `NonUnitalRing` and not a `NonUnitalSemiring`, it may be more
-convenient to declare instances using `StarOrderedRing.ofNonnegIff'`.
+convenient to declare instances using `StarOrderedRing.of_nonneg_iff`.
 
 Porting note: dropped an unneeded assumption
 `add_le_add_left : ∀ {x y}, x ≤ y → ∀ z, z + x ≤ z + y` -/
@@ -89,9 +89,9 @@ This is provided for convenience because it holds in some common scenarios (e.g.
 and obviates the hassle of `AddSubmonoid.closure_induction` when creating those instances.
 
 If you are working with a `NonUnitalRing` and not a `NonUnitalSemiring`, see
-`StarOrderedRing.ofNonnegIff` for a more convenient version.
+`StarOrderedRing.of_nonneg_iff` for a more convenient version.
  -/
-lemma ofLEIff [NonUnitalSemiring R] [PartialOrder R] [StarRing R]
+lemma of_le_iff [NonUnitalSemiring R] [PartialOrder R] [StarRing R]
     (h_le_iff : ∀ x y : R, x ≤ y ↔ ∃ s, y = x + star s * s) : StarOrderedRing R where
   le_iff x y := by
     refine' ⟨fun h => _, _⟩
@@ -105,19 +105,19 @@ lemma ofLEIff [NonUnitalSemiring R] [PartialOrder R] [StarRing R]
       · rintro a b ha hb x y rfl
         rw [← add_assoc]
         exact (ha _ _ rfl).trans (hb _ _ rfl)
-#align star_ordered_ring.of_le_iff StarOrderedRing.ofLEIffₓ
+#align star_ordered_ring.of_le_iff StarOrderedRing.of_le_iffₓ
 
 /-- When `R` is a non-unital ring, to construct a `StarOrderedRing` instance it suffices to
 show that the nonnegative elements are precisely those elements in the `AddSubmonoid` generated
 by `star s * s` for `s : R`. -/
-lemma ofNonnegIff [NonUnitalRing R] [PartialOrder R] [StarRing R]
+lemma of_nonneg_iff [NonUnitalRing R] [PartialOrder R] [StarRing R]
     (h_add : ∀ {x y : R}, x ≤ y → ∀ z, z + x ≤ z + y)
     (h_nonneg_iff : ∀ x : R, 0 ≤ x ↔ x ∈ AddSubmonoid.closure (Set.range fun s : R => star s * s)) :
     StarOrderedRing R where
   le_iff x y := by
     haveI : CovariantClass R R (· + ·) (· ≤ ·) := ⟨fun _ _ _ h => h_add h _⟩
     simpa only [← sub_eq_iff_eq_add', sub_nonneg, exists_eq_right'] using h_nonneg_iff (y - x)
-#align star_ordered_ring.of_nonneg_iff StarOrderedRing.ofNonnegIff
+#align star_ordered_ring.of_nonneg_iff StarOrderedRing.of_nonneg_iff
 
 /-- When `R` is a non-unital ring, to construct a `StarOrderedRing` instance it suffices to
 show that the nonnegative elements are precisely those elements of the form `star s * s`
@@ -126,13 +126,13 @@ for `s : R`.
 This is provided for convenience because it holds in many common scenarios (e.g.,`ℝ`, `ℂ`, or
 any C⋆-algebra), and obviates the hassle of `AddSubmonoid.closure_induction` when creating those
 instances. -/
-lemma ofNonnegIff' [NonUnitalRing R] [PartialOrder R] [StarRing R]
+lemma of_nonneg_iff' [NonUnitalRing R] [PartialOrder R] [StarRing R]
     (h_add : ∀ {x y : R}, x ≤ y → ∀ z, z + x ≤ z + y)
     (h_nonneg_iff : ∀ x : R, 0 ≤ x ↔ ∃ s, x = star s * s) : StarOrderedRing R :=
-  ofLEIff <| by
+  of_le_iff <| by
     haveI : CovariantClass R R (· + ·) (· ≤ ·) := ⟨fun _ _ _ h => h_add h _⟩
     simpa [sub_eq_iff_eq_add', sub_nonneg] using fun x y => h_nonneg_iff (y - x)
-#align star_ordered_ring.of_nonneg_iff' StarOrderedRing.ofNonnegIff'
+#align star_ordered_ring.of_nonneg_iff' StarOrderedRing.of_nonneg_iff'
 
 theorem nonneg_iff [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {x : R} :
     0 ≤ x ↔ x ∈ AddSubmonoid.closure (Set.range fun s : R => star s * s) := by
diff --git a/Mathlib/Analysis/RCLike/Basic.lean b/Mathlib/Analysis/RCLike/Basic.lean
index 513ad19293768..2a036ccb5e57c 100644
--- a/Mathlib/Analysis/RCLike/Basic.lean
+++ b/Mathlib/Analysis/RCLike/Basic.lean
@@ -881,7 +881,7 @@ lemma neg_iff_exists_ofReal : z < 0 ↔ ∃ x < (0 : ℝ), x = z := by
 
 Note this is only an instance with `open scoped ComplexOrder`. -/
 lemma toStarOrderedRing : StarOrderedRing K :=
-  StarOrderedRing.ofNonnegIff'
+  StarOrderedRing.of_nonneg_iff'
     (h_add := fun {x y} hxy z => by
       rw [RCLike.le_iff_re_im] at *
       simpa [map_add, add_le_add_iff_left, add_right_inj] using hxy)
diff --git a/Mathlib/Data/Real/Sqrt.lean b/Mathlib/Data/Real/Sqrt.lean
index e45a5740cbb7a..3f1e9bd6be082 100644
--- a/Mathlib/Data/Real/Sqrt.lean
+++ b/Mathlib/Data/Real/Sqrt.lean
@@ -463,7 +463,7 @@ want `StarOrderedRing ℝ` to be available globally, so we include this instance
 In addition, providing this instance here makes it available earlier in the import
 hierarchy; otherwise in order to access it we would need to import `Analysis.RCLike.Basic` -/
 instance : StarOrderedRing ℝ :=
-  StarOrderedRing.ofNonnegIff' add_le_add_left fun r => by
+  StarOrderedRing.of_nonneg_iff' add_le_add_left fun r => by
     refine ⟨fun hr => ⟨√r, (mul_self_sqrt hr).symm⟩, ?_⟩
     rintro ⟨s, rfl⟩
     exact mul_self_nonneg s
@@ -471,7 +471,7 @@ instance : StarOrderedRing ℝ :=
 end Real
 
 instance NNReal.instStarOrderedRing : StarOrderedRing ℝ≥0 := by
-  refine .ofLEIff fun x y ↦ ⟨fun h ↦ ?_, ?_⟩
+  refine .of_le_iff fun x y ↦ ⟨fun h ↦ ?_, ?_⟩
   · obtain ⟨d, rfl⟩ := exists_add_of_le h
     refine ⟨sqrt d, ?_⟩
     simp only [star_trivial, mul_self_sqrt]