diff --git a/Counterexamples/Cyclotomic105.lean b/Counterexamples/Cyclotomic105.lean
index 7d9d4d28b945bd..0b0b6c3f5a89af 100644
--- a/Counterexamples/Cyclotomic105.lean
+++ b/Counterexamples/Cyclotomic105.lean
@@ -94,7 +94,10 @@ theorem cyclotomic_105 :
   repeat' norm_num
 
 theorem coeff_cyclotomic_105 : coeff (cyclotomic 105 ℤ) 7 = -2 := by
-  simp [cyclotomic_105, coeff_one, coeff_X_of_ne_one]
+  rw [cyclotomic_105]
+  -- `Int.reduceNeg` produces an invalid proof that incorrectly transforms this goal into `False`,
+  -- c.f. https://github.com/leanprover/lean4/issues/6467.
+  simp [coeff_X_of_ne_one, coeff_one, -Int.reduceNeg]
 
 theorem not_forall_coeff_cyclotomic_neg_one_zero_one :
     ¬∀ n i, coeff (cyclotomic n ℤ) i ∈ ({-1, 0, 1} : Set ℤ) := by
diff --git a/Mathlib.lean b/Mathlib.lean
index 64737dac22cb7e..2de875ff969dea 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -4941,6 +4941,7 @@ import Mathlib.Tactic.NormNum.Prime
 import Mathlib.Tactic.NormNum.Result
 import Mathlib.Tactic.NthRewrite
 import Mathlib.Tactic.Observe
+import Mathlib.Tactic.OfNat
 import Mathlib.Tactic.PPWithUniv
 import Mathlib.Tactic.Peel
 import Mathlib.Tactic.Polyrith
diff --git a/Mathlib/Algebra/CharP/Defs.lean b/Mathlib/Algebra/CharP/Defs.lean
index 00eef1858e8460..0e349074434102 100644
--- a/Mathlib/Algebra/CharP/Defs.lean
+++ b/Mathlib/Algebra/CharP/Defs.lean
@@ -61,14 +61,12 @@ lemma natCast_eq_natCast' (h : a ≡ b [MOD p]) : (a : R) = b := by
 
 @[simp] lemma cast_eq_zero : (p : R) = 0 := (cast_eq_zero_iff R p p).2 dvd_rfl
 
--- See note [no_index around OfNat.ofNat]
---
 -- TODO: This lemma needs to be `@[simp]` for confluence in the presence of `CharP.cast_eq_zero` and
 -- `Nat.cast_ofNat`, but with `no_index` on its entire LHS, it matches literally every expression so
 -- is too expensive. If https://github.com/leanprover/lean4/issues/2867 is fixed in a performant way, this can be made `@[simp]`.
 --
 -- @[simp]
-lemma ofNat_eq_zero [p.AtLeastTwo] : no_index (OfNat.ofNat p : R) = 0 := cast_eq_zero R p
+lemma ofNat_eq_zero [p.AtLeastTwo] : (ofNat(p) : R) = 0 := cast_eq_zero R p
 
 lemma natCast_eq_natCast_mod (a : ℕ) : (a : R) = a % p :=
   natCast_eq_natCast' R p (Nat.mod_modEq a p).symm
diff --git a/Mathlib/Algebra/DirectSum/Ring.lean b/Mathlib/Algebra/DirectSum/Ring.lean
index 883dc0bb086a7f..1ad1ff8412c36e 100644
--- a/Mathlib/Algebra/DirectSum/Ring.lean
+++ b/Mathlib/Algebra/DirectSum/Ring.lean
@@ -424,9 +424,8 @@ instance : NatCast (A 0) :=
 theorem of_natCast (n : ℕ) : of A 0 n = n :=
   rfl
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
-theorem of_zero_ofNat (n : ℕ) [n.AtLeastTwo] : of A 0 (no_index (OfNat.ofNat n)) = OfNat.ofNat n :=
+theorem of_zero_ofNat (n : ℕ) [n.AtLeastTwo] : of A 0 ofNat(n) = ofNat(n) :=
   of_natCast A n
 
 /-- The `Semiring` structure derived from `GSemiring A`. -/
diff --git a/Mathlib/Algebra/Group/Defs.lean b/Mathlib/Algebra/Group/Defs.lean
index ab65c89102d885..324b405f14be4d 100644
--- a/Mathlib/Algebra/Group/Defs.lean
+++ b/Mathlib/Algebra/Group/Defs.lean
@@ -9,6 +9,7 @@ import Mathlib.Algebra.Group.ZeroOne
 import Mathlib.Algebra.Group.Operations
 import Mathlib.Logic.Function.Defs
 import Mathlib.Tactic.Simps.Basic
+import Mathlib.Tactic.OfNat
 import Batteries.Logic
 
 /-!
@@ -888,9 +889,8 @@ theorem zpow_natCast (a : G) : ∀ n : ℕ, a ^ (n : ℤ) = a ^ n
 @[deprecated (since := "2024-03-20")] alias zpow_coe_nat := zpow_natCast
 @[deprecated (since := "2024-03-20")] alias coe_nat_zsmul := natCast_zsmul
 
--- See note [no_index around OfNat.ofNat]
 @[to_additive ofNat_zsmul]
-lemma zpow_ofNat (a : G) (n : ℕ) : a ^ (no_index (OfNat.ofNat n) : ℤ) = a ^ OfNat.ofNat n :=
+lemma zpow_ofNat (a : G) (n : ℕ) : a ^ (ofNat(n) : ℤ) = a ^ OfNat.ofNat n :=
   zpow_natCast ..
 
 theorem zpow_negSucc (a : G) (n : ℕ) : a ^ (Int.negSucc n) = (a ^ (n + 1))⁻¹ := by
