diff --git a/Mathlib/Algebra/AddConstMap/Basic.lean b/Mathlib/Algebra/AddConstMap/Basic.lean
index 25685a81e92e9..f71b10f9c82ba 100644
--- a/Mathlib/Algebra/AddConstMap/Basic.lean
+++ b/Mathlib/Algebra/AddConstMap/Basic.lean
@@ -87,7 +87,7 @@ theorem map_add_one [AddMonoidWithOne G] [Add H] [AddConstMapClass F G H 1 b]
 @[scoped simp]
 theorem map_add_ofNat' [AddMonoidWithOne G] [AddMonoid H] [AddConstMapClass F G H 1 b]
     (f : F) (x : G) (n : ℕ) [n.AtLeastTwo] :
-    f (x + no_index (OfNat.ofNat n)) = f x + (OfNat.ofNat n : ℕ) • b :=
+    f (x + ofNat(n)) = f x + (OfNat.ofNat n : ℕ) • b :=
   map_add_nat' f x n
 
 theorem map_add_nat [AddMonoidWithOne G] [AddMonoidWithOne H] [AddConstMapClass F G H 1 1]
@@ -181,7 +181,7 @@ theorem map_sub_nat' [AddGroupWithOne G] [AddGroup H] [AddConstMapClass F G H 1
 @[scoped simp]
 theorem map_sub_ofNat' [AddGroupWithOne G] [AddGroup H] [AddConstMapClass F G H 1 b]
     (f : F) (x : G) (n : ℕ) [n.AtLeastTwo] :
-    f (x - no_index (OfNat.ofNat n)) = f x - OfNat.ofNat n • b :=
+    f (x - ofNat(n)) = f x - OfNat.ofNat n • b :=
   map_sub_nat' f x n
 
 @[scoped simp]
diff --git a/Mathlib/Algebra/CharZero/Defs.lean b/Mathlib/Algebra/CharZero/Defs.lean
index c82356e6fa6e7..f536a1bb1d7a4 100644
--- a/Mathlib/Algebra/CharZero/Defs.lean
+++ b/Mathlib/Algebra/CharZero/Defs.lean
@@ -89,20 +89,20 @@ namespace OfNat
 
 variable [AddMonoidWithOne R] [CharZero R]
 
-@[simp] lemma ofNat_ne_zero (n : ℕ) [n.AtLeastTwo] : (no_index (ofNat n) : R) ≠ 0 :=
+@[simp] lemma ofNat_ne_zero (n : ℕ) [n.AtLeastTwo] : (ofNat(n) : R) ≠ 0 :=
   Nat.cast_ne_zero.2 (NeZero.ne n)
 
-@[simp] lemma zero_ne_ofNat (n : ℕ) [n.AtLeastTwo] : 0 ≠ (no_index (ofNat n) : R) :=
+@[simp] lemma zero_ne_ofNat (n : ℕ) [n.AtLeastTwo] : 0 ≠ (ofNat(n) : R) :=
   (ofNat_ne_zero n).symm
 
-@[simp] lemma ofNat_ne_one (n : ℕ) [n.AtLeastTwo] : (no_index (ofNat n) : R) ≠ 1 :=
+@[simp] lemma ofNat_ne_one (n : ℕ) [n.AtLeastTwo] : (ofNat(n) : R) ≠ 1 :=
   Nat.cast_ne_one.2 (Nat.AtLeastTwo.ne_one)
 
-@[simp] lemma one_ne_ofNat (n : ℕ) [n.AtLeastTwo] : (1 : R) ≠ no_index (ofNat n) :=
+@[simp] lemma one_ne_ofNat (n : ℕ) [n.AtLeastTwo] : (1 : R) ≠ ofNat(n) :=
   (ofNat_ne_one n).symm
 
 @[simp] lemma ofNat_eq_ofNat {m n : ℕ} [m.AtLeastTwo] [n.AtLeastTwo] :
-    (no_index (ofNat m) : R) = no_index (ofNat n) ↔ (ofNat m : ℕ) = ofNat n :=
+    (ofNat(m) : R) = ofNat(n) ↔ (ofNat m : ℕ) = ofNat n :=
   Nat.cast_inj
 
 end OfNat
diff --git a/Mathlib/Algebra/DirectSum/Internal.lean b/Mathlib/Algebra/DirectSum/Internal.lean
index a75722faa88dc..fb7946b75ad16 100644
--- a/Mathlib/Algebra/DirectSum/Internal.lean
+++ b/Mathlib/Algebra/DirectSum/Internal.lean
@@ -337,7 +337,7 @@ instance instSemiring : Semiring (A 0) := (subsemiring A).toSemiring
 @[simp, norm_cast] theorem coe_natCast (n : ℕ) : (n : A 0) = (n : R) := rfl
 
 @[simp, norm_cast] theorem coe_ofNat (n : ℕ) [n.AtLeastTwo] :
-    (no_index (OfNat.ofNat n) : A 0) = (OfNat.ofNat n : R) := rfl
+    (ofNat(n) : A 0) = (OfNat.ofNat n : R) := rfl
 
 end Semiring
 
