[Merged by Bors] - refactor: add an ofNat() elaborator

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) = 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

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`. -/

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
 
 /-!
@@ -902,9 +903,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

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

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)]

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]

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")]

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]
@@ -1362,9 +1359,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
@@ -1498,10 +1494,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]