chore(*): replace no_index (ofNat n) with ofNat(n) everywhere

This PR was made by searching for `no_index.*ofNat` and replacing all of the relevant occurrences with `ofNat(n)`. This is a rather naïve approach, but at least puts everything back in the same notation for easier applying and reviewing of later fixes.
leanprover-community · Jan 6, 2025 · 2ea8ebe · 2ea8ebe
1 parent 5716319
commit 2ea8ebe
Show file tree

Hide file tree

Showing 53 changed files with 157 additions and 237 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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