chore: use ofNat more (#20546)

grunweg · grunweg · commit ceb6589394fc · 2025-01-10T18:19:02.000Z
When a theorem statement contains both ofNat and OfNat.ofNat, replace the latter by the former: as eric-wieser [says](#20521 (review)), these are mostly theorems that work forwards, but not backwards, with simp. Very much not exhaustive, there are perhaps 160 instances in mathlib remaining. Co-authored-by: grunweg <rothgami@math.hu-berlin.de>
diff --git a/Mathlib/Algebra/AddConstMap/Basic.lean b/Mathlib/Algebra/AddConstMap/Basic.lean
@@ -87,15 +87,15 @@ 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 + ofNat(n)) = f x + (OfNat.ofNat n : ℕ) • b :=
+    f (x + ofNat(n)) = f x + (ofNat(n) : ℕ) • b :=
   map_add_nat' f x n
 
 theorem map_add_nat [AddMonoidWithOne G] [AddMonoidWithOne H] [AddConstMapClass F G H 1 1]
     (f : F) (x : G) (n : ℕ) : f (x + n) = f x + n := by simp
 
 theorem map_add_ofNat [AddMonoidWithOne G] [AddMonoidWithOne H] [AddConstMapClass F G H 1 1]
     (f : F) (x : G) (n : ℕ) [n.AtLeastTwo] :
-    f (x + OfNat.ofNat n) = f x + OfNat.ofNat n := map_add_nat f x n
+    f (x + ofNat(n)) = f x + ofNat(n) := map_add_nat f x n
 
 @[scoped simp]
 theorem map_const [AddZeroClass G] [Add H] [AddConstMapClass F G H a b] (f : F) :
@@ -118,15 +118,15 @@ theorem map_nat' [AddMonoidWithOne G] [AddMonoid H] [AddConstMapClass F G H 1 b]
 
 theorem map_ofNat' [AddMonoidWithOne G] [AddMonoid H] [AddConstMapClass F G H 1 b]
     (f : F) (n : ℕ) [n.AtLeastTwo] :
-    f (OfNat.ofNat n) = f 0 + (OfNat.ofNat n : ℕ) • b :=
+    f (ofNat(n)) = f 0 + (ofNat(n) : ℕ) • b :=
   map_nat' f n
 
 theorem map_nat [AddMonoidWithOne G] [AddMonoidWithOne H] [AddConstMapClass F G H 1 1]
     (f : F) (n : ℕ) : f n = f 0 + n := by simp
 
 theorem map_ofNat [AddMonoidWithOne G] [AddMonoidWithOne H] [AddConstMapClass F G H 1 1]
     (f : F) (n : ℕ) [n.AtLeastTwo] :
-    f (OfNat.ofNat n) = f 0 + OfNat.ofNat n := map_nat f n
+    f ofNat(n) = f 0 + ofNat(n) := map_nat f n
 
 @[scoped simp]
 theorem map_const_add [AddCommSemigroup G] [Add H] [AddConstMapClass F G H a b]
@@ -148,15 +148,15 @@ theorem map_nat_add' [AddCommMonoidWithOne G] [AddMonoid H] [AddConstMapClass F
 
 theorem map_ofNat_add' [AddCommMonoidWithOne G] [AddMonoid H] [AddConstMapClass F G H 1 b]
     (f : F) (n : ℕ) [n.AtLeastTwo] (x : G) :
-    f (OfNat.ofNat n + x) = f x + OfNat.ofNat n • b :=
+    f (ofNat(n) + x) = f x + ofNat(n) • b :=
   map_nat_add' f n x
 
 theorem map_nat_add [AddCommMonoidWithOne G] [AddMonoidWithOne H] [AddConstMapClass F G H 1 1]
     (f : F) (n : ℕ) (x : G) : f (↑n + x) = f x + n := by simp
 
 theorem map_ofNat_add [AddCommMonoidWithOne G] [AddMonoidWithOne H] [AddConstMapClass F G H 1 1]
     (f : F) (n : ℕ) [n.AtLeastTwo] (x : G) :
-    f (OfNat.ofNat n + x) = f x + OfNat.ofNat n :=
+    f (ofNat(n) + x) = f x + ofNat(n) :=
   map_nat_add f n x
 
 @[scoped simp]
@@ -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 - ofNat(n)) = f x - OfNat.ofNat n • b :=
+    f (x - ofNat(n)) = f x - ofNat(n) • b :=
   map_sub_nat' f x n
 
 @[scoped simp]
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] :
-    (ofNat(n) : A 0) = (OfNat.ofNat n : R) := rfl
+    (ofNat(n) : A 0) = (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) :
-    (ofNat(n) : Module.End R M) m = OfNat.ofNat n • m := rfl
+    (ofNat(n) : Module.End R M) m = 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/Module/NatInt.lean b/Mathlib/Algebra/Module/NatInt.lean
@@ -103,7 +103,7 @@ lemma Nat.cast_smul_eq_nsmul (n : ℕ) (b : M) : (n : R) • b = n • b := by
 
 /-- `nsmul` is equal to any other module structure via a cast. -/
 lemma ofNat_smul_eq_nsmul (n : ℕ) [n.AtLeastTwo] (b : M) :