diff --git a/Mathlib/Algebra/Group/Hom/End.lean b/Mathlib/Algebra/Group/Hom/End.lean
index caa7de5333f3dc..f3538c92cd2d92 100644
--- a/Mathlib/Algebra/Group/Hom/End.lean
+++ b/Mathlib/Algebra/Group/Hom/End.lean
@@ -34,9 +34,8 @@ instance instAddMonoidWithOne (M) [AddCommMonoid M] : AddMonoidWithOne (AddMonoi
 @[simp]
 lemma natCast_apply [AddCommMonoid M] (n : ℕ) (m : M) : (↑n : AddMonoid.End M) m = n • m := rfl
 
--- See note [no_index around OfNat.ofNat]
 @[simp] lemma ofNat_apply [AddCommMonoid M] (n : ℕ) [n.AtLeastTwo] (m : M) :
-    (no_index (OfNat.ofNat n : AddMonoid.End M)) m = n • m := rfl
+    (ofNat(n) : AddMonoid.End M) m = n • m := rfl
 
 instance instSemiring [AddCommMonoid M] : Semiring (AddMonoid.End M) :=
   { AddMonoid.End.monoid M, AddMonoidHom.addCommMonoid, AddMonoid.End.instAddMonoidWithOne M with
diff --git a/Mathlib/Algebra/Group/Opposite.lean b/Mathlib/Algebra/Group/Opposite.lean
index fbb777e3f9af91..527a665d95d21b 100644
--- a/Mathlib/Algebra/Group/Opposite.lean
+++ b/Mathlib/Algebra/Group/Opposite.lean
@@ -208,10 +208,9 @@ end DivInvMonoid
 theorem op_natCast [NatCast α] (n : ℕ) : op (n : α) = n :=
   rfl
 
--- See note [no_index around OfNat.ofNat]
 @[to_additive (attr := simp)]
 theorem op_ofNat [NatCast α] (n : ℕ) [n.AtLeastTwo] :
-    op (no_index (OfNat.ofNat n : α)) = OfNat.ofNat n :=
+    op (ofNat(n) : α) = ofNat(n) :=
   rfl
 
 @[to_additive (attr := simp, norm_cast)]
@@ -222,10 +221,9 @@ theorem op_intCast [IntCast α] (n : ℤ) : op (n : α) = n :=
 theorem unop_natCast [NatCast α] (n : ℕ) : unop (n : αᵐᵒᵖ) = n :=
   rfl
 
--- See note [no_index around OfNat.ofNat]
 @[to_additive (attr := simp)]
 theorem unop_ofNat [NatCast α] (n : ℕ) [n.AtLeastTwo] :
-    unop (no_index (OfNat.ofNat n : αᵐᵒᵖ)) = OfNat.ofNat n :=
+    unop (ofNat(n) : αᵐᵒᵖ) = ofNat(n) :=
   rfl
 
 @[to_additive (attr := simp, norm_cast)]
diff --git a/Mathlib/Algebra/Group/ULift.lean b/Mathlib/Algebra/Group/ULift.lean
index ce331c7da82881..f7088335116e88 100644
--- a/Mathlib/Algebra/Group/ULift.lean
+++ b/Mathlib/Algebra/Group/ULift.lean
@@ -112,10 +112,9 @@ instance instIntCast [IntCast α] : IntCast (ULift α) := ⟨(up ·)⟩
 theorem up_natCast [NatCast α] (n : ℕ) : up (n : α) = n :=
   rfl
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem up_ofNat [NatCast α] (n : ℕ) [n.AtLeastTwo] :
-    up (no_index (OfNat.ofNat n : α)) = OfNat.ofNat n :=
+    up (ofNat(n) : α) = ofNat(n) :=
   rfl
 
 @[simp, norm_cast]
@@ -126,10 +125,9 @@ theorem up_intCast [IntCast α] (n : ℤ) : up (n : α) = n :=
 theorem down_natCast [NatCast α] (n : ℕ) : down (n : ULift α) = n :=
   rfl
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem down_ofNat [NatCast α] (n : ℕ) [n.AtLeastTwo] :
-    down (no_index (OfNat.ofNat n : ULift α)) = OfNat.ofNat n :=
+    down (ofNat(n) : ULift α) = ofNat(n) :=
   rfl
 
 @[simp, norm_cast]
diff --git a/Mathlib/Algebra/Module/NatInt.lean b/Mathlib/Algebra/Module/NatInt.lean
index 22860f13912659..a0ef8033c90e57 100644
--- a/Mathlib/Algebra/Module/NatInt.lean
+++ b/Mathlib/Algebra/Module/NatInt.lean
@@ -102,9 +102,8 @@ lemma Nat.cast_smul_eq_nsmul (n : ℕ) (b : M) : (n : R) • b = n • b := by
   | succ n ih => rw [Nat.cast_succ, add_smul, add_smul, one_smul, ih, one_smul]
 
 /-- `nsmul` is equal to any other module structure via a cast. -/
--- See note [no_index around OfNat.ofNat]
 lemma ofNat_smul_eq_nsmul (n : ℕ) [n.AtLeastTwo] (b : M) :
-    (no_index (OfNat.ofNat n) : R) • b = OfNat.ofNat n • b := Nat.cast_smul_eq_nsmul ..
+    (ofNat(n) : R) • b = OfNat.ofNat n • b := Nat.cast_smul_eq_nsmul ..
 
 /-- `nsmul` is equal to any other module structure via a cast. -/
 @[deprecated Nat.cast_smul_eq_nsmul (since := "2024-07-23")]
diff --git a/Mathlib/Algebra/MvPolynomial/Basic.lean b/Mathlib/Algebra/MvPolynomial/Basic.lean
index ffbf49a56e5dda..154517230d9069 100644
--- a/Mathlib/Algebra/MvPolynomial/Basic.lean
+++ b/Mathlib/Algebra/MvPolynomial/Basic.lean
@@ -922,9 +922,8 @@ theorem eval₂_one : (1 : MvPolynomial σ R).eval₂ f g = 1 :=
 @[simp] theorem eval₂_natCast (n : Nat) : (n : MvPolynomial σ R).eval₂ f g = n :=
   (eval₂_C _ _ _).trans (map_natCast f n)
 
--- See note [no_index around OfNat.ofNat]
 @[simp] theorem eval₂_ofNat (n : Nat) [n.AtLeastTwo] :
-    (no_index (OfNat.ofNat n) : MvPolynomial σ R).eval₂ f g = OfNat.ofNat n :=
+    (ofNat(n) : MvPolynomial σ R).eval₂ f g = ofNat(n) :=
   eval₂_natCast f g n
 
 @[simp]
@@ -1077,9 +1076,8 @@ theorem eval_C : ∀ a, eval f (C a) = a :=
 theorem eval_X : ∀ n, eval f (X n) = f n :=
   eval₂_X _ _
 
--- See note [no_index around OfNat.ofNat]
 @[simp] theorem eval_ofNat (n : Nat) [n.AtLeastTwo] :
-    (no_index (OfNat.ofNat n) : MvPolynomial σ R).eval f = OfNat.ofNat n :=
+    (ofNat(n) : MvPolynomial σ R).eval f = ofNat(n) :=
   map_ofNat _ n
 
 @[simp]
@@ -1142,9 +1140,8 @@ theorem map_monomial (s : σ →₀ ℕ) (a : R) : map f (monomial s a) = monomi
 theorem map_C : ∀ a : R, map f (C a : MvPolynomial σ R) = C (f a) :=
   map_monomial _ _
 
--- See note [no_index around OfNat.ofNat]
 @[simp] protected theorem map_ofNat (n : Nat) [n.AtLeastTwo] :
-    (no_index (OfNat.ofNat n) : MvPolynomial σ R).map f = OfNat.ofNat n :=
+    (ofNat(n) : MvPolynomial σ R).map f = ofNat(n) :=
   _root_.map_ofNat _ _
 
 @[simp]
@@ -1366,9 +1363,8 @@ theorem aeval_X (s : σ) : aeval f (X s : MvPolynomial _ R) = f s :=
 theorem aeval_C (r : R) : aeval f (C r) = algebraMap R S₁ r :=
   eval₂_C _ _ _
 
--- See note [no_index around OfNat.ofNat]
 @[simp] theorem aeval_ofNat (n : Nat) [n.AtLeastTwo] :
-    aeval f (no_index (OfNat.ofNat n) : MvPolynomial σ R) = OfNat.ofNat n :=
+    aeval f (ofNat(n) : MvPolynomial σ R) = ofNat(n) :=
   map_ofNat _ _
 
 theorem aeval_unique (φ : MvPolynomial σ R →ₐ[R] S₁) : φ = aeval (φ ∘ X) := by
@@ -1502,10 +1498,9 @@ theorem aevalTower_X (i : σ) : aevalTower g y (X i) = y i :=
 theorem aevalTower_C (x : R) : aevalTower g y (C x) = g x :=
   eval₂_C _ _ _
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem aevalTower_ofNat (n : Nat) [n.AtLeastTwo] :
-    aevalTower g y (no_index (OfNat.ofNat n) : MvPolynomial σ R) = OfNat.ofNat n :=
+    aevalTower g y (ofNat(n) : MvPolynomial σ R) = ofNat(n) :=
   _root_.map_ofNat _ _
 
 @[simp]
diff --git a/Mathlib/Algebra/Order/Floor.lean b/Mathlib/Algebra/Order/Floor.lean
index bc330a5f70b730..a4bf99e945b6e7 100644
--- a/Mathlib/Algebra/Order/Floor.lean
+++ b/Mathlib/Algebra/Order/Floor.lean
@@ -170,9 +170,8 @@ theorem floor_zero : ⌊(0 : α)⌋₊ = 0 := by rw [← Nat.cast_zero, floor_na
 @[simp]
 theorem floor_one : ⌊(1 : α)⌋₊ = 1 := by rw [← Nat.cast_one, floor_natCast]
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
-theorem floor_ofNat (n : ℕ) [n.AtLeastTwo] : ⌊no_index (OfNat.ofNat n : α)⌋₊ = n :=
+theorem floor_ofNat (n : ℕ) [n.AtLeastTwo] : ⌊(ofNat(n) : α)⌋₊ = ofNat(n) :=
   Nat.floor_natCast _
 
 theorem floor_of_nonpos (ha : a ≤ 0) : ⌊a⌋₊ = 0 :=
@@ -291,9 +290,8 @@ theorem ceil_zero : ⌈(0 : α)⌉₊ = 0 := by rw [← Nat.cast_zero, ceil_natC
 @[simp]
 theorem ceil_one : ⌈(1 : α)⌉₊ = 1 := by rw [← Nat.cast_one, ceil_natCast]
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
-theorem ceil_ofNat (n : ℕ) [n.AtLeastTwo] : ⌈no_index (OfNat.ofNat n : α)⌉₊ = n := ceil_natCast n
+theorem ceil_ofNat (n : ℕ) [n.AtLeastTwo] : ⌈(ofNat(n) : α)⌉₊ = ofNat(n) := ceil_natCast n
 
 @[simp]
 theorem ceil_eq_zero : ⌈a⌉₊ = 0 ↔ a ≤ 0 := by rw [← Nat.le_zero, ceil_le, Nat.cast_zero]
@@ -402,9 +400,8 @@ theorem floor_add_one (ha : 0 ≤ a) : ⌊a + 1⌋₊ = ⌊a⌋₊ + 1 := by
   -- Porting note: broken `convert floor_add_nat ha 1`
   rw [← cast_one, floor_add_nat ha 1]
 
--- See note [no_index around OfNat.ofNat]
 theorem floor_add_ofNat (ha : 0 ≤ a) (n : ℕ) [n.AtLeastTwo] :
-    ⌊a + (no_index (OfNat.ofNat n))⌋₊ = ⌊a⌋₊ + OfNat.ofNat n :=
+    ⌊a + ofNat(n)⌋₊ = ⌊a⌋₊ + ofNat(n) :=
   floor_add_nat ha n
 
 @[simp]
@@ -422,10 +419,9 @@ theorem floor_sub_nat [Sub α] [OrderedSub α] [ExistsAddOfLE α] (a : α) (n :
 theorem floor_sub_one [Sub α] [OrderedSub α] [ExistsAddOfLE α] (a : α) : ⌊a - 1⌋₊ = ⌊a⌋₊ - 1 :=
   mod_cast floor_sub_nat a 1
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem floor_sub_ofNat [Sub α] [OrderedSub α] [ExistsAddOfLE α] (a : α) (n : ℕ) [n.AtLeastTwo] :
-    ⌊a - (no_index (OfNat.ofNat n))⌋₊ = ⌊a⌋₊ - OfNat.ofNat n :=
+    ⌊a - ofNat(n)⌋₊ = ⌊a⌋₊ - ofNat(n) :=
   floor_sub_nat a n
 
 theorem ceil_add_nat (ha : 0 ≤ a) (n : ℕ) : ⌈a + n⌉₊ = ⌈a⌉₊ + n :=
@@ -441,9 +437,8 @@ theorem ceil_add_one (ha : 0 ≤ a) : ⌈a + 1⌉₊ = ⌈a⌉₊ + 1 := by
   -- Porting note: broken `convert ceil_add_nat ha 1`
   rw [cast_one.symm, ceil_add_nat ha 1]
 
--- See note [no_index around OfNat.ofNat]
 theorem ceil_add_ofNat (ha : 0 ≤ a) (n : ℕ) [n.AtLeastTwo] :
-    ⌈a + (no_index (OfNat.ofNat n))⌉₊ = ⌈a⌉₊ + OfNat.ofNat n :=
+    ⌈a + ofNat(n)⌉₊ = ⌈a⌉₊ + ofNat(n) :=
   ceil_add_nat ha n
 
 @[bound]
@@ -488,9 +483,8 @@ theorem floor_div_nat (a : α) (n : ℕ) : ⌊a / n⌋₊ = ⌊a⌋₊ / n := by
   · exact lt_div_mul_add hn
   · exact cast_pos.2 hn
 
--- See note [no_index around OfNat.ofNat]
 theorem floor_div_ofNat (a : α) (n : ℕ) [n.AtLeastTwo] :
-    ⌊a / (no_index (OfNat.ofNat n))⌋₊ = ⌊a⌋₊ / OfNat.ofNat n :=
+    ⌊a / ofNat(n)⌋₊ = ⌊a⌋₊ / ofNat(n) :=
   floor_div_nat a n
 
 /-- Natural division is the floor of field division. -/
@@ -699,8 +693,7 @@ theorem floor_zero : ⌊(0 : α)⌋ = 0 := by rw [← cast_zero, floor_intCast]
 @[simp]
 theorem floor_one : ⌊(1 : α)⌋ = 1 := by rw [← cast_one, floor_intCast]
 
--- See note [no_index around OfNat.ofNat]
-@[simp] theorem floor_ofNat (n : ℕ) [n.AtLeastTwo] : ⌊(no_index (OfNat.ofNat n : α))⌋ = n :=
+@[simp] theorem floor_ofNat (n : ℕ) [n.AtLeastTwo] : ⌊(ofNat(n) : α)⌋ = ofNat(n) :=
   floor_natCast n
 
 @[mono]
@@ -743,20 +736,18 @@ theorem floor_int_add (z : ℤ) (a : α) : ⌊↑z + a⌋ = z + ⌊a⌋ := by
 theorem floor_add_nat (a : α) (n : ℕ) : ⌊a + n⌋ = ⌊a⌋ + n := by
   rw [← Int.cast_natCast, floor_add_int]
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem floor_add_ofNat (a : α) (n : ℕ) [n.AtLeastTwo] :
-    ⌊a + (no_index (OfNat.ofNat n))⌋ = ⌊a⌋ + OfNat.ofNat n :=
+    ⌊a + ofNat(n)⌋ = ⌊a⌋ + ofNat(n) :=
   floor_add_nat a n
 
 @[simp]
 theorem floor_nat_add (n : ℕ) (a : α) : ⌊↑n + a⌋ = n + ⌊a⌋ := by
   rw [← Int.cast_natCast, floor_int_add]
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem floor_ofNat_add (n : ℕ) [n.AtLeastTwo] (a : α) :
-    ⌊(no_index (OfNat.ofNat n)) + a⌋ = OfNat.ofNat n + ⌊a⌋ :=
+    ⌊ofNat(n) + a⌋ = ofNat(n) + ⌊a⌋ :=
   floor_nat_add n a
 
 @[simp]
@@ -769,10 +760,9 @@ theorem floor_sub_nat (a : α) (n : ℕ) : ⌊a - n⌋ = ⌊a⌋ - n := by
 
 @[simp] theorem floor_sub_one (a : α) : ⌊a - 1⌋ = ⌊a⌋ - 1 := mod_cast floor_sub_nat a 1
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem floor_sub_ofNat (a : α) (n : ℕ) [n.AtLeastTwo] :
-    ⌊a - (no_index (OfNat.ofNat n))⌋ = ⌊a⌋ - OfNat.ofNat n :=
+    ⌊a - ofNat(n)⌋ = ⌊a⌋ - ofNat(n) :=
   floor_sub_nat a n
 
 theorem abs_sub_lt_one_of_floor_eq_floor {α : Type*} [LinearOrderedCommRing α] [FloorRing α]
@@ -830,10 +820,9 @@ theorem fract_add_nat (a : α) (m : ℕ) : fract (a + m) = fract a := by
 @[simp]
 theorem fract_add_one (a : α) : fract (a + 1) = fract a := mod_cast fract_add_nat a 1
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem fract_add_ofNat (a : α) (n : ℕ) [n.AtLeastTwo] :
-    fract (a + (no_index (OfNat.ofNat n))) = fract a :=
+    fract (a + ofNat(n)) = fract a :=
   fract_add_nat a n
 
 @[simp]
@@ -845,10 +834,9 @@ theorem fract_nat_add (n : ℕ) (a : α) : fract (↑n + a) = fract a := by rw [
 @[simp]
 theorem fract_one_add (a : α) : fract (1 + a) = fract a := mod_cast fract_nat_add 1 a
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem fract_ofNat_add (n : ℕ) [n.AtLeastTwo] (a : α) :
-    fract ((no_index (OfNat.ofNat n)) + a) = fract a :=
+    fract (ofNat(n) + a) = fract a :=
   fract_nat_add n a
 
 @[simp]
@@ -864,10 +852,9 @@ theorem fract_sub_nat (a : α) (n : ℕ) : fract (a - n) = fract a := by
 @[simp]
 theorem fract_sub_one (a : α) : fract (a - 1) = fract a := mod_cast fract_sub_nat a 1
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem fract_sub_ofNat (a : α) (n : ℕ) [n.AtLeastTwo] :
-    fract (a - (no_index (OfNat.ofNat n))) = fract a :=
+    fract (a - ofNat(n)) = fract a :=
   fract_sub_nat a n
 
 -- Was a duplicate lemma under a bad name
@@ -921,10 +908,9 @@ theorem fract_intCast (z : ℤ) : fract (z : α) = 0 := by
 @[simp]
 theorem fract_natCast (n : ℕ) : fract (n : α) = 0 := by simp [fract]
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem fract_ofNat (n : ℕ) [n.AtLeastTwo] :
-    fract ((no_index (OfNat.ofNat n)) : α) = 0 :=
+    fract (ofNat(n) : α) = 0 :=
   fract_natCast n
 
 theorem fract_floor (a : α) : fract (⌊a⌋ : α) = 0 :=
@@ -1122,9 +1108,8 @@ theorem ceil_intCast (z : ℤ) : ⌈(z : α)⌉ = z :=
 theorem ceil_natCast (n : ℕ) : ⌈(n : α)⌉ = n :=
   eq_of_forall_ge_iff fun a => by rw [ceil_le, ← cast_natCast, cast_le]
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
-theorem ceil_ofNat (n : ℕ) [n.AtLeastTwo] : ⌈(no_index (OfNat.ofNat n : α))⌉ = n := ceil_natCast n
+theorem ceil_ofNat (n : ℕ) [n.AtLeastTwo] : ⌈(ofNat(n) : α)⌉ = ofNat(n) := ceil_natCast n
 
 theorem ceil_mono : Monotone (ceil : α → ℤ) :=
   gc_ceil_coe.monotone_l
@@ -1143,10 +1128,9 @@ theorem ceil_add_one (a : α) : ⌈a + 1⌉ = ⌈a⌉ + 1 := by
   -- Porting note: broken `convert ceil_add_int a (1 : ℤ)`
   rw [← ceil_add_int a (1 : ℤ), cast_one]
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem ceil_add_ofNat (a : α) (n : ℕ) [n.AtLeastTwo] :
-    ⌈a + (no_index (OfNat.ofNat n))⌉ = ⌈a⌉ + OfNat.ofNat n :=
+    ⌈a + ofNat(n)⌉ = ⌈a⌉ + ofNat(n) :=
   ceil_add_nat a n
 
 @[simp]
@@ -1162,10 +1146,9 @@ theorem ceil_sub_nat (a : α) (n : ℕ) : ⌈a - n⌉ = ⌈a⌉ - n := by
 theorem ceil_sub_one (a : α) : ⌈a - 1⌉ = ⌈a⌉ - 1 := by
   rw [eq_sub_iff_add_eq, ← ceil_add_one, sub_add_cancel]
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem ceil_sub_ofNat (a : α) (n : ℕ) [n.AtLeastTwo] :
-    ⌈a - (no_index (OfNat.ofNat n))⌉ = ⌈a⌉ - OfNat.ofNat n :=
+    ⌈a - ofNat(n)⌉ = ⌈a⌉ - ofNat(n) :=
   ceil_sub_nat a n
 
 @[bound]
@@ -1362,9 +1345,8 @@ theorem round_one : round (1 : α) = 1 := by simp [round]
 @[simp]
 theorem round_natCast (n : ℕ) : round (n : α) = n := by simp [round]
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
-theorem round_ofNat (n : ℕ) [n.AtLeastTwo] : round (no_index (OfNat.ofNat n : α)) = n :=
+theorem round_ofNat (n : ℕ) [n.AtLeastTwo] : round (ofNat(n) : α) = ofNat(n) :=
   round_natCast n
 
 @[simp]
@@ -1394,20 +1376,18 @@ theorem round_sub_one (a : α) : round (a - 1) = round a - 1 := by
 theorem round_add_nat (x : α) (y : ℕ) : round (x + y) = round x + y :=
   mod_cast round_add_int x y
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem round_add_ofNat (x : α) (n : ℕ) [n.AtLeastTwo] :
-    round (x + (no_index (OfNat.ofNat n))) = round x + OfNat.ofNat n :=
+    round (x + ofNat(n)) = round x + ofNat(n) :=
   round_add_nat x n
 
 @[simp]
 theorem round_sub_nat (x : α) (y : ℕ) : round (x - y) = round x - y :=
   mod_cast round_sub_int x y
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem round_sub_ofNat (x : α) (n : ℕ) [n.AtLeastTwo] :
-    round (x - (no_index (OfNat.ofNat n))) = round x - OfNat.ofNat n :=
+    round (x - ofNat(n)) = round x - ofNat(n) :=
   round_sub_nat x n
 
 @[simp]
@@ -1418,10 +1398,9 @@ theorem round_int_add (x : α) (y : ℤ) : round ((y : α) + x) = y + round x :=
 theorem round_nat_add (x : α) (y : ℕ) : round ((y : α) + x) = y + round x := by
   rw [add_comm, round_add_nat, add_comm]
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem round_ofNat_add (n : ℕ) [n.AtLeastTwo] (x : α) :
-    round ((no_index (OfNat.ofNat n)) + x) = OfNat.ofNat n + round x :=
+    round (ofNat(n) + x) = ofNat(n) + round x :=
   round_nat_add x n
 
 theorem abs_sub_round_eq_min (x : α) : |x - round x| = min (fract x) (1 - fract x) := by
diff --git a/Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean b/Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
index 3d47f485ab7e98..b9bc99747bd14c 100644
--- a/Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
+++ b/Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
@@ -324,31 +324,30 @@ instance addMonoidWithOne : AddMonoidWithOne (WithTop α) :=
 @[deprecated (since := "2024-04-05")] alias nat_ne_top := natCast_ne_top
 @[deprecated (since := "2024-04-05")] alias top_ne_nat := top_ne_natCast
 
--- See note [no_index around OfNat.ofNat]
 @[simp] lemma coe_ofNat (n : ℕ) [n.AtLeastTwo] :
-    (no_index (OfNat.ofNat n : α) : WithTop α) = OfNat.ofNat n := rfl
+    ((ofNat(n) : α) : WithTop α) = ofNat(n) := rfl
 @[simp] lemma coe_eq_ofNat (n : ℕ) [n.AtLeastTwo] (m : α) :
-    (m : WithTop α) = no_index (OfNat.ofNat n) ↔ m = OfNat.ofNat n :=
+    (m : WithTop α) = ofNat(n) ↔ m = ofNat(n) :=
   coe_eq_coe
 @[simp] lemma ofNat_eq_coe (n : ℕ) [n.AtLeastTwo] (m : α) :
-    no_index (OfNat.ofNat n) = (m : WithTop α) ↔ OfNat.ofNat n = m :=
+    ofNat(n) = (m : WithTop α) ↔ ofNat(n) = m :=
   coe_eq_coe
-@[simp] lemma ofNat_ne_top (n : ℕ) [n.AtLeastTwo] : no_index (OfNat.ofNat n : WithTop α) ≠ ⊤ :=
+@[simp] lemma ofNat_ne_top (n : ℕ) [n.AtLeastTwo] : (ofNat(n) : WithTop α) ≠ ⊤ :=
   natCast_ne_top n
-@[simp] lemma top_ne_ofNat (n : ℕ) [n.AtLeastTwo] : (⊤ : WithTop α) ≠ no_index (OfNat.ofNat n) :=
+@[simp] lemma top_ne_ofNat (n : ℕ) [n.AtLeastTwo] : (⊤ : WithTop α) ≠ ofNat(n) :=
   top_ne_natCast n
 
 @[simp] lemma map_ofNat {f : α → β} (n : ℕ) [n.AtLeastTwo] :
-    WithTop.map f (no_index (OfNat.ofNat n : WithTop α)) = f (OfNat.ofNat n) := map_coe f n
+    WithTop.map f (ofNat(n) : WithTop α) = f (ofNat(n)) := map_coe f n
 
 @[simp] lemma map_natCast {f : α → β} (n : ℕ) :
     WithTop.map f (n : WithTop α) = f n := map_coe f n
 
 lemma map_eq_ofNat_iff {f : β → α} {n : ℕ} [n.AtLeastTwo] {a : WithTop β} :
-    a.map f = OfNat.ofNat n ↔ ∃ x, a = .some x ∧ f x = n := map_eq_some_iff
+    a.map f = ofNat(n) ↔ ∃ x, a = .some x ∧ f x = n := map_eq_some_iff
 
 lemma ofNat_eq_map_iff {f : β → α} {n : ℕ} [n.AtLeastTwo] {a : WithTop β} :
-    OfNat.ofNat n = a.map f ↔ ∃ x, a = .some x ∧ f x = n := some_eq_map_iff
+    ofNat(n) = a.map f ↔ ∃ x, a = .some x ∧ f x = n := some_eq_map_iff
 
 lemma map_eq_natCast_iff {f : β → α} {n : ℕ} {a : WithTop β} :
     a.map f = n ↔ ∃ x, a = .some x ∧ f x = n := map_eq_some_iff
@@ -533,31 +532,30 @@ instance addMonoidWithOne : AddMonoidWithOne (WithBot α) := WithTop.addMonoidWi
 @[deprecated (since := "2024-04-05")] alias nat_ne_bot := natCast_ne_bot
 @[deprecated (since := "2024-04-05")] alias bot_ne_nat := bot_ne_natCast
 
--- See note [no_index around OfNat.ofNat]
 @[simp] lemma coe_ofNat (n : ℕ) [n.AtLeastTwo] :
-    (no_index (OfNat.ofNat n : α) : WithBot α) = OfNat.ofNat n := rfl
+    ((ofNat(n) : α) : WithBot α) = ofNat(n) := rfl
 @[simp] lemma coe_eq_ofNat (n : ℕ) [n.AtLeastTwo] (m : α) :
-    (m : WithBot α) = no_index (OfNat.ofNat n) ↔ m = OfNat.ofNat n :=
+    (m : WithBot α) = ofNat(n) ↔ m = ofNat(n) :=
   coe_eq_coe
 @[simp] lemma ofNat_eq_coe (n : ℕ) [n.AtLeastTwo] (m : α) :
-    no_index (OfNat.ofNat n) = (m : WithBot α) ↔ OfNat.ofNat n = m :=
+    ofNat(n) = (m : WithBot α) ↔ ofNat(n) = m :=
   coe_eq_coe
-@[simp] lemma ofNat_ne_bot (n : ℕ) [n.AtLeastTwo] : no_index (OfNat.ofNat n : WithBot α) ≠ ⊥ :=
+@[simp] lemma ofNat_ne_bot (n : ℕ) [n.AtLeastTwo] : (ofNat(n) : WithBot α) ≠ ⊥ :=
   natCast_ne_bot n
-@[simp] lemma bot_ne_ofNat (n : ℕ) [n.AtLeastTwo] : (⊥ : WithBot α) ≠ no_index (OfNat.ofNat n) :=
+@[simp] lemma bot_ne_ofNat (n : ℕ) [n.AtLeastTwo] : (⊥ : WithBot α) ≠ ofNat(n) :=
   bot_ne_natCast n
 
 @[simp] lemma map_ofNat {f : α → β} (n : ℕ) [n.AtLeastTwo] :
-    WithBot.map f (no_index (OfNat.ofNat n : WithBot α)) = f (OfNat.ofNat n) := map_coe f n
+    WithBot.map f (ofNat(n) : WithBot α) = f ofNat(n) := map_coe f n
 
 @[simp] lemma map_natCast {f : α → β} (n : ℕ) :
     WithBot.map f (n : WithBot α) = f n := map_coe f n
 
 lemma map_eq_ofNat_iff {f : β → α} {n : ℕ} [n.AtLeastTwo] {a : WithBot β} :
-    a.map f = OfNat.ofNat n ↔ ∃ x, a = .some x ∧ f x = n := map_eq_some_iff
+    a.map f = ofNat(n) ↔ ∃ x, a = .some x ∧ f x = n := map_eq_some_iff
 
 lemma ofNat_eq_map_iff {f : β → α} {n : ℕ} [n.AtLeastTwo] {a : WithBot β} :
-    OfNat.ofNat n = a.map f ↔ ∃ x, a = .some x ∧ f x = n := some_eq_map_iff
+    ofNat(n) = a.map f ↔ ∃ x, a = .some x ∧ f x = n := some_eq_map_iff
 
 lemma map_eq_natCast_iff {f : β → α} {n : ℕ} {a : WithBot β} :
     a.map f = n ↔ ∃ x, a = .some x ∧ f x = n := map_eq_some_iff
diff --git a/Mathlib/Algebra/Polynomial/Basic.lean b/Mathlib/Algebra/Polynomial/Basic.lean
index a5757859e7bfaf..d88f59b1d6cca6 100644
--- a/Mathlib/Algebra/Polynomial/Basic.lean
+++ b/Mathlib/Algebra/Polynomial/Basic.lean
@@ -667,16 +667,14 @@ theorem coeff_natCast_ite : (Nat.cast m : R[X]).coeff n = ite (n = 0) m 0 := by
 @[deprecated (since := "2024-04-17")]
 alias coeff_nat_cast_ite := coeff_natCast_ite
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem coeff_ofNat_zero (a : ℕ) [a.AtLeastTwo] :
-    coeff (no_index (OfNat.ofNat a : R[X])) 0 = OfNat.ofNat a :=
+    coeff (ofNat(a) : R[X]) 0 = ofNat(a) :=
   coeff_monomial
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem coeff_ofNat_succ (a n : ℕ) [h : a.AtLeastTwo] :
-    coeff (no_index (OfNat.ofNat a : R[X])) (n + 1) = 0 := by
+    coeff (ofNat(a) : R[X]) (n + 1) = 0 := by
   rw [← Nat.cast_ofNat]
   simp [-Nat.cast_ofNat]
 
diff --git a/Mathlib/Algebra/Polynomial/Coeff.lean b/Mathlib/Algebra/Polynomial/Coeff.lean
index 1997d5ce972f09..de59da07ebfc23 100644
--- a/Mathlib/Algebra/Polynomial/Coeff.lean
+++ b/Mathlib/Algebra/Polynomial/Coeff.lean
@@ -172,13 +172,11 @@ theorem coeff_mul_C (p : R[X]) (n : ℕ) (a : R) : coeff (p * C a) n = coeff p n
 @[simp] lemma coeff_natCast_mul {a k : ℕ} :
   coeff ((a : R[X]) * p) k = a * coeff p k := coeff_C_mul _
 
--- See note [no_index around OfNat.ofNat]
 @[simp] lemma coeff_mul_ofNat {a k : ℕ} [Nat.AtLeastTwo a] :
-  coeff (p * (no_index (OfNat.ofNat a) : R[X])) k = coeff p k * OfNat.ofNat a := coeff_mul_C _ _ _
+  coeff (p * (ofNat(a) : R[X])) k = coeff p k * ofNat(a) := coeff_mul_C _ _ _
 
--- See note [no_index around OfNat.ofNat]
 @[simp] lemma coeff_ofNat_mul {a k : ℕ} [Nat.AtLeastTwo a] :
-  coeff ((no_index (OfNat.ofNat a) : R[X]) * p) k = OfNat.ofNat a * coeff p k := coeff_C_mul _
+  coeff ((ofNat(a) : R[X]) * p) k = ofNat(a) * coeff p k := coeff_C_mul _
 
 @[simp] lemma coeff_mul_intCast [Ring S] {p : S[X]} {a : ℤ} {k : ℕ} :
   coeff (p * (a : S[X])) k = coeff p k * (↑a : S) := coeff_mul_C _ _ _
diff --git a/Mathlib/Algebra/Polynomial/Degree/Definitions.lean b/Mathlib/Algebra/Polynomial/Degree/Definitions.lean
index 3dabffa2ed70da..a7f16ee7d9aa66 100644
--- a/Mathlib/Algebra/Polynomial/Degree/Definitions.lean
+++ b/Mathlib/Algebra/Polynomial/Degree/Definitions.lean
@@ -177,10 +177,9 @@ theorem natDegree_natCast (n : ℕ) : natDegree (n : R[X]) = 0 := by
 @[deprecated (since := "2024-04-17")]
 alias natDegree_nat_cast := natDegree_natCast
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem natDegree_ofNat (n : ℕ) [Nat.AtLeastTwo n] :
-    natDegree (no_index (OfNat.ofNat n : R[X])) = 0 :=
+    natDegree (ofNat(n) : R[X]) = 0 :=
   natDegree_natCast _
 
 theorem degree_natCast_le (n : ℕ) : degree (n : R[X]) ≤ 0 := degree_le_of_natDegree_le (by simp)
diff --git a/Mathlib/Algebra/Ring/Center.lean b/Mathlib/Algebra/Ring/Center.lean
index 73f4fbcbad95f0..828c1c41ecadbc 100644
--- a/Mathlib/Algebra/Ring/Center.lean
+++ b/Mathlib/Algebra/Ring/Center.lean
@@ -37,10 +37,9 @@ theorem natCast_mem_center [NonAssocSemiring M] (n : ℕ) : (n : M) ∈ Set.cent
     | zero => rw [Nat.cast_zero, mul_zero, mul_zero, mul_zero]
     | succ n ihn => rw [Nat.cast_succ, mul_add, ihn, mul_add, mul_add, mul_one, mul_one]
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem ofNat_mem_center [NonAssocSemiring M] (n : ℕ) [n.AtLeastTwo] :
-    (no_index (OfNat.ofNat n)) ∈ Set.center M :=
+    ofNat(n) ∈ Set.center M :=
   natCast_mem_center M n
 
 @[simp]
diff --git a/Mathlib/Algebra/Ring/Int/Parity.lean b/Mathlib/Algebra/Ring/Int/Parity.lean
index 8a6ea4b3ac36dd..cd9699824a4986 100644
--- a/Mathlib/Algebra/Ring/Int/Parity.lean
+++ b/Mathlib/Algebra/Ring/Int/Parity.lean
@@ -154,10 +154,9 @@ theorem isSquare_natCast_iff {n : ℕ} : IsSquare (n : ℤ) ↔ IsSquare n := by
   · exact ⟨x.natAbs, (natAbs_mul_natAbs_eq h.symm).symm⟩
   · exact ⟨x, mod_cast h⟩
 
--- 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(n) : ℕ) :=
   isSquare_natCast_iff
 
 end Int
diff --git a/Mathlib/Data/Fin/Basic.lean b/Mathlib/Data/Fin/Basic.lean
index 4fcd6469077693..11123477cd16a4 100644
--- a/Mathlib/Data/Fin/Basic.lean
+++ b/Mathlib/Data/Fin/Basic.lean
@@ -1513,9 +1513,8 @@ theorem coe_natCast_eq_mod (m n : ℕ) [NeZero m] :
     ((n : Fin m) : ℕ) = n % m :=
   rfl
 
--- See note [no_index around OfNat.ofNat]
 theorem coe_ofNat_eq_mod (m n : ℕ) [NeZero m] :
-    ((no_index (OfNat.ofNat n) : Fin m) : ℕ) = OfNat.ofNat n % m :=
+    ((ofNat(n) : Fin m) : ℕ) = ofNat(n) % m :=
   rfl
 
 section Mul
diff --git a/Mathlib/Data/Int/Cast/Basic.lean b/Mathlib/Data/Int/Cast/Basic.lean
index 6885e5e943ea97..ade0aeafd71c28 100644
--- a/Mathlib/Data/Int/Cast/Basic.lean
+++ b/Mathlib/Data/Int/Cast/Basic.lean
@@ -60,10 +60,9 @@ theorem cast_natCast (n : ℕ) : ((n : ℤ) : R) = n :=
   AddGroupWithOne.intCast_ofNat _
 -- expected `n` to be implicit, and `HasLiftT`
 
--- See note [no_index around OfNat.ofNat]
 @[simp, norm_cast]
 theorem cast_ofNat (n : ℕ) [n.AtLeastTwo] :
-    ((no_index (OfNat.ofNat n) : ℤ) : R) = OfNat.ofNat n := by
+    ((ofNat(n) : ℤ) : R) = ofNat(n) := by
   simpa only [OfNat.ofNat] using AddGroupWithOne.intCast_ofNat (R := R) n
 
 @[simp, norm_cast]
diff --git a/Mathlib/Data/Int/Log.lean b/Mathlib/Data/Int/Log.lean
index 4d5f3c0e387221..a892892decb010 100644
--- a/Mathlib/Data/Int/Log.lean
+++ b/Mathlib/Data/Int/Log.lean
@@ -72,10 +72,9 @@ theorem log_natCast (b : ℕ) (n : ℕ) : log b (n : R) = Nat.log b n := by
   · rw [log_of_one_le_right, Nat.floor_natCast]
     simp
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem log_ofNat (b : ℕ) (n : ℕ) [n.AtLeastTwo] :
-    log b (no_index (OfNat.ofNat n : R)) = Nat.log b (OfNat.ofNat n) :=
+    log b (ofNat(n) : R) = Nat.log b ofNat(n) :=
   log_natCast b n
 
 theorem log_of_left_le_one {b : ℕ} (hb : b ≤ 1) (r : R) : log b r = 0 := by
@@ -221,10 +220,9 @@ theorem clog_natCast (b : ℕ) (n : ℕ) : clog b (n : R) = Nat.clog b n := by
   · simp [clog_of_right_le_one]
   · rw [clog_of_one_le_right, (Nat.ceil_eq_iff (Nat.succ_ne_zero n)).mpr] <;> simp
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem clog_ofNat (b : ℕ) (n : ℕ) [n.AtLeastTwo] :
-    clog b (no_index (OfNat.ofNat n : R)) = Nat.clog b (OfNat.ofNat n) :=
+    clog b (ofNat(n) : R) = Nat.clog b ofNat(n) :=
   clog_natCast b n
 
 theorem clog_of_left_le_one {b : ℕ} (hb : b ≤ 1) (r : R) : clog b r = 0 := by
diff --git a/Mathlib/Data/Int/Sqrt.lean b/Mathlib/Data/Int/Sqrt.lean
index 1c6db061ba8f78..f8cccdb7928fe2 100644
--- a/Mathlib/Data/Int/Sqrt.lean
+++ b/Mathlib/Data/Int/Sqrt.lean
@@ -36,9 +36,8 @@ theorem sqrt_nonneg (n : ℤ) : 0 ≤ sqrt n :=
 @[simp, norm_cast]
 theorem sqrt_natCast (n : ℕ) : Int.sqrt (n : ℤ) = Nat.sqrt n := by rw [sqrt, toNat_ofNat]
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
-theorem sqrt_ofNat (n : ℕ) : Int.sqrt (no_index (OfNat.ofNat n) : ℤ) = Nat.sqrt (OfNat.ofNat n) :=
+theorem sqrt_ofNat (n : ℕ) : Int.sqrt ofNat(n) = Nat.sqrt ofNat(n) :=
   sqrt_natCast _
 
 end Int
diff --git a/Mathlib/Data/Nat/Cast/Defs.lean b/Mathlib/Data/Nat/Cast/Defs.lean
index 5575f08cbd7e73..dce8ade4fbffbd 100644
--- a/Mathlib/Data/Nat/Cast/Defs.lean
+++ b/Mathlib/Data/Nat/Cast/Defs.lean
@@ -5,6 +5,7 @@ Authors: Mario Carneiro, Gabriel Ebner
 -/
 import Mathlib.Algebra.Group.Defs
 import Mathlib.Tactic.SplitIfs
+import Mathlib.Tactic.OfNat
 
 /-!
 # Cast of natural numbers
@@ -62,11 +63,14 @@ library_note "no_index around OfNat.ofNat"
 When writing lemmas about `OfNat.ofNat` that assume `Nat.AtLeastTwo`, the term needs to be wrapped
 in `no_index` so as not to confuse `simp`, as `no_index (OfNat.ofNat n)`.
 
+Rather than referencing this library note, use `ofNat(n)` as a shorthand for
+`no_index (OfNat.ofNat n)`.
+
 Some discussion is [on Zulip here](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.E2.9C.94.20Polynomial.2Ecoeff.20example/near/395438147).
 -/
 
 @[simp, norm_cast] theorem Nat.cast_ofNat {n : ℕ} [NatCast R] [Nat.AtLeastTwo n] :
-  (Nat.cast (no_index (OfNat.ofNat n)) : R) = OfNat.ofNat n := rfl
+  (Nat.cast ofNat(n) : R) = ofNat(n) := rfl
 
 @[deprecated Nat.cast_ofNat (since := "2024-12-22")]
 theorem Nat.cast_eq_ofNat {n : ℕ} [NatCast R] [Nat.AtLeastTwo n] :
diff --git a/Mathlib/Data/Nat/Cast/Order/Ring.lean b/Mathlib/Data/Nat/Cast/Order/Ring.lean
index 693d3ef4c6797e..54269e96efeb05 100644
--- a/Mathlib/Data/Nat/Cast/Order/Ring.lean
+++ b/Mathlib/Data/Nat/Cast/Order/Ring.lean
@@ -30,10 +30,9 @@ theorem cast_nonneg {α} [OrderedSemiring α] (n : ℕ) : 0 ≤ (n : α) :=
   cast_nonneg' n
 
 /-- Specialisation of `Nat.ofNat_nonneg'`, which seems to be easier for Lean to use. -/
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem ofNat_nonneg {α} [OrderedSemiring α] (n : ℕ) [n.AtLeastTwo] :
-    0 ≤ (no_index (OfNat.ofNat n : α)) :=
+    0 ≤ (ofNat(n) : α) :=
   ofNat_nonneg' n
 
 @[simp, norm_cast]
@@ -53,16 +52,14 @@ variable [NeZero (1 : α)]
 theorem cast_pos {α} [OrderedSemiring α] [Nontrivial α] {n : ℕ} : (0 : α) < n ↔ 0 < n := cast_pos'
 
 /-- See also `Nat.ofNat_pos`, specialised for an `OrderedSemiring`. -/
--- See note [no_index around OfNat.ofNat]
 @[simp low]
-theorem ofNat_pos' {n : ℕ} [n.AtLeastTwo] : 0 < (no_index (OfNat.ofNat n : α)) :=
+theorem ofNat_pos' {n : ℕ} [n.AtLeastTwo] : 0 < (ofNat(n) : α) :=
   cast_pos'.mpr (NeZero.pos n)
 
 /-- Specialisation of `Nat.ofNat_pos'`, which seems to be easier for Lean to use. -/
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem ofNat_pos {α} [OrderedSemiring α] [Nontrivial α] {n : ℕ} [n.AtLeastTwo] :
-    0 < (no_index (OfNat.ofNat n : α)) :=
+    0 < (ofNat(n) : α) :=
   ofNat_pos'
 
 end Nontrivial
@@ -84,10 +81,9 @@ theorem cast_tsub [CanonicallyOrderedCommSemiring α] [Sub α] [OrderedSub α]
 theorem abs_cast [LinearOrderedRing α] (a : ℕ) : |(a : α)| = a :=
   abs_of_nonneg (cast_nonneg a)
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem abs_ofNat [LinearOrderedRing α] (n : ℕ) [n.AtLeastTwo] :
-    |(no_index (OfNat.ofNat n : α))| = OfNat.ofNat n :=
+    |(ofNat(n) : α)| = ofNat(n) :=
   abs_cast n
 
 lemma mul_le_pow {a : ℕ} (ha : a ≠ 1) (b : ℕ) :
diff --git a/Mathlib/Data/Nat/Cast/Prod.lean b/Mathlib/Data/Nat/Cast/Prod.lean
index 9903b6c4873ac4..1f38821eeb1df6 100644
--- a/Mathlib/Data/Nat/Cast/Prod.lean
+++ b/Mathlib/Data/Nat/Cast/Prod.lean
@@ -26,19 +26,17 @@ instance instAddMonoidWithOne : AddMonoidWithOne (α × β) :=
 @[simp]
 theorem fst_natCast (n : ℕ) : (n : α × β).fst = n := by induction n <;> simp [*]
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem fst_ofNat (n : ℕ) [n.AtLeastTwo] :
-    (no_index (OfNat.ofNat n : α × β)).1 = (OfNat.ofNat n : α) :=
+    (ofNat(n) : α × β).1 = (ofNat(n) : α) :=
   rfl
 
 @[simp]
 theorem snd_natCast (n : ℕ) : (n : α × β).snd = n := by induction n <;> simp [*]
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem snd_ofNat (n : ℕ) [n.AtLeastTwo] :
-    (no_index (OfNat.ofNat n : α × β)).2 = (OfNat.ofNat n : β) :=
+    (ofNat(n) : α × β).2 = (ofNat(n) : β) :=
   rfl
 
 end Prod
diff --git a/Mathlib/Data/Nat/Cast/Synonym.lean b/Mathlib/Data/Nat/Cast/Synonym.lean
index 075d62d0d87cf3..11b1f4d3b233ae 100644
--- a/Mathlib/Data/Nat/Cast/Synonym.lean
+++ b/Mathlib/Data/Nat/Cast/Synonym.lean
@@ -42,20 +42,18 @@ instance [h : AddCommMonoidWithOne α] : AddCommMonoidWithOne αᵒᵈ :=
 theorem toDual_natCast [NatCast α] (n : ℕ) : toDual (n : α) = n :=
   rfl
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem toDual_ofNat [NatCast α] (n : ℕ) [n.AtLeastTwo] :
-    (toDual (no_index (OfNat.ofNat n : α))) = OfNat.ofNat n :=
+    (toDual (ofNat(n) : α)) = ofNat(n) :=
   rfl
 
 @[simp]
 theorem ofDual_natCast [NatCast α] (n : ℕ) : (ofDual n : α) = n :=
   rfl
 
--- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem ofDual_ofNat [NatCast α] (n : ℕ) [n.AtLeastTwo] :
-    (ofDual (no_index (OfNat.ofNat n : αᵒᵈ))) = OfNat.ofNat n :=
+    (ofDual (ofNat(n) : αᵒᵈ)) = ofNat(n) :=
   rfl
 
 /-! ### Lexicographic order -/
diff --git a/Mathlib/Data/Rat/Cast/Defs.lean b/Mathlib/Data/Rat/Cast/Defs.lean
index 4b9f06c0c9542e..a5fc916543c003 100644
--- a/Mathlib/Data/Rat/Cast/Defs.lean
+++ b/Mathlib/Data/Rat/Cast/Defs.lean
@@ -33,9 +33,8 @@ variable [DivisionSemiring α] {q r : ℚ≥0}
 
 @[simp, norm_cast] lemma cast_natCast (n : ℕ) : ((n : ℚ≥0) : α) = n := by simp [cast_def]
 
--- See note [no_index around OfNat.ofNat]
 @[simp, norm_cast] lemma cast_ofNat (n : ℕ) [n.AtLeastTwo] :
-    no_index (OfNat.ofNat n : ℚ≥0) = (OfNat.ofNat n : α) := cast_natCast _
+    (ofNat(n) : ℚ≥0) = (ofNat(n) : α) := cast_natCast _
 
 @[simp, norm_cast] lemma cast_zero : ((0 : ℚ≥0) : α) = 0 := (cast_natCast _).trans Nat.cast_zero
 @[simp, norm_cast] lemma cast_one : ((1 : ℚ≥0) : α) = 1 := (cast_natCast _).trans Nat.cast_one
@@ -118,9 +117,8 @@ theorem cast_natCast (n : ℕ) : ((n : ℚ) : α) = n := by
 @[deprecated (since := "2024-03-21")] alias cast_coe_int := cast_intCast
 @[deprecated (since := "2024-03-21")] alias cast_coe_nat := cast_natCast
 
--- See note [no_index around OfNat.ofNat]
 @[simp, norm_cast] lemma cast_ofNat (n : ℕ) [n.AtLeastTwo] :
-    ((no_index (OfNat.ofNat n : ℚ)) : α) = (OfNat.ofNat n : α) := by
+    ((ofNat(n) : ℚ) : α) = (ofNat(n) : α) := by
   simp [cast_def]
 
 @[simp, norm_cast]
diff --git a/Mathlib/Data/Rat/Defs.lean b/Mathlib/Data/Rat/Defs.lean
index 4c5c728579ffa8..cb77cd4efc0c39 100644
--- a/Mathlib/Data/Rat/Defs.lean
+++ b/Mathlib/Data/Rat/Defs.lean
@@ -51,9 +51,8 @@ theorem ofInt_eq_cast (n : ℤ) : ofInt n = Int.cast n :=
   rfl
 
 -- TODO: Replace `Rat.ofNat_num`/`Rat.ofNat_den` in Batteries
--- See note [no_index around OfNat.ofNat]
-@[simp] lemma num_ofNat (n : ℕ) : num (no_index (OfNat.ofNat n)) = OfNat.ofNat n := rfl
-@[simp] lemma den_ofNat (n : ℕ) : den (no_index (OfNat.ofNat n)) = 1 := rfl
+@[simp] lemma num_ofNat (n : ℕ) : num ofNat(n) = ofNat(n) := rfl
+@[simp] lemma den_ofNat (n : ℕ) : den ofNat(n) = 1 := rfl
 
 @[simp, norm_cast] lemma num_natCast (n : ℕ) : num n = n := rfl
 
@@ -386,11 +385,11 @@ theorem den_neg_eq_den (q : ℚ) : (-q).den = q.den :=
 theorem num_neg_eq_neg_num (q : ℚ) : (-q).num = -q.num :=
   rfl
 
-@[simp]
+-- Not `@[simp]` as `num_ofNat` is stronger.
 theorem num_zero : Rat.num 0 = 0 :=
   rfl
 
-@[simp]
+-- Not `@[simp]` as `den_ofNat` is stronger.
 theorem den_zero : Rat.den 0 = 1 :=
   rfl
 
@@ -399,7 +398,7 @@ lemma zero_of_num_zero {q : ℚ} (hq : q.num = 0) : q = 0 := by simpa [hq] using
 theorem zero_iff_num_zero {q : ℚ} : q = 0 ↔ q.num = 0 :=
   ⟨fun _ => by simp [*], zero_of_num_zero⟩
 
-@[simp]
+-- `Not `@[simp]` as `num_ofNat` is stronger.
 theorem num_one : (1 : ℚ).num = 1 :=
   rfl
 
diff --git a/Mathlib/Lean/Expr/Basic.lean b/Mathlib/Lean/Expr/Basic.lean
index 57caa17facbf9a..4606e2f6b56925 100644
--- a/Mathlib/Lean/Expr/Basic.lean
+++ b/Mathlib/Lean/Expr/Basic.lean
@@ -262,6 +262,7 @@ section recognizers
 partial def numeral? (e : Expr) : Option Nat :=
   if let some n := e.rawNatLit? then n
   else
+    let e := e.consumeMData -- `OfNat` numerals may have `no_index` around them from `ofNat()`
     let f := e.getAppFn
     if !f.isConst then none
     else
diff --git a/Mathlib/NumberTheory/Transcendental/Liouville/Residual.lean b/Mathlib/NumberTheory/Transcendental/Liouville/Residual.lean
index 3703485af27371..9e0eff961d50c8 100644
--- a/Mathlib/NumberTheory/Transcendental/Liouville/Residual.lean
+++ b/Mathlib/NumberTheory/Transcendental/Liouville/Residual.lean
@@ -61,7 +61,12 @@ theorem eventually_residual_liouville : ∀ᶠ x in residual ℝ, Liouville x :=
     refine fun n => ⟨r.num * 2, r.den * 2, ?_, ?_⟩
     · have := r.pos; omega
     · convert @mem_ball_self ℝ _ (r : ℝ) _ _
-      · push_cast; norm_cast; simp [Rat.divInt_mul_right (two_ne_zero), Rat.mkRat_self]
+      · push_cast
+        -- Workaround for https://github.com/leanprover/lean4/pull/6438; this eliminates an
+        -- `Expr.mdata` that would cause `norm_cast` to skip a numeral.
+        rw [Eq.refl (2 : ℝ)]
+        norm_cast
+        simp [Rat.divInt_mul_right (two_ne_zero), Rat.mkRat_self]
       · refine one_div_pos.2 (pow_pos (Int.cast_pos.2 ?_) _)
         exact mul_pos (Int.natCast_pos.2 r.pos) zero_lt_two
 
diff --git a/Mathlib/Tactic.lean b/Mathlib/Tactic.lean
index b9bfe92da053bb..7938e6809683b7 100644
--- a/Mathlib/Tactic.lean
+++ b/Mathlib/Tactic.lean
@@ -188,6 +188,7 @@ import Mathlib.Tactic.NormNum.Prime
 import Mathlib.Tactic.NormNum.Result
 import Mathlib.Tactic.NthRewrite
 import Mathlib.Tactic.Observe
+import Mathlib.Tactic.OfNat
 import Mathlib.Tactic.PPWithUniv
 import Mathlib.Tactic.Peel
 import Mathlib.Tactic.Polyrith
diff --git a/Mathlib/Tactic/Common.lean b/Mathlib/Tactic/Common.lean
index 94a9e57234ef39..b59d768f32d0c3 100644
--- a/Mathlib/Tactic/Common.lean
+++ b/Mathlib/Tactic/Common.lean
@@ -72,6 +72,7 @@ import Mathlib.Tactic.MkIffOfInductiveProp
 -- import Mathlib.Tactic.NormNum.Basic
 import Mathlib.Tactic.NthRewrite
 import Mathlib.Tactic.Observe
+import Mathlib.Tactic.OfNat
 -- `positivity` imports `Data.Nat.Factorial.Basic`, but hopefully this can be rearranged.
 -- import Mathlib.Tactic.Positivity
 import Mathlib.Tactic.ProjectionNotation
diff --git a/Mathlib/Tactic/OfNat.lean b/Mathlib/Tactic/OfNat.lean
new file mode 100644
index 00000000000000..fb3dbeebb64bd9
--- /dev/null
+++ b/Mathlib/Tactic/OfNat.lean
@@ -0,0 +1,18 @@
+/-
+Copyright (c) 2024 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+import Mathlib.Init
+
+/-! # The `ofNat()` macro -/
+
+/--
+This macro is a shorthand for `OfNat.ofNat` combined with `no_index`.
+
+When writing lemmas about `OfNat.ofNat`, the term needs to be wrapped
+in `no_index` so as not to confuse `simp`, as `no_index (OfNat.ofNat n)`.
+
+Some discussion is [on Zulip here](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.E2.9C.94.20Polynomial.2Ecoeff.20example/near/395438147).
+-/
+macro "ofNat(" n:term ")" : term => `(no_index (OfNat.ofNat $n))
diff --git a/Mathlib/Tactic/Rify.lean b/Mathlib/Tactic/Rify.lean
index b8538585d92da7..77801b38118d53 100644
--- a/Mathlib/Tactic/Rify.lean
+++ b/Mathlib/Tactic/Rify.lean
@@ -82,8 +82,7 @@ macro_rules
 @[deprecated (since := "2024-04-17")]
 alias rat_cast_ne := ratCast_ne
 
--- See note [no_index around OfNat.ofNat]
 @[rify_simps] lemma ofNat_rat_real (a : ℕ) [a.AtLeastTwo] :
-    ((no_index (OfNat.ofNat a : ℚ)) : ℝ) = (OfNat.ofNat a : ℝ) := rfl
+    ((ofNat(a) : ℚ) : ℝ) = (ofNat(a) : ℝ) := rfl
 
 end Mathlib.Tactic.Rify
diff --git a/Mathlib/Topology/ContinuousMap/Bounded/Basic.lean b/Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
index ab3605b44b21f1..c32fd5163a6e07 100644
--- a/Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
+++ b/Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
@@ -1220,10 +1220,9 @@ instance : NatCast (α →ᵇ R) :=
 @[simp, norm_cast]
 theorem coe_natCast (n : ℕ) : ((n : α →ᵇ R) : α → R) = n := rfl
 
--- See note [no_index around OfNat.ofNat]
 @[simp, norm_cast]
 theorem coe_ofNat (n : ℕ) [n.AtLeastTwo] :
-    ((no_index (OfNat.ofNat n) : α →ᵇ R) : α → R) = OfNat.ofNat n :=
+    ((ofNat(n) : α →ᵇ R) : α → R) = ofNat(n) :=
   rfl
 
 instance : IntCast (α →ᵇ R) :=
diff --git a/scripts/noshake.json b/scripts/noshake.json
index 22f216add93040..a45672285115cb 100644
--- a/scripts/noshake.json
+++ b/scripts/noshake.json
@@ -450,6 +450,7 @@
   "Mathlib.Algebra.Group.Units.Basic": ["Mathlib.Tactic.Subsingleton"],
   "Mathlib.Algebra.Group.Units": ["Mathlib.Tactic.Subsingleton"],
   "Mathlib.Algebra.Group.Pi.Basic": ["Batteries.Tactic.Classical"],
+  "Mathlib.Algebra.Group.Defs": ["Mathlib.Tactic.OfNat"],
   "Mathlib.Algebra.GeomSum": ["Mathlib.Algebra.Order.BigOperators.Ring.Finset"],
   "Mathlib.Algebra.Category.Ring.Basic":
   ["Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso"],