diff --git a/Mathlib/Algebra/Module/LinearMap/End.lean b/Mathlib/Algebra/Module/LinearMap/End.lean
index 5f1a7fe6fd3d0..d7cac2488f1b0 100644
--- a/Mathlib/Algebra/Module/LinearMap/End.lean
+++ b/Mathlib/Algebra/Module/LinearMap/End.lean
@@ -89,7 +89,7 @@ theorem _root_.Module.End.natCast_apply (n : ℕ) (m : M) : (↑n : Module.End R
 
 @[simp]
 theorem _root_.Module.End.ofNat_apply (n : ℕ) [n.AtLeastTwo] (m : M) :
-    (no_index (OfNat.ofNat n) : Module.End R M) m = OfNat.ofNat n • m := rfl
+    (ofNat(n) : Module.End R M) m = OfNat.ofNat n • m := rfl
 
 instance _root_.Module.End.ring : Ring (Module.End R N₁) :=
   { Module.End.semiring, LinearMap.addCommGroup with
diff --git a/Mathlib/Algebra/Order/SuccPred/WithBot.lean b/Mathlib/Algebra/Order/SuccPred/WithBot.lean
index df9812d972bf8..08d2abbd2dca9 100644
--- a/Mathlib/Algebra/Order/SuccPred/WithBot.lean
+++ b/Mathlib/Algebra/Order/SuccPred/WithBot.lean
@@ -24,6 +24,6 @@ lemma succ_one : succ (1 : WithBot α) = 2 := by simpa [one_add_one_eq_two] usin
 
 @[simp]
 lemma succ_ofNat (n : ℕ) [n.AtLeastTwo] :
-    succ (no_index (OfNat.ofNat n) : WithBot α) = OfNat.ofNat n + 1 := succ_natCast n
+    succ (ofNat(n) : WithBot α) = OfNat.ofNat n + 1 := succ_natCast n
 
 end WithBot
diff --git a/Mathlib/Algebra/Polynomial/Derivative.lean b/Mathlib/Algebra/Polynomial/Derivative.lean
index c23fdfc0c1e98..e0154c45d7370 100644
--- a/Mathlib/Algebra/Polynomial/Derivative.lean
+++ b/Mathlib/Algebra/Polynomial/Derivative.lean
@@ -195,7 +195,7 @@ alias derivative_nat_cast := derivative_natCast
 
 @[simp]
 theorem derivative_ofNat (n : ℕ) [n.AtLeastTwo] :
-    derivative (no_index (OfNat.ofNat n) : R[X]) = 0 :=
+    derivative (ofNat(n) : R[X]) = 0 :=
   derivative_natCast
 
 theorem iterate_derivative_eq_zero {p : R[X]} {x : ℕ} (hx : p.natDegree < x) :
diff --git a/Mathlib/Algebra/Polynomial/Eval/Defs.lean b/Mathlib/Algebra/Polynomial/Eval/Defs.lean
index af51045eb7816..5b47a0237e819 100644
--- a/Mathlib/Algebra/Polynomial/Eval/Defs.lean
+++ b/Mathlib/Algebra/Polynomial/Eval/Defs.lean
@@ -102,10 +102,9 @@ theorem eval₂_natCast (n : ℕ) : (n : R[X]).eval₂ f x = n := by
 @[deprecated (since := "2024-04-17")]
 alias eval₂_nat_cast := eval₂_natCast
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 lemma eval₂_ofNat {S : Type*} [Semiring S] (n : ℕ) [n.AtLeastTwo] (f : R →+* S) (a : S) :
-    (no_index (OfNat.ofNat n : R[X])).eval₂ f a = OfNat.ofNat n := by
+    (ofNat(n) : R[X]).eval₂ f a = OfNat.ofNat n := by
   simp [OfNat.ofNat]
 
 variable [Semiring T]
@@ -263,10 +262,9 @@ theorem eval₂_at_natCast {S : Type*} [Semiring S] (f : R →+* S) (n : ℕ) :
 @[deprecated (since := "2024-04-17")]
 alias eval₂_at_nat_cast := eval₂_at_natCast
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem eval₂_at_ofNat {S : Type*} [Semiring S] (f : R →+* S) (n : ℕ) [n.AtLeastTwo] :
-    p.eval₂ f (no_index (OfNat.ofNat n)) = f (p.eval (OfNat.ofNat n)) := by
+    p.eval₂ f ofNat(n) = f (p.eval (OfNat.ofNat n)) := by
   simp [OfNat.ofNat]
 
 @[simp]
@@ -279,10 +277,9 @@ theorem eval_natCast {n : ℕ} : (n : R[X]).eval x = n := by simp only [← C_eq
 @[deprecated (since := "2024-04-17")]
 alias eval_nat_cast := eval_natCast
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 lemma eval_ofNat (n : ℕ) [n.AtLeastTwo] (a : R) :
-    (no_index (OfNat.ofNat n : R[X])).eval a = OfNat.ofNat n := by
+    (ofNat(n) : R[X]).eval a = OfNat.ofNat n := by
   simp only [OfNat.ofNat, eval_natCast]
 
 @[simp]
@@ -398,7 +395,7 @@ theorem natCast_comp {n : ℕ} : (n : R[X]).comp p = n := by rw [← C_eq_natCas
 alias nat_cast_comp := natCast_comp
 
 @[simp]
-theorem ofNat_comp (n : ℕ) [n.AtLeastTwo] : (no_index (OfNat.ofNat n) : R[X]).comp p = n :=
+theorem ofNat_comp (n : ℕ) [n.AtLeastTwo] : (ofNat(n) : R[X]).comp p = n :=
   natCast_comp
 
 @[simp]
@@ -550,10 +547,9 @@ protected theorem map_natCast (n : ℕ) : (n : R[X]).map f = n :=
 @[deprecated (since := "2024-04-17")]
 alias map_nat_cast := map_natCast
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 protected theorem map_ofNat (n : ℕ) [n.AtLeastTwo] :
-    (no_index (OfNat.ofNat n) : R[X]).map f = OfNat.ofNat n :=
+    (ofNat(n) : R[X]).map f = OfNat.ofNat n :=
   show (n : R[X]).map f = n by rw [Polynomial.map_natCast]
 
 --TODO rename to `map_dvd_map`
diff --git a/Mathlib/Algebra/Ring/Subsemiring/Defs.lean b/Mathlib/Algebra/Ring/Subsemiring/Defs.lean
index 3fe12b9558589..912ae88a54629 100644
--- a/Mathlib/Algebra/Ring/Subsemiring/Defs.lean
+++ b/Mathlib/Algebra/Ring/Subsemiring/Defs.lean
@@ -32,7 +32,7 @@ theorem natCast_mem [AddSubmonoidWithOneClass S R] (n : ℕ) : (n : R) ∈ s :=
 
 @[aesop safe apply (rule_sets := [SetLike])]
 lemma ofNat_mem [AddSubmonoidWithOneClass S R] (s : S) (n : ℕ) [n.AtLeastTwo] :
-    no_index (OfNat.ofNat n) ∈ s := by
+    ofNat(n) ∈ s := by
   rw [← Nat.cast_ofNat]; exact natCast_mem s n
 
 instance (priority := 74) AddSubmonoidWithOneClass.toAddMonoidWithOne
diff --git a/Mathlib/Algebra/Star/Basic.lean b/Mathlib/Algebra/Star/Basic.lean
index 04f2f59e38df2..929ae83b99d4a 100644
--- a/Mathlib/Algebra/Star/Basic.lean
+++ b/Mathlib/Algebra/Star/Basic.lean
@@ -289,7 +289,7 @@ theorem star_natCast [NonAssocSemiring R] [StarRing R] (n : ℕ) : star (n : R)
 
 @[simp]
 theorem star_ofNat [NonAssocSemiring R] [StarRing R] (n : ℕ) [n.AtLeastTwo] :
-    star (no_index (OfNat.ofNat n) : R) = OfNat.ofNat n :=
+    star (ofNat(n) : R) = OfNat.ofNat n :=
   star_natCast _
 
 section
diff --git a/Mathlib/Analysis/Complex/Basic.lean b/Mathlib/Analysis/Complex/Basic.lean
index 05dc52915295f..73c4f7ae5cdfa 100644
--- a/Mathlib/Analysis/Complex/Basic.lean
+++ b/Mathlib/Analysis/Complex/Basic.lean
@@ -154,10 +154,10 @@ theorem comap_abs_nhds_zero : comap abs (𝓝 0) = 𝓝 0 :=
 @[simp 1100, norm_cast] lemma nnnorm_ratCast (q : ℚ) : ‖(q : ℂ)‖₊ = ‖(q : ℝ)‖₊ := nnnorm_real q
 
 @[simp 1100] lemma norm_ofNat (n : ℕ) [n.AtLeastTwo] :
-    ‖(no_index (OfNat.ofNat n) : ℂ)‖ = OfNat.ofNat n := norm_natCast n
+    ‖(ofNat(n) : ℂ)‖ = OfNat.ofNat n := norm_natCast n
 
 @[simp 1100] lemma nnnorm_ofNat (n : ℕ) [n.AtLeastTwo] :
-    ‖(no_index (OfNat.ofNat n) : ℂ)‖₊ = OfNat.ofNat n := nnnorm_natCast n
+    ‖(ofNat(n) : ℂ)‖₊ = OfNat.ofNat n := nnnorm_natCast n
 
 @[deprecated (since := "2024-08-25")] alias norm_nat := norm_natCast
 @[deprecated (since := "2024-08-25")] alias norm_int := norm_intCast
@@ -693,7 +693,7 @@ lemma natCast_mem_slitPlane {n : ℕ} : ↑n ∈ slitPlane ↔ n ≠ 0 := by
 alias nat_cast_mem_slitPlane := natCast_mem_slitPlane
 
 @[simp]
-lemma ofNat_mem_slitPlane (n : ℕ) [n.AtLeastTwo] : no_index (OfNat.ofNat n) ∈ slitPlane :=
+lemma ofNat_mem_slitPlane (n : ℕ) [n.AtLeastTwo] : ofNat(n) ∈ slitPlane :=
   natCast_mem_slitPlane.2 (NeZero.ne n)
 
 lemma mem_slitPlane_iff_not_le_zero {z : ℂ} : z ∈ slitPlane ↔ ¬z ≤ 0 :=
diff --git a/Mathlib/Analysis/Normed/Group/Basic.lean b/Mathlib/Analysis/Normed/Group/Basic.lean
index fc2858dbb2006..493bd417df034 100644
--- a/Mathlib/Analysis/Normed/Group/Basic.lean
+++ b/Mathlib/Analysis/Normed/Group/Basic.lean
@@ -1240,10 +1240,10 @@ theorem le_norm_self (r : ℝ) : r ≤ ‖r‖ :=
 @[deprecated (since := "2024-04-05")] alias nnnorm_coe_nat := nnnorm_natCast
 
 @[simp 1100] lemma norm_ofNat (n : ℕ) [n.AtLeastTwo] :
-    ‖(no_index (OfNat.ofNat n) : ℝ)‖ = OfNat.ofNat n := norm_natCast n
+    ‖(ofNat(n) : ℝ)‖ = OfNat.ofNat n := norm_natCast n
 
 @[simp 1100] lemma nnnorm_ofNat (n : ℕ) [n.AtLeastTwo] :
-    ‖(no_index (OfNat.ofNat n) : ℝ)‖₊ = OfNat.ofNat n := nnnorm_natCast n
+    ‖(ofNat(n) : ℝ)‖₊ = OfNat.ofNat n := nnnorm_natCast n
 
 lemma norm_two : ‖(2 : ℝ)‖ = 2 := abs_of_pos zero_lt_two
 lemma nnnorm_two : ‖(2 : ℝ)‖₊ = 2 := NNReal.eq <| by simp
diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean b/Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
index 0086e643a19b8..1b221e58e8826 100644
--- a/Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
@@ -201,7 +201,7 @@ lemma natCast_arg {n : ℕ} : arg n = 0 :=
   ofReal_natCast n ▸ arg_ofReal_of_nonneg n.cast_nonneg
 
 @[simp]
-lemma ofNat_arg {n : ℕ} [n.AtLeastTwo] : arg (no_index (OfNat.ofNat n)) = 0 :=
+lemma ofNat_arg {n : ℕ} [n.AtLeastTwo] : arg ofNat(n) = 0 :=
   natCast_arg
 
 theorem arg_eq_zero_iff {z : ℂ} : arg z = 0 ↔ 0 ≤ z.re ∧ z.im = 0 := by
diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/Log.lean b/Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
index 6beddd4acf3e0..60934d34bd710 100644
--- a/Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
@@ -65,7 +65,7 @@ lemma natCast_log {n : ℕ} : Real.log n = log n := ofReal_natCast n ▸ ofReal_
 
 @[simp]
 lemma ofNat_log {n : ℕ} [n.AtLeastTwo] :
-    Real.log (no_index (OfNat.ofNat n)) = log (OfNat.ofNat n) :=
+    Real.log ofNat(n) = log (OfNat.ofNat n) :=
   natCast_log
 
 theorem log_ofReal_re (x : ℝ) : (log (x : ℂ)).re = Real.log x := by simp [log_re]
diff --git a/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean b/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
index d8f00d79a6694..5d627dc71ac06 100644
--- a/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
@@ -330,7 +330,7 @@ theorem Gamma_nat_eq_factorial (n : ℕ) : Gamma (n + 1) = n ! := by
 
 @[simp]
 theorem Gamma_ofNat_eq_factorial (n : ℕ) [(n + 1).AtLeastTwo] :
-    Gamma (no_index (OfNat.ofNat (n + 1) : ℂ)) = n ! :=
+    Gamma (ofNat(n + 1) : ℂ) = n ! :=
   mod_cast Gamma_nat_eq_factorial (n : ℕ)
 
 /-- At `0` the Gamma function is undefined; by convention we assign it the value `0`. -/
@@ -434,7 +434,7 @@ theorem Gamma_nat_eq_factorial (n : ℕ) : Gamma (n + 1) = n ! := by
 
 @[simp]
 theorem Gamma_ofNat_eq_factorial (n : ℕ) [(n + 1).AtLeastTwo] :
-    Gamma (no_index (OfNat.ofNat (n + 1) : ℝ)) = n ! :=
+    Gamma (ofNat(n + 1) : ℝ) = n ! :=
   mod_cast Gamma_nat_eq_factorial (n : ℕ)
 
 /-- At `0` the Gamma function is undefined; by convention we assign it the value `0`. -/
diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean b/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
index 43bf1bcc6be45..cbe2f010c0703 100644
--- a/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
@@ -176,7 +176,7 @@ alias rpow_nat_cast := rpow_natCast
 
 @[simp]
 lemma rpow_ofNat (x : ℝ≥0) (n : ℕ) [n.AtLeastTwo] :
-    x ^ (no_index (OfNat.ofNat n) : ℝ) = x ^ (OfNat.ofNat n : ℕ) :=
+    x ^ (ofNat(n) : ℝ) = x ^ (OfNat.ofNat n : ℕ) :=
   rpow_natCast x n
 
 theorem rpow_two (x : ℝ≥0) : x ^ (2 : ℝ) = x ^ 2 := rpow_ofNat x 2
@@ -635,7 +635,7 @@ alias rpow_nat_cast := rpow_natCast
 
 @[simp]
 lemma rpow_ofNat (x : ℝ≥0∞) (n : ℕ) [n.AtLeastTwo] :
-    x ^ (no_index (OfNat.ofNat n) : ℝ) = x ^ (OfNat.ofNat n) :=
+    x ^ (ofNat(n) : ℝ) = x ^ (OfNat.ofNat n) :=
   rpow_natCast x n
 
 @[simp, norm_cast]
diff --git a/Mathlib/Data/ENNReal/Real.lean b/Mathlib/Data/ENNReal/Real.lean
index 879ef89de544e..bf44809f4e036 100644
--- a/Mathlib/Data/ENNReal/Real.lean
+++ b/Mathlib/Data/ENNReal/Real.lean
@@ -216,7 +216,7 @@ lemma ofReal_lt_one {p : ℝ} : ENNReal.ofReal p < 1 ↔ p < 1 := by
 
 @[simp]
 lemma ofReal_lt_ofNat {p : ℝ} {n : ℕ} [n.AtLeastTwo] :
-    ENNReal.ofReal p < no_index (OfNat.ofNat n) ↔ p < OfNat.ofNat n :=
+    ENNReal.ofReal p < ofNat(n) ↔ p < OfNat.ofNat n :=
   ofReal_lt_natCast (NeZero.ne n)
 
 @[simp]
@@ -232,7 +232,7 @@ lemma one_le_ofReal {p : ℝ} : 1 ≤ ENNReal.ofReal p ↔ 1 ≤ p := by
 
 @[simp]
 lemma ofNat_le_ofReal {n : ℕ} [n.AtLeastTwo] {p : ℝ} :
-    no_index (OfNat.ofNat n) ≤ ENNReal.ofReal p ↔ OfNat.ofNat n ≤ p :=
+    ofNat(n) ≤ ENNReal.ofReal p ↔ OfNat.ofNat n ≤ p :=
   natCast_le_ofReal (NeZero.ne n)
 
 @[simp, norm_cast]
@@ -248,7 +248,7 @@ lemma ofReal_le_one {r : ℝ} : ENNReal.ofReal r ≤ 1 ↔ r ≤ 1 :=
 
 @[simp]
 lemma ofReal_le_ofNat {r : ℝ} {n : ℕ} [n.AtLeastTwo] :
-    ENNReal.ofReal r ≤ no_index (OfNat.ofNat n) ↔ r ≤ OfNat.ofNat n :=
+    ENNReal.ofReal r ≤ ofNat(n) ↔ r ≤ OfNat.ofNat n :=
   ofReal_le_natCast
 
 @[simp]
@@ -263,7 +263,7 @@ lemma one_lt_ofReal {r : ℝ} : 1 < ENNReal.ofReal r ↔ 1 < r := coe_lt_coe.tra
 
 @[simp]
 lemma ofNat_lt_ofReal {n : ℕ} [n.AtLeastTwo] {r : ℝ} :
-    no_index (OfNat.ofNat n) < ENNReal.ofReal r ↔ OfNat.ofNat n < r :=
+    ofNat(n) < ENNReal.ofReal r ↔ OfNat.ofNat n < r :=
   natCast_lt_ofReal
 
 @[simp]
@@ -279,7 +279,7 @@ lemma ofReal_eq_one {r : ℝ} : ENNReal.ofReal r = 1 ↔ r = 1 :=
 
 @[simp]
 lemma ofReal_eq_ofNat {r : ℝ} {n : ℕ} [n.AtLeastTwo] :
-    ENNReal.ofReal r = no_index (OfNat.ofNat n) ↔ r = OfNat.ofNat n :=
+    ENNReal.ofReal r = ofNat(n) ↔ r = OfNat.ofNat n :=
   ofReal_eq_natCast (NeZero.ne n)
 
 theorem ofReal_sub (p : ℝ) {q : ℝ} (hq : 0 ≤ q) :
diff --git a/Mathlib/Data/ENat/Basic.lean b/Mathlib/Data/ENat/Basic.lean
index 7f2011f33653d..99492bb51fbaf 100644
--- a/Mathlib/Data/ENat/Basic.lean
+++ b/Mathlib/Data/ENat/Basic.lean
@@ -104,7 +104,7 @@ def lift (x : ℕ∞) (h : x < ⊤) : ℕ := WithTop.untop x (WithTop.lt_top_iff
 @[simp] theorem lift_zero : lift 0 (WithTop.coe_lt_top 0) = 0 := rfl
 @[simp] theorem lift_one : lift 1 (WithTop.coe_lt_top 1) = 1 := rfl
 @[simp] theorem lift_ofNat (n : ℕ) [n.AtLeastTwo] :
-    lift (no_index (OfNat.ofNat n)) (WithTop.coe_lt_top n) = OfNat.ofNat n := rfl
+    lift ofNat(n) (WithTop.coe_lt_top n) = OfNat.ofNat n := rfl
 
 @[simp] theorem add_lt_top {a b : ℕ∞} : a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤ := WithTop.add_lt_top
 
@@ -145,9 +145,8 @@ theorem toNat_zero : toNat 0 = 0 :=
 theorem toNat_one : toNat 1 = 1 :=
   rfl
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
-theorem toNat_ofNat (n : ℕ) [n.AtLeastTwo] : toNat (no_index (OfNat.ofNat n)) = n :=
+theorem toNat_ofNat (n : ℕ) [n.AtLeastTwo] : toNat ofNat(n) = n :=
   rfl
 
 @[simp]
@@ -164,19 +163,17 @@ theorem recTopCoe_zero {C : ℕ∞ → Sort*} (d : C ⊤) (f : ∀ a : ℕ, C a)
 theorem recTopCoe_one {C : ℕ∞ → Sort*} (d : C ⊤) (f : ∀ a : ℕ, C a) : @recTopCoe C d f 1 = f 1 :=
   rfl
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem recTopCoe_ofNat {C : ℕ∞ → Sort*} (d : C ⊤) (f : ∀ a : ℕ, C a) (x : ℕ) [x.AtLeastTwo] :
-    @recTopCoe C d f (no_index (OfNat.ofNat x)) = f (OfNat.ofNat x) :=
+    @recTopCoe C d f ofNat(x) = f (OfNat.ofNat x) :=
   rfl
 
 @[simp]
 theorem top_ne_coe (a : ℕ) : ⊤ ≠ (a : ℕ∞) :=
   nofun
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
-theorem top_ne_ofNat (a : ℕ) [a.AtLeastTwo] : ⊤ ≠ (no_index (OfNat.ofNat a : ℕ∞)) :=
+theorem top_ne_ofNat (a : ℕ) [a.AtLeastTwo] : ⊤ ≠ (ofNat(a) : ℕ∞) :=
   nofun
 
 @[simp] lemma top_ne_zero : (⊤ : ℕ∞) ≠ 0 := nofun
@@ -186,9 +183,8 @@ theorem top_ne_ofNat (a : ℕ) [a.AtLeastTwo] : ⊤ ≠ (no_index (OfNat.ofNat a
 theorem coe_ne_top (a : ℕ) : (a : ℕ∞) ≠ ⊤ :=
   nofun
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
-theorem ofNat_ne_top (a : ℕ) [a.AtLeastTwo] : (no_index (OfNat.ofNat a : ℕ∞)) ≠ ⊤ :=
+theorem ofNat_ne_top (a : ℕ) [a.AtLeastTwo] : (ofNat(a) : ℕ∞) ≠ ⊤ :=
   nofun
 
 @[simp] lemma zero_ne_top : 0 ≠ (⊤ : ℕ∞) := nofun
@@ -202,9 +198,8 @@ theorem top_sub_coe (a : ℕ) : (⊤ : ℕ∞) - a = ⊤ :=
 theorem top_sub_one : (⊤ : ℕ∞) - 1 = ⊤ :=
   top_sub_coe 1
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
-theorem top_sub_ofNat (a : ℕ) [a.AtLeastTwo] : (⊤ : ℕ∞) - (no_index (OfNat.ofNat a)) = ⊤ :=
+theorem top_sub_ofNat (a : ℕ) [a.AtLeastTwo] : (⊤ : ℕ∞) - ofNat(a) = ⊤ :=
   top_sub_coe a
 
 @[simp]
@@ -382,7 +377,7 @@ theorem map_zero (f : ℕ → α) : map f 0 = f 0 := rfl
 theorem map_one (f : ℕ → α) : map f 1 = f 1 := rfl
 
 @[simp]
-theorem map_ofNat (f : ℕ → α) (n : ℕ) [n.AtLeastTwo] : map f (no_index (OfNat.ofNat n)) = f n := rfl
+theorem map_ofNat (f : ℕ → α) (n : ℕ) [n.AtLeastTwo] : map f ofNat(n) = f n := rfl
 
 @[simp]
 lemma map_eq_top_iff {f : ℕ → α} : map f n = ⊤ ↔ n = ⊤ := WithTop.map_eq_top_iff
diff --git a/Mathlib/Data/Matrix/ConjTranspose.lean b/Mathlib/Data/Matrix/ConjTranspose.lean
index 5f5843664ca6b..4b856340799ca 100644
--- a/Mathlib/Data/Matrix/ConjTranspose.lean
+++ b/Mathlib/Data/Matrix/ConjTranspose.lean
@@ -163,17 +163,15 @@ theorem conjTranspose_eq_natCast [DecidableEq n] [Semiring α] [StarRing α]
   (Function.Involutive.eq_iff conjTranspose_conjTranspose).trans <|
     by rw [conjTranspose_natCast]
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem conjTranspose_ofNat [DecidableEq n] [Semiring α] [StarRing α] (d : ℕ) [d.AtLeastTwo] :
-    (no_index (OfNat.ofNat d) : Matrix n n α)ᴴ = OfNat.ofNat d :=
+    (ofNat(d) : Matrix n n α)ᴴ = OfNat.ofNat d :=
   conjTranspose_natCast _
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem conjTranspose_eq_ofNat [DecidableEq n] [Semiring α] [StarRing α]
     {M : Matrix n n α} {d : ℕ} [d.AtLeastTwo] :
-    Mᴴ = no_index (OfNat.ofNat d) ↔ M = OfNat.ofNat d :=
+    Mᴴ = ofNat(d) ↔ M = OfNat.ofNat d :=
   conjTranspose_eq_natCast
 
 @[simp]
@@ -239,11 +237,10 @@ theorem conjTranspose_natCast_smul [Semiring R] [AddCommMonoid α] [StarAddMonoi
     (c : ℕ) (M : Matrix m n α) : ((c : R) • M)ᴴ = (c : R) • Mᴴ :=
   Matrix.ext <| by simp
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem conjTranspose_ofNat_smul [Semiring R] [AddCommMonoid α] [StarAddMonoid α] [Module R α]
     (c : ℕ) [c.AtLeastTwo] (M : Matrix m n α) :
-    ((no_index (OfNat.ofNat c : R)) • M)ᴴ = (OfNat.ofNat c : R) • Mᴴ :=
+    ((ofNat(c) : R) • M)ᴴ = (OfNat.ofNat c : R) • Mᴴ :=
   conjTranspose_natCast_smul c M
 
 @[simp]
@@ -256,11 +253,10 @@ theorem conjTranspose_inv_natCast_smul [DivisionSemiring R] [AddCommMonoid α] [
     [Module R α] (c : ℕ) (M : Matrix m n α) : ((c : R)⁻¹ • M)ᴴ = (c : R)⁻¹ • Mᴴ :=
   Matrix.ext <| by simp
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem conjTranspose_inv_ofNat_smul [DivisionSemiring R] [AddCommMonoid α] [StarAddMonoid α]
     [Module R α] (c : ℕ) [c.AtLeastTwo] (M : Matrix m n α) :
-    ((no_index (OfNat.ofNat c : R))⁻¹ • M)ᴴ = (OfNat.ofNat c : R)⁻¹ • Mᴴ :=
+    ((ofNat(c) : R)⁻¹ • M)ᴴ = (OfNat.ofNat c : R)⁻¹ • Mᴴ :=
   conjTranspose_inv_natCast_smul c M
 
 @[simp]
diff --git a/Mathlib/Data/Matrix/Diagonal.lean b/Mathlib/Data/Matrix/Diagonal.lean
index a1ae509a8b378..89efdc3f4b838 100644
--- a/Mathlib/Data/Matrix/Diagonal.lean
+++ b/Mathlib/Data/Matrix/Diagonal.lean
@@ -117,13 +117,11 @@ theorem diagonal_natCast [Zero α] [NatCast α] (m : ℕ) : diagonal (fun _ : n
 @[norm_cast]
 theorem diagonal_natCast' [Zero α] [NatCast α] (m : ℕ) : diagonal ((m : n → α)) = m := rfl
 
--- See note [no_index around OfNat.ofNat]
 theorem diagonal_ofNat [Zero α] [NatCast α] (m : ℕ) [m.AtLeastTwo] :
-    diagonal (fun _ : n => no_index (OfNat.ofNat m : α)) = OfNat.ofNat m := rfl
+    diagonal (fun _ : n => (ofNat(m) : α)) = OfNat.ofNat m := rfl
 
--- See note [no_index around OfNat.ofNat]
 theorem diagonal_ofNat' [Zero α] [NatCast α] (m : ℕ) [m.AtLeastTwo] :
-    diagonal (no_index (OfNat.ofNat m : n → α)) = OfNat.ofNat m := rfl
+    diagonal (ofNat(m) : n → α) = OfNat.ofNat m := rfl
 
 instance [Zero α] [IntCast α] : IntCast (Matrix n n α) where
   intCast m := diagonal fun _ => m
@@ -146,10 +144,9 @@ protected theorem map_natCast [AddMonoidWithOne α] [AddMonoidWithOne β]
     (d : Matrix n n α).map f = diagonal (fun _ => f d) :=
   diagonal_map h
 
--- See note [no_index around OfNat.ofNat]
 protected theorem map_ofNat [AddMonoidWithOne α] [AddMonoidWithOne β]
     {f : α → β} (h : f 0 = 0) (d : ℕ) [d.AtLeastTwo] :
-    (no_index (OfNat.ofNat d) : Matrix n n α).map f = diagonal (fun _ => f (OfNat.ofNat d)) :=
+    (ofNat(d) : Matrix n n α).map f = diagonal (fun _ => f (OfNat.ofNat d)) :=
   diagonal_map h
 
 protected theorem map_intCast [AddGroupWithOne α] [AddGroupWithOne β]
@@ -310,17 +307,15 @@ theorem transpose_eq_natCast [DecidableEq n] [AddMonoidWithOne α] {M : Matrix n
     Mᵀ = d ↔ M = d :=
   transpose_eq_diagonal
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem transpose_ofNat [DecidableEq n] [AddMonoidWithOne α] (d : ℕ) [d.AtLeastTwo] :
-    (no_index (OfNat.ofNat d) : Matrix n n α)ᵀ = OfNat.ofNat d :=
+    (ofNat(d) : Matrix n n α)ᵀ = OfNat.ofNat d :=
   transpose_natCast _
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem transpose_eq_ofNat [DecidableEq n] [AddMonoidWithOne α]
     {M : Matrix n n α} {d : ℕ} [d.AtLeastTwo] :
-    Mᵀ = no_index (OfNat.ofNat d) ↔ M = OfNat.ofNat d :=
+    Mᵀ = ofNat(d) ↔ M = OfNat.ofNat d :=
   transpose_eq_diagonal
 
 @[simp]
diff --git a/Mathlib/Data/Matrix/Kronecker.lean b/Mathlib/Data/Matrix/Kronecker.lean
index 1d108492e89cf..0d5b9fc77bc99 100644
--- a/Mathlib/Data/Matrix/Kronecker.lean
+++ b/Mathlib/Data/Matrix/Kronecker.lean
@@ -313,12 +313,12 @@ theorem natCast_kronecker [NonAssocSemiring α] [DecidableEq l] (a : ℕ) (B : M
     simp [(Nat.cast_commute a _).eq]
 
 theorem kronecker_ofNat [Semiring α] [DecidableEq n] (A : Matrix l m α) (b : ℕ) [b.AtLeastTwo] :
-    A ⊗ₖ (no_index (OfNat.ofNat b) : Matrix n n α) =
+    A ⊗ₖ (ofNat(b) : Matrix n n α) =
       blockDiagonal fun _ => A <• (OfNat.ofNat b : α) :=
   kronecker_diagonal _ _
 
 theorem ofNat_kronecker [Semiring α] [DecidableEq l] (a : ℕ) [a.AtLeastTwo] (B : Matrix m n α) :
-    (no_index (OfNat.ofNat a) : Matrix l l α) ⊗ₖ B =
+    (ofNat(a) : Matrix l l α) ⊗ₖ B =
       Matrix.reindex (.prodComm _ _) (.prodComm _ _)
         (blockDiagonal fun _ => (OfNat.ofNat a : α) • B) :=
   diagonal_kronecker _ _
diff --git a/Mathlib/Data/Matrix/Mul.lean b/Mathlib/Data/Matrix/Mul.lean
index 96502a2383140..3d4f563be4268 100644
--- a/Mathlib/Data/Matrix/Mul.lean
+++ b/Mathlib/Data/Matrix/Mul.lean
@@ -814,16 +814,14 @@ theorem vecMul_natCast (x : ℕ) (v : m → α) : v ᵥ* x = MulOpposite.op (x :
   vecMul_diagonal_const _ _
 
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem ofNat_mulVec (x : ℕ) [x.AtLeastTwo] (v : m → α) :
-    OfNat.ofNat (no_index x) *ᵥ v = (OfNat.ofNat x : α) • v :=
+    ofNat(x) *ᵥ v = (OfNat.ofNat x : α) • v :=
   natCast_mulVec _ _
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem vecMul_ofNat (x : ℕ) [x.AtLeastTwo] (v : m → α) :
-    v ᵥ* OfNat.ofNat (no_index x) = MulOpposite.op (OfNat.ofNat x : α) • v :=
+    v ᵥ* ofNat(x) = MulOpposite.op (OfNat.ofNat x : α) • v :=
   vecMul_natCast _ _
 
 end NonAssocSemiring
diff --git a/Mathlib/Data/Matrix/Notation.lean b/Mathlib/Data/Matrix/Notation.lean
index 66a14eeaec9ed..b53ad948bf0c6 100644
--- a/Mathlib/Data/Matrix/Notation.lean
+++ b/Mathlib/Data/Matrix/Notation.lean
@@ -418,15 +418,13 @@ theorem natCast_fin_three (n : ℕ) :
   ext i j
   fin_cases i <;> fin_cases j <;> rfl
 
--- See note [no_index around OfNat.ofNat]
 theorem ofNat_fin_two (n : ℕ) [n.AtLeastTwo] :
-    (no_index (OfNat.ofNat n) : Matrix (Fin 2) (Fin 2) α) =
+    (ofNat(n) : Matrix (Fin 2) (Fin 2) α) =
       !![OfNat.ofNat n, 0; 0, OfNat.ofNat n] :=
   natCast_fin_two _
 
--- See note [no_index around OfNat.ofNat]
 theorem ofNat_fin_three (n : ℕ) [n.AtLeastTwo] :
-    (no_index (OfNat.ofNat n) : Matrix (Fin 3) (Fin 3) α) =
+    (ofNat(n) : Matrix (Fin 3) (Fin 3) α) =
       !![OfNat.ofNat n, 0, 0; 0, OfNat.ofNat n, 0; 0, 0, OfNat.ofNat n] :=
   natCast_fin_three _
 
diff --git a/Mathlib/Data/NNRat/Defs.lean b/Mathlib/Data/NNRat/Defs.lean
index 1b559909a9913..05d7636202277 100644
--- a/Mathlib/Data/NNRat/Defs.lean
+++ b/Mathlib/Data/NNRat/Defs.lean
@@ -188,7 +188,6 @@ def coeHom : ℚ≥0 →+* ℚ where
 
 @[simp, norm_cast] lemma coe_natCast (n : ℕ) : (↑(↑n : ℚ≥0) : ℚ) = n := rfl
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem mk_natCast (n : ℕ) : @Eq ℚ≥0 (⟨(n : ℚ), Nat.cast_nonneg' n⟩ : ℚ≥0) n :=
   rfl
@@ -336,10 +335,9 @@ lemma coprime_num_den (q : ℚ≥0) : q.num.Coprime q.den := by simpa [num, den]
 @[simp, norm_cast] lemma num_natCast (n : ℕ) : num n = n := rfl
 @[simp, norm_cast] lemma den_natCast (n : ℕ) : den n = 1 := rfl
 
--- See note [no_index around OfNat.ofNat]
-@[simp] lemma num_ofNat (n : ℕ) [n.AtLeastTwo] : num (no_index (OfNat.ofNat n)) = OfNat.ofNat n :=
+@[simp] lemma num_ofNat (n : ℕ) [n.AtLeastTwo] : num ofNat(n) = OfNat.ofNat n :=
   rfl
-@[simp] lemma den_ofNat (n : ℕ) [n.AtLeastTwo] : den (no_index (OfNat.ofNat n)) = 1 := rfl
+@[simp] lemma den_ofNat (n : ℕ) [n.AtLeastTwo] : den ofNat(n) = 1 := rfl
 
 theorem ext_num_den (hn : p.num = q.num) (hd : p.den = q.den) : p = q := by
   refine ext <| Rat.ext ?_ hd
diff --git a/Mathlib/Data/NNReal/Defs.lean b/Mathlib/Data/NNReal/Defs.lean
index fb7ef70dca4ff..d4e8839414a7d 100644
--- a/Mathlib/Data/NNReal/Defs.lean
+++ b/Mathlib/Data/NNReal/Defs.lean
@@ -314,10 +314,9 @@ theorem mk_natCast (n : ℕ) : @Eq ℝ≥0 (⟨(n : ℝ), n.cast_nonneg⟩ : ℝ
 theorem toNNReal_coe_nat (n : ℕ) : Real.toNNReal n = n :=
   NNReal.eq <| by simp [Real.coe_toNNReal]
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem _root_.Real.toNNReal_ofNat (n : ℕ) [n.AtLeastTwo] :
-    Real.toNNReal (no_index (OfNat.ofNat n)) = OfNat.ofNat n :=
+    Real.toNNReal ofNat(n) = OfNat.ofNat n :=
   toNNReal_coe_nat n
 
 /-- `Real.toNNReal` and `NNReal.toReal : ℝ≥0 → ℝ` form a Galois insertion. -/
@@ -528,7 +527,7 @@ alias toNNReal_eq_nat_cast := toNNReal_eq_natCast
 
 @[simp]
 lemma toNNReal_eq_ofNat {r : ℝ} {n : ℕ} [n.AtLeastTwo] :
-    r.toNNReal = no_index (OfNat.ofNat n) ↔ r = OfNat.ofNat n :=
+    r.toNNReal = ofNat(n) ↔ r = OfNat.ofNat n :=
   toNNReal_eq_natCast (NeZero.ne n)
 
 @[simp]
@@ -559,12 +558,12 @@ alias nat_cast_lt_toNNReal := natCast_lt_toNNReal
 
 @[simp]
 lemma toNNReal_le_ofNat {r : ℝ} {n : ℕ} [n.AtLeastTwo] :
-    r.toNNReal ≤ no_index (OfNat.ofNat n) ↔ r ≤ n :=
+    r.toNNReal ≤ ofNat(n) ↔ r ≤ n :=
   toNNReal_le_natCast
 
 @[simp]
 lemma ofNat_lt_toNNReal {r : ℝ} {n : ℕ} [n.AtLeastTwo] :
-    no_index (OfNat.ofNat n) < r.toNNReal ↔ n < r :=
+    ofNat(n) < r.toNNReal ↔ n < r :=
   natCast_lt_toNNReal
 
 @[simp]
@@ -625,12 +624,12 @@ alias toNNReal_lt_nat_cast := toNNReal_lt_natCast
 
 @[simp]
 lemma toNNReal_lt_ofNat {r : ℝ} {n : ℕ} [n.AtLeastTwo] :
-    r.toNNReal < no_index (OfNat.ofNat n) ↔ r < OfNat.ofNat n :=
+    r.toNNReal < ofNat(n) ↔ r < OfNat.ofNat n :=
   toNNReal_lt_natCast (NeZero.ne n)
 
 @[simp]
 lemma ofNat_le_toNNReal {n : ℕ} {r : ℝ} [n.AtLeastTwo] :
-    no_index (OfNat.ofNat n) ≤ r.toNNReal ↔ OfNat.ofNat n ≤ r :=
+    ofNat(n) ≤ r.toNNReal ↔ OfNat.ofNat n ≤ r :=
   natCast_le_toNNReal (NeZero.ne n)
 
 @[simp]
diff --git a/Mathlib/Data/Nat/Cast/Basic.lean b/Mathlib/Data/Nat/Cast/Basic.lean
index 77459f473b112..4d4457e98263a 100644
--- a/Mathlib/Data/Nat/Cast/Basic.lean
+++ b/Mathlib/Data/Nat/Cast/Basic.lean
@@ -158,12 +158,12 @@ theorem map_natCast [FunLike F R S] [RingHomClass F R S] (f : F) : ∀ n : ℕ,
   map_natCast' f <| map_one f
 
 /-- This lemma is not marked `@[simp]` lemma because its `#discr_tree_key` (for the LHS) would just
-be `DFunLike.coe _ _`, due to the `no_index` that https://github.com/leanprover/lean4/issues/2867
+be `DFunLike.coe _ _`, due to the `ofNat` that https://github.com/leanprover/lean4/issues/2867
 forces us to include, and therefore it would negatively impact performance.
 
 If that issue is resolved, this can be marked `@[simp]`. -/
 theorem map_ofNat [FunLike F R S] [RingHomClass F R S] (f : F) (n : ℕ) [Nat.AtLeastTwo n] :
-    (f (no_index (OfNat.ofNat n)) : S) = OfNat.ofNat n :=
+    (f ofNat(n) : S) = OfNat.ofNat n :=
   map_natCast f n
 
 theorem ext_nat [FunLike F ℕ R] [RingHomClass F ℕ R] (f g : F) : f = g :=
diff --git a/Mathlib/Data/Nat/Cast/Order/Basic.lean b/Mathlib/Data/Nat/Cast/Order/Basic.lean
index 7d749878466c4..6c96978eb5a1b 100644
--- a/Mathlib/Data/Nat/Cast/Order/Basic.lean
+++ b/Mathlib/Data/Nat/Cast/Order/Basic.lean
@@ -42,9 +42,8 @@ theorem cast_nonneg' (n : ℕ) : 0 ≤ (n : α) :=
   @Nat.cast_zero α _ ▸ mono_cast (Nat.zero_le n)
 
 /-- See also `Nat.ofNat_nonneg`, specialised for an `OrderedSemiring`. -/
--- See note [no_index around OfNat.ofNat]
 @[simp low]
-theorem ofNat_nonneg' (n : ℕ) [n.AtLeastTwo] : 0 ≤ (no_index (OfNat.ofNat n : α)) := cast_nonneg' n
+theorem ofNat_nonneg' (n : ℕ) [n.AtLeastTwo] : 0 ≤ (ofNat(n) : α) := cast_nonneg' n
 
 section Nontrivial
 
@@ -100,48 +99,40 @@ theorem cast_le_one : (n : α) ≤ 1 ↔ n ≤ 1 := by rw [← cast_one, cast_le
 section
 variable [m.AtLeastTwo]
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
-theorem ofNat_le_cast : (no_index (OfNat.ofNat m : α)) ≤ n ↔ (OfNat.ofNat m : ℕ) ≤ n :=
+theorem ofNat_le_cast : (ofNat(m) : α) ≤ n ↔ (OfNat.ofNat m : ℕ) ≤ n :=
   cast_le
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
-theorem ofNat_lt_cast : (no_index (OfNat.ofNat m : α)) < n ↔ (OfNat.ofNat m : ℕ) < n :=
+theorem ofNat_lt_cast : (ofNat(m) : α) < n ↔ (OfNat.ofNat m : ℕ) < n :=
   cast_lt
 
 end
 
 variable [n.AtLeastTwo]
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
-theorem cast_le_ofNat : (m : α) ≤ (no_index (OfNat.ofNat n)) ↔ m ≤ OfNat.ofNat n :=
+theorem cast_le_ofNat : (m : α) ≤ (ofNat(n) : α) ↔ m ≤ OfNat.ofNat n :=
   cast_le
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
-theorem cast_lt_ofNat : (m : α) < (no_index (OfNat.ofNat n)) ↔ m < OfNat.ofNat n :=
+theorem cast_lt_ofNat : (m : α) < (ofNat(n) : α) ↔ m < OfNat.ofNat n :=
   cast_lt
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
-theorem one_lt_ofNat : 1 < (no_index (OfNat.ofNat n : α)) :=
+theorem one_lt_ofNat : 1 < (ofNat(n) : α) :=
   one_lt_cast.mpr AtLeastTwo.one_lt
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
-theorem one_le_ofNat : 1 ≤ (no_index (OfNat.ofNat n : α)) :=
+theorem one_le_ofNat : 1 ≤ (ofNat(n) : α) :=
   one_le_cast.mpr NeZero.one_le
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
-theorem not_ofNat_le_one : ¬(no_index (OfNat.ofNat n : α)) ≤ 1 :=
+theorem not_ofNat_le_one : ¬(ofNat(n) : α) ≤ 1 :=
   (cast_le_one.not.trans not_le).mpr AtLeastTwo.one_lt
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
-theorem not_ofNat_lt_one : ¬(no_index (OfNat.ofNat n : α)) < 1 :=
+theorem not_ofNat_lt_one : ¬(ofNat(n) : α) < 1 :=
   mt le_of_lt not_ofNat_le_one
 
 variable [m.AtLeastTwo]
@@ -150,18 +141,14 @@ variable [m.AtLeastTwo]
 -- and `Nat.cast_ofNat`, but their LHSs match literally every inequality, so they're too expensive.
 -- If https://github.com/leanprover/lean4/issues/2867 is fixed in a performant way, these can be made `@[simp]`.
 
--- See note [no_index around OfNat.ofNat]
 -- @[simp]
 theorem ofNat_le :
-    (no_index (OfNat.ofNat m : α)) ≤ (no_index (OfNat.ofNat n)) ↔
-      (OfNat.ofNat m : ℕ) ≤ OfNat.ofNat n :=
+    (ofNat(m) : α) ≤ (ofNat(n) : α) ↔ (OfNat.ofNat m : ℕ) ≤ OfNat.ofNat n :=
   cast_le
 
--- See note [no_index around OfNat.ofNat]
 -- @[simp]
 theorem ofNat_lt :
-    (no_index (OfNat.ofNat m : α)) < (no_index (OfNat.ofNat n)) ↔
-      (OfNat.ofNat m : ℕ) < OfNat.ofNat n :=
+    (ofNat(m) : α) < (ofNat(n) : α) ↔ (OfNat.ofNat m : ℕ) < OfNat.ofNat n :=
   cast_lt
 
 end OrderedSemiring
diff --git a/Mathlib/Data/Nat/Cast/Synonym.lean b/Mathlib/Data/Nat/Cast/Synonym.lean
index 11b1f4d3b233a..e4288948265a2 100644
--- a/Mathlib/Data/Nat/Cast/Synonym.lean
+++ b/Mathlib/Data/Nat/Cast/Synonym.lean
@@ -74,7 +74,7 @@ theorem toLex_natCast [NatCast α] (n : ℕ) : toLex (n : α) = n :=
 
 @[simp]
 theorem toLex_ofNat [NatCast α] (n : ℕ) [n.AtLeastTwo] :
-    (toLex (no_index (OfNat.ofNat n : α))) = OfNat.ofNat n :=
+    toLex ofNat(n) = OfNat.ofNat n :=
   rfl
 
 @[simp]
@@ -83,5 +83,5 @@ theorem ofLex_natCast [NatCast α] (n : ℕ) : (ofLex n : α) = n :=
 
 @[simp]
 theorem ofLex_ofNat [NatCast α] (n : ℕ) [n.AtLeastTwo] :
-    (ofLex (no_index (OfNat.ofNat n : Lex α))) = OfNat.ofNat n :=
+    ofLex (ofNat(n) : Lex α) = OfNat.ofNat n :=
   rfl
diff --git a/Mathlib/Data/Nat/PartENat.lean b/Mathlib/Data/Nat/PartENat.lean
index 1000c54d34db3..22dbf8f8562ca 100644
--- a/Mathlib/Data/Nat/PartENat.lean
+++ b/Mathlib/Data/Nat/PartENat.lean
@@ -114,9 +114,8 @@ theorem natCast_inj {x y : ℕ} : (x : PartENat) = y ↔ x = y :=
 theorem dom_natCast (x : ℕ) : (x : PartENat).Dom :=
   trivial
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
-theorem dom_ofNat (x : ℕ) [x.AtLeastTwo] : (no_index (OfNat.ofNat x : PartENat)).Dom :=
+theorem dom_ofNat (x : ℕ) [x.AtLeastTwo] : (ofNat(x) : PartENat).Dom :=
   trivial
 
 @[simp]
@@ -189,10 +188,9 @@ theorem get_zero (h : (0 : PartENat).Dom) : (0 : PartENat).get h = 0 :=
 theorem get_one (h : (1 : PartENat).Dom) : (1 : PartENat).get h = 1 :=
   rfl
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
-theorem get_ofNat' (x : ℕ) [x.AtLeastTwo] (h : (no_index (OfNat.ofNat x : PartENat)).Dom) :
-    Part.get (no_index (OfNat.ofNat x : PartENat)) h = (no_index (OfNat.ofNat x)) :=
+theorem get_ofNat' (x : ℕ) [x.AtLeastTwo] (h : (ofNat(x) : PartENat).Dom) :
+    Part.get (ofNat(x) : PartENat) h = ofNat(x) :=
   get_natCast' x h
 
 nonrec theorem get_eq_iff_eq_some {a : PartENat} {ha : a.Dom} {b : ℕ} : a.get ha = b ↔ a = some b :=
@@ -327,9 +325,8 @@ theorem zero_lt_top : (0 : PartENat) < ⊤ :=
 theorem one_lt_top : (1 : PartENat) < ⊤ :=
   natCast_lt_top 1
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
-theorem ofNat_lt_top (x : ℕ) [x.AtLeastTwo] : (no_index (OfNat.ofNat x : PartENat)) < ⊤ :=
+theorem ofNat_lt_top (x : ℕ) [x.AtLeastTwo] : (ofNat(x) : PartENat) < ⊤ :=
   natCast_lt_top x
 
 @[simp]
@@ -344,9 +341,8 @@ theorem zero_ne_top : (0 : PartENat) ≠ ⊤ :=
 theorem one_ne_top : (1 : PartENat) ≠ ⊤ :=
   natCast_ne_top 1
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
-theorem ofNat_ne_top (x : ℕ) [x.AtLeastTwo] : (no_index (OfNat.ofNat x : PartENat)) ≠ ⊤ :=
+theorem ofNat_ne_top (x : ℕ) [x.AtLeastTwo] : (ofNat(x) : PartENat) ≠ ⊤ :=
   natCast_ne_top x
 
 theorem not_isMax_natCast (x : ℕ) : ¬IsMax (x : PartENat) :=
@@ -556,7 +552,7 @@ theorem toWithTop_natCast' (n : ℕ) {_ : Decidable (n : PartENat).Dom} :
 
 @[simp]
 theorem toWithTop_ofNat (n : ℕ) [n.AtLeastTwo] {_ : Decidable (OfNat.ofNat n : PartENat).Dom} :
-    toWithTop (no_index (OfNat.ofNat n : PartENat)) = OfNat.ofNat n := toWithTop_natCast' n
+    toWithTop (ofNat(n) : PartENat) = OfNat.ofNat n := toWithTop_natCast' n
 
 -- Porting note: statement changed. Mathlib 3 statement was
 -- ```
@@ -621,7 +617,7 @@ theorem ofENat_zero : ofENat 0 = 0 := rfl
 theorem ofENat_one : ofENat 1 = 1 := rfl
 
 @[simp, norm_cast]
-theorem ofENat_ofNat (n : Nat) [n.AtLeastTwo] : ofENat (no_index (OfNat.ofNat n)) = OfNat.ofNat n :=
+theorem ofENat_ofNat (n : Nat) [n.AtLeastTwo] : ofENat ofNat(n) = OfNat.ofNat n :=
   rfl
 
 @[simp, norm_cast]
@@ -679,7 +675,7 @@ theorem withTopEquiv_one : withTopEquiv 1 = 1 := by
   simp
 
 theorem withTopEquiv_ofNat (n : Nat) [n.AtLeastTwo] :
-    withTopEquiv (no_index (OfNat.ofNat n)) = OfNat.ofNat n := by
+    withTopEquiv ofNat(n) = OfNat.ofNat n := by
   simp
 
 theorem withTopEquiv_le {x y : PartENat} : withTopEquiv x ≤ withTopEquiv y ↔ x ≤ y := by
@@ -701,7 +697,7 @@ theorem withTopEquiv_symm_one : withTopEquiv.symm 1 = 1 := by
   simp
 
 theorem withTopEquiv_symm_ofNat (n : Nat) [n.AtLeastTwo] :
-    withTopEquiv.symm (no_index (OfNat.ofNat n)) = OfNat.ofNat n := by
+    withTopEquiv.symm ofNat(n) = OfNat.ofNat n := by
   simp
 
 theorem withTopEquiv_symm_le {x y : ℕ∞} : withTopEquiv.symm x ≤ withTopEquiv.symm y ↔ x ≤ y := by
diff --git a/Mathlib/Data/Nat/Prime/Int.lean b/Mathlib/Data/Nat/Prime/Int.lean
index d357a3d303050..474b170148988 100644
--- a/Mathlib/Data/Nat/Prime/Int.lean
+++ b/Mathlib/Data/Nat/Prime/Int.lean
@@ -38,10 +38,9 @@ end Nat
 
 namespace Int
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem prime_ofNat_iff {n : ℕ} :
-    Prime (no_index (OfNat.ofNat n : ℤ)) ↔ Nat.Prime (OfNat.ofNat n) :=
+    Prime (ofNat(n) : ℤ) ↔ Nat.Prime (OfNat.ofNat n) :=
   Nat.prime_iff_prime_int.symm
 
 theorem prime_two : Prime (2 : ℤ) :=
diff --git a/Mathlib/Data/PNat/Basic.lean b/Mathlib/Data/PNat/Basic.lean
index 087e1dc61c787..5b28b50869c1a 100644
--- a/Mathlib/Data/PNat/Basic.lean
+++ b/Mathlib/Data/PNat/Basic.lean
@@ -56,12 +56,12 @@ theorem natPred_inj {m n : ℕ+} : m.natPred = n.natPred ↔ m = n :=
 
 @[simp, norm_cast]
 lemma val_ofNat (n : ℕ) [NeZero n] :
-    ((no_index (OfNat.ofNat n) : ℕ+) : ℕ) = OfNat.ofNat n :=
+    ((ofNat(n) : ℕ+) : ℕ) = OfNat.ofNat n :=
   rfl
 
 @[simp]
 lemma mk_ofNat (n : ℕ) (h : 0 < n) :
-    @Eq ℕ+ (⟨no_index (OfNat.ofNat n), h⟩ : ℕ+) (haveI : NeZero n := ⟨h.ne'⟩; OfNat.ofNat n) :=
+    @Eq ℕ+ (⟨ofNat(n), h⟩ : ℕ+) (haveI : NeZero n := ⟨h.ne'⟩; OfNat.ofNat n) :=
   rfl
 
 end PNat
@@ -182,17 +182,17 @@ theorem recOn_succ (n : ℕ+) {p : ℕ+ → Sort*} (p1 hp) :
 
 @[simp]
 theorem ofNat_le_ofNat {m n : ℕ} [NeZero m] [NeZero n] :
-    (no_index (OfNat.ofNat m) : ℕ+) ≤ no_index (OfNat.ofNat n) ↔ OfNat.ofNat m ≤ OfNat.ofNat n :=
+    (ofNat(m) : ℕ+) ≤ ofNat(n) ↔ OfNat.ofNat m ≤ OfNat.ofNat n :=
   .rfl
 
 @[simp]
 theorem ofNat_lt_ofNat {m n : ℕ} [NeZero m] [NeZero n] :
-    (no_index (OfNat.ofNat m) : ℕ+) < no_index (OfNat.ofNat n) ↔ OfNat.ofNat m < OfNat.ofNat n :=
+    (ofNat(m) : ℕ+) < ofNat(n) ↔ OfNat.ofNat m < OfNat.ofNat n :=
   .rfl
 
 @[simp]
 theorem ofNat_inj {m n : ℕ} [NeZero m] [NeZero n] :
-    (no_index (OfNat.ofNat m) : ℕ+) = no_index (OfNat.ofNat n) ↔ OfNat.ofNat m = OfNat.ofNat n :=
+    (ofNat(m) : ℕ+) = ofNat(n) ↔ OfNat.ofNat m = OfNat.ofNat n :=
   Subtype.mk_eq_mk
 
 @[simp, norm_cast]
diff --git a/Mathlib/Data/Rat/Cast/Order.lean b/Mathlib/Data/Rat/Cast/Order.lean
index 618e76fd32375..e5287b4093aaf 100644
--- a/Mathlib/Data/Rat/Cast/Order.lean
+++ b/Mathlib/Data/Rat/Cast/Order.lean
@@ -174,16 +174,16 @@ def castOrderEmbedding : ℚ≥0 ↪o K :=
 section ofNat
 variable {n : ℕ} [n.AtLeastTwo]
 
-@[simp] lemma cast_le_ofNat : (p : K) ≤ no_index (OfNat.ofNat n) ↔ p ≤ OfNat.ofNat n := by
+@[simp] lemma cast_le_ofNat : (p : K) ≤ ofNat(n) ↔ p ≤ OfNat.ofNat n := by
   simp [← cast_le (K := K)]
 
-@[simp] lemma ofNat_le_cast : no_index (OfNat.ofNat n) ≤ (p : K) ↔ OfNat.ofNat n ≤ p := by
+@[simp] lemma ofNat_le_cast : ofNat(n) ≤ (p : K) ↔ OfNat.ofNat n ≤ p := by
   simp [← cast_le (K := K)]
 
-@[simp] lemma cast_lt_ofNat : (p : K) < no_index (OfNat.ofNat n) ↔ p < OfNat.ofNat n := by
+@[simp] lemma cast_lt_ofNat : (p : K) < ofNat(n) ↔ p < OfNat.ofNat n := by
   simp [← cast_lt (K := K)]
 
-@[simp] lemma ofNat_lt_cast : no_index (OfNat.ofNat n) < (p : K) ↔ OfNat.ofNat n < p := by
+@[simp] lemma ofNat_lt_cast : ofNat(n) < (p : K) ↔ OfNat.ofNat n < p := by
   simp [← cast_lt (K := K)]
 
 end ofNat
diff --git a/Mathlib/Data/Rat/Lemmas.lean b/Mathlib/Data/Rat/Lemmas.lean
index 739a18a81c1b1..e0ac6e8bf3883 100644
--- a/Mathlib/Data/Rat/Lemmas.lean
+++ b/Mathlib/Data/Rat/Lemmas.lean
@@ -125,10 +125,9 @@ theorem isSquare_natCast_iff {n : ℕ} : IsSquare (n : ℚ) ↔ IsSquare n := by
 theorem isSquare_intCast_iff {z : ℤ} : IsSquare (z : ℚ) ↔ IsSquare z := by
   simp_rw [isSquare_iff, intCast_num, intCast_den, IsSquare.one, and_true]
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem isSquare_ofNat_iff {n : ℕ} :
-    IsSquare (no_index (OfNat.ofNat n) : ℚ) ↔ IsSquare (OfNat.ofNat n : ℕ) :=
+    IsSquare (ofNat(n) : ℚ) ↔ IsSquare (OfNat.ofNat n : ℕ) :=
   isSquare_natCast_iff
 
 section Casts
@@ -265,7 +264,7 @@ theorem inv_natCast_num (a : ℕ) : (a : ℚ)⁻¹.num = Int.sign a :=
   inv_intCast_num a
 
 @[simp]
-theorem inv_ofNat_num (a : ℕ) [a.AtLeastTwo] : (no_index (OfNat.ofNat a : ℚ))⁻¹.num = 1 :=
+theorem inv_ofNat_num (a : ℕ) [a.AtLeastTwo] : (ofNat(a) : ℚ)⁻¹.num = 1 :=
   inv_natCast_num_of_pos (Nat.pos_of_neZero a)
 
 @[simp]
@@ -301,7 +300,7 @@ theorem inv_natCast_den (a : ℕ) : (a : ℚ)⁻¹.den = if a = 0 then 1 else a
 
 @[simp]
 theorem inv_ofNat_den (a : ℕ) [a.AtLeastTwo] :
-    (no_index (OfNat.ofNat a : ℚ))⁻¹.den = OfNat.ofNat a :=
+    (ofNat(a) : ℚ)⁻¹.den = OfNat.ofNat a :=
   inv_natCast_den_of_pos (Nat.pos_of_neZero a)
 
 protected theorem «forall» {p : ℚ → Prop} : (∀ r, p r) ↔ ∀ a b : ℤ, p (a / b) :=
diff --git a/Mathlib/Data/Rat/Sqrt.lean b/Mathlib/Data/Rat/Sqrt.lean
index 7c9fe65973ca4..5f6d920bde3b8 100644
--- a/Mathlib/Data/Rat/Sqrt.lean
+++ b/Mathlib/Data/Rat/Sqrt.lean
@@ -45,9 +45,8 @@ theorem sqrt_intCast (z : ℤ) : Rat.sqrt (z : ℚ) = Int.sqrt z := by
 theorem sqrt_natCast (n : ℕ) : Rat.sqrt (n : ℚ) = Nat.sqrt n := by
   rw [← Int.cast_natCast, sqrt_intCast, Int.sqrt_natCast, Int.cast_natCast]
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
-theorem sqrt_ofNat (n : ℕ) : Rat.sqrt (no_index (OfNat.ofNat n) : ℚ) = Nat.sqrt (OfNat.ofNat n) :=
+theorem sqrt_ofNat (n : ℕ) : Rat.sqrt (ofNat(n) : ℚ) = Nat.sqrt (OfNat.ofNat n) :=
   sqrt_natCast _
 
 end Rat
diff --git a/Mathlib/Data/Real/Hyperreal.lean b/Mathlib/Data/Real/Hyperreal.lean
index fd849459ea9f9..4e7a601f04cdc 100644
--- a/Mathlib/Data/Real/Hyperreal.lean
+++ b/Mathlib/Data/Real/Hyperreal.lean
@@ -72,10 +72,9 @@ theorem coe_neg (x : ℝ) : ↑(-x) = (-x : ℝ*) :=
 theorem coe_add (x y : ℝ) : ↑(x + y) = (x + y : ℝ*) :=
   rfl
 
--- See note [no_index around OfNat.ofNat]
 @[simp, norm_cast]
 theorem coe_ofNat (n : ℕ) [n.AtLeastTwo] :
-    ((no_index (OfNat.ofNat n : ℝ)) : ℝ*) = OfNat.ofNat n :=
+    ((ofNat(n) : ℝ) : ℝ*) = OfNat.ofNat n :=
   rfl
 
 @[simp, norm_cast]
diff --git a/Mathlib/Data/ZMod/IntUnitsPower.lean b/Mathlib/Data/ZMod/IntUnitsPower.lean
index 61cc3341fdfc7..80e8edf23f8c4 100644
--- a/Mathlib/Data/ZMod/IntUnitsPower.lean
+++ b/Mathlib/Data/ZMod/IntUnitsPower.lean
@@ -71,9 +71,8 @@ example : Int.instUnitsPow = DivInvMonoid.toZPow := rfl
   change ((n : R) • Additive.ofMul u).toMul = _
   rw [Nat.cast_smul_eq_nsmul, toMul_nsmul, toMul_ofMul]
 
--- See note [no_index around OfNat.ofNat]
 lemma uzpow_coe_nat (s : ℤˣ) (n : ℕ) [n.AtLeastTwo] :
-    s ^ (no_index (OfNat.ofNat n : R)) = s ^ (no_index (OfNat.ofNat n : ℕ)) :=
+    s ^ (ofNat(n) : R) = s ^ (ofNat(n) : ℕ) :=
   uzpow_natCast _ _
 
 @[simp] lemma one_uzpow (x : R) : (1 : ℤˣ) ^ x = 1 :=
diff --git a/Mathlib/LinearAlgebra/Matrix/PosDef.lean b/Mathlib/LinearAlgebra/Matrix/PosDef.lean
index fb373744d8173..5e46c1956c392 100644
--- a/Mathlib/LinearAlgebra/Matrix/PosDef.lean
+++ b/Mathlib/LinearAlgebra/Matrix/PosDef.lean
@@ -108,9 +108,8 @@ protected theorem natCast [StarOrderedRing R] [DecidableEq n] (d : ℕ) :
     rw [Nat.cast_smul_eq_nsmul]
     exact nsmul_nonneg (dotProduct_star_self_nonneg _) _⟩
 
--- See note [no_index around OfNat.ofNat]
 protected theorem ofNat [StarOrderedRing R] [DecidableEq n] (d : ℕ) [d.AtLeastTwo] :
-    PosSemidef (no_index (OfNat.ofNat d) : Matrix n n R) :=
+    PosSemidef (ofNat(d) : Matrix n n R) :=
   .natCast d
 
 protected theorem intCast [StarOrderedRing R] [DecidableEq n] (d : ℤ) (hd : 0 ≤ d) :
@@ -386,10 +385,9 @@ theorem _root_.Matrix.posDef_natCast_iff [StarOrderedRing R] [DecidableEq n] [No
     PosDef (d : Matrix n n R) ↔ 0 < d :=
   posDef_diagonal_iff.trans <| by simp
 
--- See note [no_index around OfNat.ofNat]
 protected theorem ofNat [StarOrderedRing R] [DecidableEq n] [NoZeroDivisors R]
     (d : ℕ) [d.AtLeastTwo] :
-    PosDef (no_index (OfNat.ofNat d) : Matrix n n R) :=
+    PosDef (ofNat(d) : Matrix n n R) :=
   .natCast d (NeZero.ne _)
 
 protected theorem intCast [StarOrderedRing R] [DecidableEq n] [NoZeroDivisors R]
diff --git a/Mathlib/NumberTheory/LucasLehmer.lean b/Mathlib/NumberTheory/LucasLehmer.lean
index 7990d0b3b0785..01356b10609e7 100644
--- a/Mathlib/NumberTheory/LucasLehmer.lean
+++ b/Mathlib/NumberTheory/LucasLehmer.lean
@@ -270,14 +270,12 @@ instance : NatCast (X q) where
 
 @[simp] theorem snd_natCast (n : ℕ) : (n : X q).snd = (0 : ZMod q) := rfl
 
--- See note [no_index around OfNat.ofNat]
 @[simp] theorem ofNat_fst (n : ℕ) [n.AtLeastTwo] :
-    (no_index (OfNat.ofNat n) : X q).fst = OfNat.ofNat n :=
+    (ofNat(n) : X q).fst = OfNat.ofNat n :=
   rfl
 
--- See note [no_index around OfNat.ofNat]
 @[simp] theorem ofNat_snd (n : ℕ) [n.AtLeastTwo] :
-    (no_index (OfNat.ofNat n) : X q).snd = 0 :=
+    (ofNat(n) : X q).snd = 0 :=
   rfl
 
 instance : AddGroupWithOne (X q) :=
diff --git a/Mathlib/NumberTheory/Padics/PadicNumbers.lean b/Mathlib/NumberTheory/Padics/PadicNumbers.lean
index a2b72fdf7bbad..c03112d1c05ed 100644
--- a/Mathlib/NumberTheory/Padics/PadicNumbers.lean
+++ b/Mathlib/NumberTheory/Padics/PadicNumbers.lean
@@ -977,10 +977,9 @@ lemma valuation_intCast (n : ℤ) : valuation (n : ℚ_[p]) = padicValInt p n :=
 lemma valuation_natCast (n : ℕ) : valuation (n : ℚ_[p]) = padicValNat p n := by
   rw [← Rat.cast_natCast, valuation_ratCast, padicValRat.of_nat]
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 lemma valuation_ofNat (n : ℕ) [n.AtLeastTwo] :
-    valuation (no_index (OfNat.ofNat n : ℚ_[p])) = padicValNat p n :=
+    valuation (ofNat(n) : ℚ_[p]) = padicValNat p n :=
   valuation_natCast n
 
 @[simp]
diff --git a/Mathlib/NumberTheory/Zsqrtd/Basic.lean b/Mathlib/NumberTheory/Zsqrtd/Basic.lean
index 9d477daf4ffca..f8649a18389ad 100644
--- a/Mathlib/NumberTheory/Zsqrtd/Basic.lean
+++ b/Mathlib/NumberTheory/Zsqrtd/Basic.lean
@@ -230,7 +230,7 @@ theorem natCast_re (n : ℕ) : (n : ℤ√d).re = n :=
   rfl
 
 @[simp]
-theorem ofNat_re (n : ℕ) [n.AtLeastTwo] : (no_index (OfNat.ofNat n) : ℤ√d).re = n :=
+theorem ofNat_re (n : ℕ) [n.AtLeastTwo] : (ofNat(n) : ℤ√d).re = n :=
   rfl
 
 @[simp]
@@ -238,7 +238,7 @@ theorem natCast_im (n : ℕ) : (n : ℤ√d).im = 0 :=
   rfl
 
 @[simp]
-theorem ofNat_im (n : ℕ) [n.AtLeastTwo] : (no_index (OfNat.ofNat n) : ℤ√d).im = 0 :=
+theorem ofNat_im (n : ℕ) [n.AtLeastTwo] : (ofNat(n) : ℤ√d).im = 0 :=
   rfl
 
 theorem natCast_val (n : ℕ) : (n : ℤ√d) = ⟨n, 0⟩ :=
diff --git a/Mathlib/Order/Filter/Germ/Basic.lean b/Mathlib/Order/Filter/Germ/Basic.lean
index fe099e6b204fa..f02186b5a0c53 100644
--- a/Mathlib/Order/Filter/Germ/Basic.lean
+++ b/Mathlib/Order/Filter/Germ/Basic.lean
@@ -427,16 +427,14 @@ theorem natCast_def [NatCast M] (n : ℕ) : ((fun _ ↦ n : α → M) : Germ l M
 @[simp, norm_cast]
 theorem const_nat [NatCast M] (n : ℕ) : ((n : M) : Germ l M) = n := rfl
 
--- See note [no_index around OfNat.ofNat]
 @[simp, norm_cast]
 theorem coe_ofNat [NatCast M] (n : ℕ) [n.AtLeastTwo] :
-    ((no_index (OfNat.ofNat n : α → M)) : Germ l M) = OfNat.ofNat n :=
+    ((ofNat(n) : α → M) : Germ l M) = OfNat.ofNat n :=
   rfl
 
--- See note [no_index around OfNat.ofNat]
 @[simp, norm_cast]
 theorem const_ofNat [NatCast M] (n : ℕ) [n.AtLeastTwo] :
-    ((no_index (OfNat.ofNat n : M)) : Germ l M) = OfNat.ofNat n :=
+    ((ofNat(n) : M) : Germ l M) = OfNat.ofNat n :=
   rfl
 
 instance instIntCast [IntCast M] : IntCast (Germ l M) where intCast n := (n : α → M)
diff --git a/Mathlib/SetTheory/Cardinal/Aleph.lean b/Mathlib/SetTheory/Cardinal/Aleph.lean
index 896cc181244ef..9e69e6a4684de 100644
--- a/Mathlib/SetTheory/Cardinal/Aleph.lean
+++ b/Mathlib/SetTheory/Cardinal/Aleph.lean
@@ -139,9 +139,8 @@ theorem preOmega_natCast (n : ℕ) : preOmega n = n := by
     rw [Nat.cast_lt]
     exact lt_succ n
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
-theorem preOmega_ofNat (n : ℕ) [n.AtLeastTwo] : preOmega (no_index (OfNat.ofNat n)) = n :=
+theorem preOmega_ofNat (n : ℕ) [n.AtLeastTwo] : preOmega ofNat(n) = n :=
   preOmega_natCast n
 
 theorem preOmega_le_of_forall_lt {o a : Ordinal} (ha : IsInitial a) (H : ∀ b < o, preOmega b < a) :
diff --git a/Mathlib/SetTheory/Cardinal/Basic.lean b/Mathlib/SetTheory/Cardinal/Basic.lean
index e2bee0bf6130e..d7038dc655538 100644
--- a/Mathlib/SetTheory/Cardinal/Basic.lean
+++ b/Mathlib/SetTheory/Cardinal/Basic.lean
@@ -1290,10 +1290,9 @@ theorem mk_fin (n : ℕ) : #(Fin n) = n := by simp
 @[simp]
 theorem lift_natCast (n : ℕ) : lift.{u} (n : Cardinal.{v}) = n := by induction n <;> simp [*]
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem lift_ofNat (n : ℕ) [n.AtLeastTwo] :
-    lift.{u} (no_index (OfNat.ofNat n : Cardinal.{v})) = OfNat.ofNat n :=
+    lift.{u} (ofNat(n) : Cardinal.{v}) = OfNat.ofNat n :=
   lift_natCast n
 
 @[simp]
@@ -1302,7 +1301,7 @@ theorem lift_eq_nat_iff {a : Cardinal.{u}} {n : ℕ} : lift.{v} a = n ↔ a = n
 
 @[simp]
 theorem lift_eq_ofNat_iff {a : Cardinal.{u}} {n : ℕ} [n.AtLeastTwo] :
-    lift.{v} a = (no_index (OfNat.ofNat n)) ↔ a = OfNat.ofNat n :=
+    lift.{v} a = ofNat(n) ↔ a = OfNat.ofNat n :=
   lift_eq_nat_iff
 
 @[simp]
@@ -1320,10 +1319,9 @@ theorem one_eq_lift_iff {a : Cardinal.{u}} :
     (1 : Cardinal) = lift.{v} a ↔ 1 = a := by
   simpa using nat_eq_lift_iff (n := 1)
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem ofNat_eq_lift_iff {a : Cardinal.{u}} {n : ℕ} [n.AtLeastTwo] :
-    (no_index (OfNat.ofNat n : Cardinal)) = lift.{v} a ↔ (OfNat.ofNat n : Cardinal) = a :=
+    (ofNat(n) : Cardinal) = lift.{v} a ↔ (OfNat.ofNat n : Cardinal) = a :=
   nat_eq_lift_iff
 
 @[simp]
@@ -1335,10 +1333,9 @@ theorem lift_le_one_iff {a : Cardinal.{u}} :
     lift.{v} a ≤ 1 ↔ a ≤ 1 := by
   simpa using lift_le_nat_iff (n := 1)
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem lift_le_ofNat_iff {a : Cardinal.{u}} {n : ℕ} [n.AtLeastTwo] :
-    lift.{v} a ≤ (no_index (OfNat.ofNat n)) ↔ a ≤ OfNat.ofNat n :=
+    lift.{v} a ≤ ofNat(n) ↔ a ≤ OfNat.ofNat n :=
   lift_le_nat_iff
 
 @[simp]
@@ -1350,27 +1347,24 @@ theorem one_le_lift_iff {a : Cardinal.{u}} :
     (1 : Cardinal) ≤ lift.{v} a ↔ 1 ≤ a := by
   simpa using nat_le_lift_iff (n := 1)
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem ofNat_le_lift_iff {a : Cardinal.{u}} {n : ℕ} [n.AtLeastTwo] :
-    (no_index (OfNat.ofNat n : Cardinal)) ≤ lift.{v} a ↔ (OfNat.ofNat n : Cardinal) ≤ a :=
+    (ofNat(n) : Cardinal) ≤ lift.{v} a ↔ (OfNat.ofNat n : Cardinal) ≤ a :=
   nat_le_lift_iff
 
 @[simp]
 theorem lift_lt_nat_iff {a : Cardinal.{u}} {n : ℕ} : lift.{v} a < n ↔ a < n := by
   rw [← lift_natCast.{v,u}, lift_lt]
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem lift_lt_ofNat_iff {a : Cardinal.{u}} {n : ℕ} [n.AtLeastTwo] :
-    lift.{v} a < (no_index (OfNat.ofNat n)) ↔ a < OfNat.ofNat n :=
+    lift.{v} a < ofNat(n) ↔ a < OfNat.ofNat n :=
   lift_lt_nat_iff
 
 @[simp]
 theorem nat_lt_lift_iff {n : ℕ} {a : Cardinal.{u}} : n < lift.{v} a ↔ n < a := by
   rw [← lift_natCast.{v,u}, lift_lt]
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem zero_lt_lift_iff {a : Cardinal.{u}} :
     (0 : Cardinal) < lift.{v} a ↔ 0 < a := by
@@ -1381,10 +1375,9 @@ theorem one_lt_lift_iff {a : Cardinal.{u}} :
     (1 : Cardinal) < lift.{v} a ↔ 1 < a := by
   simpa using nat_lt_lift_iff (n := 1)
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem ofNat_lt_lift_iff {a : Cardinal.{u}} {n : ℕ} [n.AtLeastTwo] :
-    (no_index (OfNat.ofNat n : Cardinal)) < lift.{v} a ↔ (OfNat.ofNat n : Cardinal) < a :=
+    (ofNat(n) : Cardinal) < lift.{v} a ↔ (OfNat.ofNat n : Cardinal) < a :=
   nat_lt_lift_iff
 
 theorem lift_mk_fin (n : ℕ) : lift #(Fin n) = n := rfl
@@ -1718,14 +1711,12 @@ theorem nat_mul_aleph0 {n : ℕ} (hn : n ≠ 0) : ↑n * ℵ₀ = ℵ₀ :=
 @[simp]
 theorem aleph0_mul_nat {n : ℕ} (hn : n ≠ 0) : ℵ₀ * n = ℵ₀ := by rw [mul_comm, nat_mul_aleph0 hn]
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
-theorem ofNat_mul_aleph0 {n : ℕ} [Nat.AtLeastTwo n] : no_index (OfNat.ofNat n) * ℵ₀ = ℵ₀ :=
+theorem ofNat_mul_aleph0 {n : ℕ} [Nat.AtLeastTwo n] : ofNat(n) * ℵ₀ = ℵ₀ :=
   nat_mul_aleph0 (NeZero.ne n)
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
-theorem aleph0_mul_ofNat {n : ℕ} [Nat.AtLeastTwo n] : ℵ₀ * no_index (OfNat.ofNat n) = ℵ₀ :=
+theorem aleph0_mul_ofNat {n : ℕ} [Nat.AtLeastTwo n] : ℵ₀ * ofNat(n) = ℵ₀ :=
   aleph0_mul_nat (NeZero.ne n)
 
 @[simp]
@@ -1740,14 +1731,12 @@ theorem aleph0_add_nat (n : ℕ) : ℵ₀ + n = ℵ₀ :=
 @[simp]
 theorem nat_add_aleph0 (n : ℕ) : ↑n + ℵ₀ = ℵ₀ := by rw [add_comm, aleph0_add_nat]
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
-theorem ofNat_add_aleph0 {n : ℕ} [Nat.AtLeastTwo n] : no_index (OfNat.ofNat n) + ℵ₀ = ℵ₀ :=
+theorem ofNat_add_aleph0 {n : ℕ} [Nat.AtLeastTwo n] : ofNat(n) + ℵ₀ = ℵ₀ :=
   nat_add_aleph0 n
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
-theorem aleph0_add_ofNat {n : ℕ} [Nat.AtLeastTwo n] : ℵ₀ + no_index (OfNat.ofNat n) = ℵ₀ :=
+theorem aleph0_add_ofNat {n : ℕ} [Nat.AtLeastTwo n] : ℵ₀ + ofNat(n) = ℵ₀ :=
   aleph0_add_nat n
 
 theorem exists_nat_eq_of_le_nat {c : Cardinal} {n : ℕ} (h : c ≤ n) : ∃ m, m ≤ n ∧ c = m := by
diff --git a/Mathlib/SetTheory/Cardinal/Continuum.lean b/Mathlib/SetTheory/Cardinal/Continuum.lean
index c04a55eca2aa0..3f36674f9acb7 100644
--- a/Mathlib/SetTheory/Cardinal/Continuum.lean
+++ b/Mathlib/SetTheory/Cardinal/Continuum.lean
@@ -115,14 +115,12 @@ theorem nat_add_continuum (n : ℕ) : ↑n + 𝔠 = 𝔠 :=
 theorem continuum_add_nat (n : ℕ) : 𝔠 + n = 𝔠 :=
   (add_comm _ _).trans (nat_add_continuum n)
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
-theorem ofNat_add_continuum {n : ℕ} [Nat.AtLeastTwo n] : no_index (OfNat.ofNat n) + 𝔠 = 𝔠 :=
+theorem ofNat_add_continuum {n : ℕ} [Nat.AtLeastTwo n] : ofNat(n) + 𝔠 = 𝔠 :=
   nat_add_continuum n
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
-theorem continuum_add_ofNat {n : ℕ} [Nat.AtLeastTwo n] : 𝔠 + no_index (OfNat.ofNat n) = 𝔠 :=
+theorem continuum_add_ofNat {n : ℕ} [Nat.AtLeastTwo n] : 𝔠 + ofNat(n) = 𝔠 :=
   continuum_add_nat n
 
 /-!
@@ -150,14 +148,12 @@ theorem nat_mul_continuum {n : ℕ} (hn : n ≠ 0) : ↑n * 𝔠 = 𝔠 :=
 theorem continuum_mul_nat {n : ℕ} (hn : n ≠ 0) : 𝔠 * n = 𝔠 :=
   (mul_comm _ _).trans (nat_mul_continuum hn)
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
-theorem ofNat_mul_continuum {n : ℕ} [Nat.AtLeastTwo n] : no_index (OfNat.ofNat n) * 𝔠 = 𝔠 :=
+theorem ofNat_mul_continuum {n : ℕ} [Nat.AtLeastTwo n] : ofNat(n) * 𝔠 = 𝔠 :=
   nat_mul_continuum (OfNat.ofNat_ne_zero n)
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
-theorem continuum_mul_ofNat {n : ℕ} [Nat.AtLeastTwo n] : 𝔠 * no_index (OfNat.ofNat n) = 𝔠 :=
+theorem continuum_mul_ofNat {n : ℕ} [Nat.AtLeastTwo n] : 𝔠 * ofNat(n) = 𝔠 :=
   continuum_mul_nat (OfNat.ofNat_ne_zero n)
 
 /-!
diff --git a/Mathlib/SetTheory/Cardinal/ENat.lean b/Mathlib/SetTheory/Cardinal/ENat.lean
index b444b8fb5cd1f..5ad5cee75b2b2 100644
--- a/Mathlib/SetTheory/Cardinal/ENat.lean
+++ b/Mathlib/SetTheory/Cardinal/ENat.lean
@@ -48,7 +48,7 @@ instance : Coe ENat Cardinal := ⟨Cardinal.ofENat⟩
 @[simp, norm_cast] lemma ofENat_one : ofENat 1 = 1 := rfl
 
 @[simp, norm_cast] lemma ofENat_ofNat (n : ℕ) [n.AtLeastTwo] :
-    ((no_index (OfNat.ofNat n : ℕ∞)) : Cardinal) = OfNat.ofNat n :=
+    ((ofNat(n) : ℕ∞) : Cardinal) = OfNat.ofNat n :=
   rfl
 
 lemma ofENat_strictMono : StrictMono ofENat :=
@@ -67,14 +67,14 @@ lemma ofENat_lt_aleph0 {m : ℕ∞} : (m : Cardinal) < ℵ₀ ↔ m < ⊤ :=
 @[simp] lemma ofENat_lt_nat {m : ℕ∞} {n : ℕ} : ofENat m < n ↔ m < n := by norm_cast
 
 @[simp] lemma ofENat_lt_ofNat {m : ℕ∞} {n : ℕ} [n.AtLeastTwo] :
-    ofENat m < no_index (OfNat.ofNat n) ↔ m < OfNat.ofNat n := ofENat_lt_nat
+    ofENat m < ofNat(n) ↔ m < OfNat.ofNat n := ofENat_lt_nat
 
 @[simp] lemma nat_lt_ofENat {m : ℕ} {n : ℕ∞} : (m : Cardinal) < n ↔ m < n := by norm_cast
 @[simp] lemma ofENat_pos {m : ℕ∞} : 0 < (m : Cardinal) ↔ 0 < m := by norm_cast
 @[simp] lemma one_lt_ofENat {m : ℕ∞} : 1 < (m : Cardinal) ↔ 1 < m := by norm_cast
 
 @[simp, norm_cast] lemma ofNat_lt_ofENat {m : ℕ} [m.AtLeastTwo] {n : ℕ∞} :
-  no_index (OfNat.ofNat m : Cardinal) < n ↔ OfNat.ofNat m < n := nat_lt_ofENat
+  (ofNat(m) : Cardinal) < n ↔ OfNat.ofNat m < n := nat_lt_ofENat
 
 lemma ofENat_mono : Monotone ofENat := ofENat_strictMono.monotone
 
@@ -88,14 +88,14 @@ lemma ofENat_le_ofENat {m n : ℕ∞} : (m : Cardinal) ≤ n ↔ m ≤ n := ofEN
 @[simp] lemma ofENat_le_one {m : ℕ∞} : ofENat m ≤ 1 ↔ m ≤ 1 := by norm_cast
 
 @[simp] lemma ofENat_le_ofNat {m : ℕ∞} {n : ℕ} [n.AtLeastTwo] :
-    ofENat m ≤ no_index (OfNat.ofNat n) ↔ m ≤ OfNat.ofNat n := ofENat_le_nat
+    ofENat m ≤ ofNat(n) ↔ m ≤ OfNat.ofNat n := ofENat_le_nat
 
 @[simp] lemma nat_le_ofENat {m : ℕ} {n : ℕ∞} : (m : Cardinal) ≤ n ↔ m ≤ n := by norm_cast
 @[simp] lemma one_le_ofENat {n : ℕ∞} : 1 ≤ (n : Cardinal) ↔ 1 ≤ n := by norm_cast
 
 @[simp]
 lemma ofNat_le_ofENat {m : ℕ} [m.AtLeastTwo] {n : ℕ∞} :
-    no_index (OfNat.ofNat m : Cardinal) ≤ n ↔ OfNat.ofNat m ≤ n := nat_le_ofENat
+    (ofNat(m) : Cardinal) ≤ n ↔ OfNat.ofNat m ≤ n := nat_le_ofENat
 
 lemma ofENat_injective : Injective ofENat := ofENat_strictMono.injective
 
@@ -112,10 +112,10 @@ lemma ofENat_inj {m n : ℕ∞} : (m : Cardinal) = n ↔ m = n := ofENat_injecti
 @[simp] lemma one_eq_ofENat {m : ℕ∞} : 1 = (m : Cardinal) ↔ m = 1 := by norm_cast; apply eq_comm
 
 @[simp] lemma ofENat_eq_ofNat {m : ℕ∞} {n : ℕ} [n.AtLeastTwo] :
-    (m : Cardinal) = no_index (OfNat.ofNat n) ↔ m = OfNat.ofNat n := ofENat_eq_nat
+    (m : Cardinal) = ofNat(n) ↔ m = OfNat.ofNat n := ofENat_eq_nat
 
 @[simp] lemma ofNat_eq_ofENat {m : ℕ} {n : ℕ∞} [m.AtLeastTwo] :
-    no_index (OfNat.ofNat m) = (n : Cardinal) ↔ OfNat.ofNat m = n := nat_eq_ofENat
+    ofNat(m) = (n : Cardinal) ↔ OfNat.ofNat m = n := nat_eq_ofENat
 
 @[simp, norm_cast] lemma lift_ofENat : ∀ m : ℕ∞, lift.{u, v} m = m
   | (m : ℕ) => lift_natCast m
@@ -247,10 +247,10 @@ lemma toENat_nat (n : ℕ) : toENat n = n := map_natCast _ n
 @[simp] lemma toENat_eq_one {a : Cardinal} : toENat a = 1 ↔ a = 1 := toENat_eq_nat
 
 @[simp] lemma toENat_le_ofNat {a : Cardinal} {n : ℕ} [n.AtLeastTwo] :
-    toENat a ≤ no_index (OfNat.ofNat n) ↔ a ≤ OfNat.ofNat n := toENat_le_nat
+    toENat a ≤ ofNat(n) ↔ a ≤ OfNat.ofNat n := toENat_le_nat
 
 @[simp] lemma toENat_eq_ofNat {a : Cardinal} {n : ℕ} [n.AtLeastTwo] :
-    toENat a = no_index (OfNat.ofNat n) ↔ a = OfNat.ofNat n := toENat_eq_nat
+    toENat a = ofNat(n) ↔ a = OfNat.ofNat n := toENat_eq_nat
 
 @[simp] lemma toENat_eq_top {a : Cardinal} : toENat a = ⊤ ↔ ℵ₀ ≤ a := enat_gc.u_eq_top
 
diff --git a/Mathlib/SetTheory/Cardinal/ToNat.lean b/Mathlib/SetTheory/Cardinal/ToNat.lean
index 80d792d3f53b3..296a181875639 100644
--- a/Mathlib/SetTheory/Cardinal/ToNat.lean
+++ b/Mathlib/SetTheory/Cardinal/ToNat.lean
@@ -85,10 +85,9 @@ theorem toNat_le_toNat (hcd : c ≤ d) (hd : d < ℵ₀) : toNat c ≤ toNat d :
 theorem toNat_lt_toNat (hcd : c < d) (hd : d < ℵ₀) : toNat c < toNat d :=
   toNat_strictMonoOn (hcd.trans hd) hd hcd
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem toNat_ofNat (n : ℕ) [n.AtLeastTwo] :
-    Cardinal.toNat (no_index (OfNat.ofNat n)) = OfNat.ofNat n :=
+    Cardinal.toNat ofNat(n) = OfNat.ofNat n :=
   toNat_natCast n
 
 /-- `toNat` has a right-inverse: coercion. -/
diff --git a/Mathlib/SetTheory/Game/Birthday.lean b/Mathlib/SetTheory/Game/Birthday.lean
index c0da2ca0c18a8..09a00361b6f86 100644
--- a/Mathlib/SetTheory/Game/Birthday.lean
+++ b/Mathlib/SetTheory/Game/Birthday.lean
@@ -215,10 +215,9 @@ theorem birthday_natCast (n : ℕ) : birthday n = n := by
   rw [← toGame_natCast]
   exact birthday_ordinalToGame _
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem birthday_ofNat (n : ℕ) [n.AtLeastTwo] :
-    birthday (no_index (OfNat.ofNat n)) = OfNat.ofNat n :=
+    birthday ofNat(n) = OfNat.ofNat n :=
   birthday_natCast n
 
 @[simp]
diff --git a/Mathlib/SetTheory/Game/Short.lean b/Mathlib/SetTheory/Game/Short.lean
index 0fd2f40701cd5..8ff13c9c88a07 100644
--- a/Mathlib/SetTheory/Game/Short.lean
+++ b/Mathlib/SetTheory/Game/Short.lean
@@ -209,7 +209,7 @@ instance shortNat : ∀ n : ℕ, Short n
   | 0 => PGame.short0
   | n + 1 => @PGame.shortAdd _ _ (shortNat n) PGame.short1
 
-instance shortOfNat (n : ℕ) [Nat.AtLeastTwo n] : Short (no_index (OfNat.ofNat n)) := shortNat n
+instance shortOfNat (n : ℕ) [Nat.AtLeastTwo n] : Short ofNat(n) := shortNat n
 
 instance shortBit0 (x : PGame.{u}) [Short x] : Short (x + x) := by infer_instance
 
diff --git a/Mathlib/SetTheory/Ordinal/Arithmetic.lean b/Mathlib/SetTheory/Ordinal/Arithmetic.lean
index c914bbd405ef9..058fe74f9c6cc 100644
--- a/Mathlib/SetTheory/Ordinal/Arithmetic.lean
+++ b/Mathlib/SetTheory/Ordinal/Arithmetic.lean
@@ -2243,10 +2243,9 @@ theorem one_add_natCast (m : ℕ) : 1 + (m : Ordinal) = succ m := by
 @[deprecated "No deprecation message was provided."  (since := "2024-04-17")]
 alias one_add_nat_cast := one_add_natCast
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem one_add_ofNat (m : ℕ) [m.AtLeastTwo] :
-    1 + (no_index (OfNat.ofNat m : Ordinal)) = Order.succ (OfNat.ofNat m : Ordinal) :=
+    1 + (ofNat(m) : Ordinal) = Order.succ (OfNat.ofNat m : Ordinal) :=
   one_add_natCast m
 
 @[simp, norm_cast]
@@ -2334,10 +2333,9 @@ theorem lift_natCast : ∀ n : ℕ, lift.{u, v} n = n
 @[deprecated "No deprecation message was provided."  (since := "2024-04-17")]
 alias lift_nat_cast := lift_natCast
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem lift_ofNat (n : ℕ) [n.AtLeastTwo] :
-    lift.{u, v} (no_index (OfNat.ofNat n)) = OfNat.ofNat n :=
+    lift.{u, v} ofNat(n) = OfNat.ofNat n :=
   lift_natCast n
 
 /-! ### Properties of ω -/
diff --git a/Mathlib/SetTheory/Ordinal/Basic.lean b/Mathlib/SetTheory/Ordinal/Basic.lean
index 33a1d3e36a834..7f225262b4727 100644
--- a/Mathlib/SetTheory/Ordinal/Basic.lean
+++ b/Mathlib/SetTheory/Ordinal/Basic.lean
@@ -867,10 +867,9 @@ theorem type_sum_lex {α β : Type u} (r : α → α → Prop) (s : β → β 
 theorem card_nat (n : ℕ) : card.{u} n = n := by
   induction n <;> [simp; simp only [card_add, card_one, Nat.cast_succ, *]]
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem card_ofNat (n : ℕ) [n.AtLeastTwo] :
-    card.{u} (no_index (OfNat.ofNat n)) = OfNat.ofNat n :=
+    card.{u} ofNat(n) = OfNat.ofNat n :=
   card_nat n
 
 instance instAddLeftMono : AddLeftMono Ordinal.{u} where
@@ -1211,9 +1210,8 @@ theorem ord_nat (n : ℕ) : ord n = n :=
 @[simp]
 theorem ord_one : ord 1 = 1 := by simpa using ord_nat 1
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
-theorem ord_ofNat (n : ℕ) [n.AtLeastTwo] : ord (no_index (OfNat.ofNat n)) = OfNat.ofNat n :=
+theorem ord_ofNat (n : ℕ) [n.AtLeastTwo] : ord ofNat(n) = OfNat.ofNat n :=
   ord_nat n
 
 @[simp]
@@ -1378,10 +1376,9 @@ theorem nat_le_card {o} {n : ℕ} : (n : Cardinal) ≤ card o ↔ (n : Ordinal)
 theorem one_le_card {o} : 1 ≤ card o ↔ 1 ≤ o := by
   simpa using nat_le_card (n := 1)
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem ofNat_le_card {o} {n : ℕ} [n.AtLeastTwo] :
-    (no_index (OfNat.ofNat n : Cardinal)) ≤ card o ↔ (OfNat.ofNat n : Ordinal) ≤ o :=
+    (ofNat(n) : Cardinal) ≤ card o ↔ (OfNat.ofNat n : Ordinal) ≤ o :=
   nat_le_card
 
 @[simp]
@@ -1405,20 +1402,18 @@ theorem zero_lt_card {o} : 0 < card o ↔ 0 < o := by
 theorem one_lt_card {o} : 1 < card o ↔ 1 < o := by
   simpa using nat_lt_card (n := 1)
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem ofNat_lt_card {o} {n : ℕ} [n.AtLeastTwo] :
-    (no_index (OfNat.ofNat n : Cardinal)) < card o ↔ (OfNat.ofNat n : Ordinal) < o :=
+    (ofNat(n) : Cardinal) < card o ↔ (OfNat.ofNat n : Ordinal) < o :=
   nat_lt_card
 
 @[simp]
 theorem card_lt_nat {o} {n : ℕ} : card o < n ↔ o < n :=
   lt_iff_lt_of_le_iff_le nat_le_card
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem card_lt_ofNat {o} {n : ℕ} [n.AtLeastTwo] :
-    card o < (no_index (OfNat.ofNat n)) ↔ o < OfNat.ofNat n :=
+    card o < ofNat(n) ↔ o < OfNat.ofNat n :=
   card_lt_nat
 
 @[simp]
@@ -1429,10 +1424,9 @@ theorem card_le_nat {o} {n : ℕ} : card o ≤ n ↔ o ≤ n :=
 theorem card_le_one {o} : card o ≤ 1 ↔ o ≤ 1 := by
   simpa using card_le_nat (n := 1)
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem card_le_ofNat {o} {n : ℕ} [n.AtLeastTwo] :
-    card o ≤ (no_index (OfNat.ofNat n)) ↔ o ≤ OfNat.ofNat n :=
+    card o ≤ ofNat(n) ↔ o ≤ OfNat.ofNat n :=
   card_le_nat
 
 @[simp]
@@ -1457,10 +1451,9 @@ theorem lift_down' {a : Cardinal.{u}} {b : Ordinal.{max u v}}
     (h : card.{max u v} b ≤ Cardinal.lift.{v, u} a) : ∃ a', lift.{v, u} a' = b :=
   mem_range_lift_of_card_le h
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem card_eq_ofNat {o} {n : ℕ} [n.AtLeastTwo] :
-    card o = (no_index (OfNat.ofNat n)) ↔ o = OfNat.ofNat n :=
+    card o = ofNat(n) ↔ o = OfNat.ofNat n :=
   card_eq_nat
 
 @[simp]
diff --git a/Mathlib/Tactic/NoncommRing.lean b/Mathlib/Tactic/NoncommRing.lean
index 7cced4a61594d..ad1410a6f8acb 100644
--- a/Mathlib/Tactic/NoncommRing.lean
+++ b/Mathlib/Tactic/NoncommRing.lean
@@ -23,9 +23,9 @@ namespace Mathlib.Tactic.NoncommRing
 section nat_lit_mul
 variable {R : Type*} [NonAssocSemiring R] (r : R) (n : ℕ)
 
-lemma nat_lit_mul_eq_nsmul [n.AtLeastTwo] : no_index (OfNat.ofNat n) * r = OfNat.ofNat n • r := by
+lemma nat_lit_mul_eq_nsmul [n.AtLeastTwo] : ofNat(n) * r = OfNat.ofNat n • r := by
   simp only [nsmul_eq_mul, Nat.cast_ofNat]
-lemma mul_nat_lit_eq_nsmul [n.AtLeastTwo] : r * no_index (OfNat.ofNat n) = OfNat.ofNat n • r := by
+lemma mul_nat_lit_eq_nsmul [n.AtLeastTwo] : r * ofNat(n) = OfNat.ofNat n • r := by
   simp only [nsmul_eq_mul', Nat.cast_ofNat]
 
 end nat_lit_mul
diff --git a/Mathlib/Tactic/Ring/PNat.lean b/Mathlib/Tactic/Ring/PNat.lean
index d5e2883e3d672..5548b15bb156b 100644
--- a/Mathlib/Tactic/Ring/PNat.lean
+++ b/Mathlib/Tactic/Ring/PNat.lean
@@ -19,12 +19,13 @@ instance : CSLift ℕ+ Nat where
   lift := PNat.val
   inj := PNat.coe_injective
 
--- FIXME: this `no_index` seems to be in the wrong place, but
+-- FIXME: this `ofNat` seems to be in the wrong place, but
 -- #synth CSLiftVal (3 : ℕ+) _ doesn't work otherwise
-instance {n} : CSLiftVal (no_index (OfNat.ofNat (n+1)) : ℕ+) (n + 1) := ⟨rfl⟩
+instance {n} : CSLiftVal (ofNat(n+1) : ℕ+) (n + 1) := ⟨rfl⟩
 
 instance {n h} : CSLiftVal (Nat.toPNat n h) n := ⟨rfl⟩
 
+
 instance {n} : CSLiftVal (Nat.succPNat n) (n + 1) := ⟨rfl⟩
 
 instance {n} : CSLiftVal (Nat.toPNat' n) (n.pred + 1) := ⟨rfl⟩
diff --git a/Mathlib/Topology/Algebra/Module/LinearMap.lean b/Mathlib/Topology/Algebra/Module/LinearMap.lean
index 48a01db20692e..c11c4e9d10354 100644
--- a/Mathlib/Topology/Algebra/Module/LinearMap.lean
+++ b/Mathlib/Topology/Algebra/Module/LinearMap.lean
@@ -505,7 +505,7 @@ theorem natCast_apply [ContinuousAdd M₁] (n : ℕ) (m : M₁) : (↑n : M₁ 
 
 @[simp]
 theorem ofNat_apply [ContinuousAdd M₁] (n : ℕ) [n.AtLeastTwo] (m : M₁) :
-    ((no_index (OfNat.ofNat n) : M₁ →L[R₁] M₁)) m = OfNat.ofNat n • m :=
+    (ofNat(n) : M₁ →L[R₁] M₁) m = OfNat.ofNat n • m :=
   rfl
 
 section ApplyAction
diff --git a/Mathlib/Topology/Algebra/SeparationQuotient/Basic.lean b/Mathlib/Topology/Algebra/SeparationQuotient/Basic.lean
index 14e8443fb52c5..536e68588f287 100644
--- a/Mathlib/Topology/Algebra/SeparationQuotient/Basic.lean
+++ b/Mathlib/Topology/Algebra/SeparationQuotient/Basic.lean
@@ -268,7 +268,7 @@ theorem mk_natCast [NatCast R] (n : ℕ) : mk (n : R) = n := rfl
 
 @[simp]
 theorem mk_ofNat [NatCast R] (n : ℕ) [n.AtLeastTwo] :
-    mk (no_index (OfNat.ofNat n) : R) = OfNat.ofNat n :=
+    mk (ofNat(n) : R) = OfNat.ofNat n :=
   rfl
 
 instance instIntCast [IntCast R] : IntCast (SeparationQuotient R) where