-    (ofNat(n) : R) • b = OfNat.ofNat n • b := Nat.cast_smul_eq_nsmul ..
+    (ofNat(n) : R) • b = 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/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 (ofNat(n) : WithBot α) = OfNat.ofNat n + 1 := succ_natCast n
+    succ (ofNat(n) : WithBot α) = ofNat(n) + 1 := succ_natCast n
 
 end WithBot
diff --git a/Mathlib/Algebra/Polynomial/Eval/Defs.lean b/Mathlib/Algebra/Polynomial/Eval/Defs.lean
@@ -104,7 +104,7 @@ alias eval₂_nat_cast := eval₂_natCast
 
 @[simp]
 lemma eval₂_ofNat {S : Type*} [Semiring S] (n : ℕ) [n.AtLeastTwo] (f : R →+* S) (a : S) :
-    (ofNat(n) : R[X]).eval₂ f a = OfNat.ofNat n := by
+    (ofNat(n) : R[X]).eval₂ f a = ofNat(n) := by
   simp [OfNat.ofNat]
 
 variable [Semiring T]
@@ -264,7 +264,7 @@ alias eval₂_at_nat_cast := eval₂_at_natCast
 
 @[simp]
 theorem eval₂_at_ofNat {S : Type*} [Semiring S] (f : R →+* S) (n : ℕ) [n.AtLeastTwo] :
-    p.eval₂ f ofNat(n) = f (p.eval (OfNat.ofNat n)) := by
+    p.eval₂ f ofNat(n) = f (p.eval (ofNat(n))) := by
   simp [OfNat.ofNat]
 
 @[simp]
@@ -279,7 +279,7 @@ alias eval_nat_cast := eval_natCast
 
 @[simp]
 lemma eval_ofNat (n : ℕ) [n.AtLeastTwo] (a : R) :
-    (ofNat(n) : R[X]).eval a = OfNat.ofNat n := by
+    (ofNat(n) : R[X]).eval a = ofNat(n) := by
   simp only [OfNat.ofNat, eval_natCast]
 
 @[simp]
@@ -549,7 +549,7 @@ alias map_nat_cast := map_natCast
 
 @[simp]
 protected theorem map_ofNat (n : ℕ) [n.AtLeastTwo] :
-    (ofNat(n) : R[X]).map f = OfNat.ofNat n :=
+    (ofNat(n) : R[X]).map f = 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/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 (ofNat(n) : R) = OfNat.ofNat n :=
+    star (ofNat(n) : R) = ofNat(n) :=
   star_natCast _
 
 section
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] :
-    ‖(ofNat(n) : ℝ)‖ = OfNat.ofNat n := norm_natCast n
+    ‖(ofNat(n) : ℝ)‖ = ofNat(n) := norm_natCast n
 
 @[simp 1100] lemma nnnorm_ofNat (n : ℕ) [n.AtLeastTwo] :
-    ‖(ofNat(n) : ℝ)‖₊ = OfNat.ofNat n := nnnorm_natCast n
+    ‖(ofNat(n) : ℝ)‖₊ = 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/Data/Matrix/Kronecker.lean b/Mathlib/Data/Matrix/Kronecker.lean
@@ -314,13 +314,13 @@ theorem natCast_kronecker [NonAssocSemiring α] [DecidableEq l] (a : ℕ) (B : M
 
 theorem kronecker_ofNat [Semiring α] [DecidableEq n] (A : Matrix l m α) (b : ℕ) [b.AtLeastTwo] :
     A ⊗ₖ (ofNat(b) : Matrix n n α) =
-      blockDiagonal fun _ => A <• (OfNat.ofNat b : α) :=
+      blockDiagonal fun _ => A <• (ofNat(b) : α) :=
   kronecker_diagonal _ _
 
 theorem ofNat_kronecker [Semiring α] [DecidableEq l] (a : ℕ) [a.AtLeastTwo] (B : Matrix m n α) :
     (ofNat(a) : Matrix l l α) ⊗ₖ B =
       Matrix.reindex (.prodComm _ _) (.prodComm _ _)
-        (blockDiagonal fun _ => (OfNat.ofNat a : α) • B) :=
+        (blockDiagonal fun _ => (ofNat(a) : α) • B) :=
   diagonal_kronecker _ _
 
 theorem one_kronecker_one [MulZeroOneClass α] [DecidableEq m] [DecidableEq n] :
diff --git a/Mathlib/Data/Matrix/Notation.lean b/Mathlib/Data/Matrix/Notation.lean
@@ -420,12 +420,12 @@ theorem natCast_fin_three (n : ℕ) :
 
 theorem ofNat_fin_two (n : ℕ) [n.AtLeastTwo] :
     (ofNat(n) : Matrix (Fin 2) (Fin 2) α) =
-      !![OfNat.ofNat n, 0; 0, OfNat.ofNat n] :=
+      !![ofNat(n), 0; 0, ofNat(n)] :=
   natCast_fin_two _
 
 theorem ofNat_fin_three (n : ℕ) [n.AtLeastTwo] :
     (ofNat(n) : Matrix (Fin 3) (Fin 3) α) =
-      !![OfNat.ofNat n, 0, 0; 0, OfNat.ofNat n, 0; 0, 0, OfNat.ofNat n] :=
+      !![ofNat(n), 0, 0; 0, ofNat(n), 0; 0, 0, ofNat(n)] :=
   natCast_fin_three _
 
 end AddMonoidWithOne
