chore: deprecate Nat.cast_eq_ofNat (#20168)

This lemma is malformed; the `n` on the RHS must be a raw literal, but the one on the left is not. Correcting the statement results in `Nat.cast_ofNat` which already exists.

Author: eric-wieser

Mathlib/Algebra/Polynomial/Basic.lean

@@ -678,8 +678,8 @@ theorem coeff_ofNat_zero (a : ℕ) [a.AtLeastTwo] :
 @[simp]
 theorem coeff_ofNat_succ (a n : ℕ) [h : a.AtLeastTwo] :
     coeff (no_index (OfNat.ofNat a : R[X])) (n + 1) = 0 := by
-  rw [← Nat.cast_eq_ofNat]
-  simp
+  rw [← Nat.cast_ofNat]
+  simp [-Nat.cast_ofNat]
 
 theorem C_mul_X_pow_eq_monomial : ∀ {n : ℕ}, C a * X ^ n = monomial n a
   | 0 => mul_one _

Mathlib/Algebra/Ring/Subsemiring/Defs.lean

@@ -33,7 +33,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
-  rw [← Nat.cast_eq_ofNat]; exact natCast_mem s n
+  rw [← Nat.cast_ofNat]; exact natCast_mem s n
 
 instance (priority := 74) AddSubmonoidWithOneClass.toAddMonoidWithOne
     [AddSubmonoidWithOneClass S R] : AddMonoidWithOne s :=

Mathlib/Analysis/SpecialFunctions/Trigonometric/EulerSineProd.lean

@@ -219,7 +219,7 @@ theorem sin_pi_mul_eq (z : ℂ) (n : ℕ) :
       dsimp only [C]
       rw [integral_cos_pow_eq, aux', integral_sin_pow, sin_zero, sin_pi, pow_succ',
         zero_mul, zero_mul, zero_mul, sub_zero, zero_div,
-        zero_add, ← mul_assoc, ← mul_assoc, mul_comm (1 / 2 : ℝ) _, Nat.cast_mul, Nat.cast_eq_ofNat]
+        zero_add, ← mul_assoc, ← mul_assoc, mul_comm (1 / 2 : ℝ) _, Nat.cast_mul, Nat.cast_ofNat]
     rw [this]
     change
       π * z * A * B / C =

Mathlib/Data/Nat/Cast/Defs.lean

@@ -68,6 +68,7 @@ Some discussion is [on Zulip here](https://leanprover.zulipchat.com/#narrow/stre
 @[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
 
+@[deprecated Nat.cast_ofNat (since := "2024-12-22")]
 theorem Nat.cast_eq_ofNat {n : ℕ} [NatCast R] [Nat.AtLeastTwo n] :
     (Nat.cast n : R) = OfNat.ofNat n :=
   rfl

Mathlib/FieldTheory/CardinalEmb.lean

@@ -210,7 +210,7 @@ instance (i : ι) : Algebra.IsSeparable (E⟮<i⟯) (E⟮<i⟯⟮b (φ i)⟯) :=
 
 open Field in
 theorem two_le_deg (i : ι) : 2 ≤ #(X i) := by
-  rw [← Nat.cast_eq_ofNat, ← toNat_le_iff_le_of_lt_aleph0 (nat_lt_aleph0 _) (deg_lt_aleph0 i),
+  rw [← Nat.cast_ofNat, ← toNat_le_iff_le_of_lt_aleph0 (nat_lt_aleph0 _) (deg_lt_aleph0 i),
     toNat_natCast, ← Nat.card, ← finSepDegree, finSepDegree_eq_finrank_of_isSeparable, Nat.succ_le]
   by_contra!
   obtain ⟨x, hx⟩ := finrank_adjoin_simple_eq_one_iff.mp (this.antisymm Module.finrank_pos)

Mathlib/LinearAlgebra/Reflection.lean

@@ -385,7 +385,8 @@ lemma reflection_reflection_iterate
   | succ n ih =>
     have hz : ∀ z : M, f y • g x • z = 2 • 2 • z := by
       intro z
-      rw [smul_smul, hgxfy, smul_smul, ← Nat.cast_smul_eq_nsmul R (2 * 2), Nat.cast_eq_ofNat]
+      rw [smul_smul, hgxfy, smul_smul, ← Nat.cast_smul_eq_nsmul R (2 * 2), show 2 * 2 = 4 from rfl,
+        Nat.cast_ofNat]
     simp only [iterate_succ', comp_apply, ih, two_smul, smul_sub, smul_add, map_add,
       LinearEquiv.trans_apply, reflection_apply_self, map_neg, reflection_apply, neg_sub, map_sub,
       map_nsmul, map_smul, smul_neg, hz, add_smul]

Mathlib/Tactic/NoncommRing.lean

@@ -23,10 +23,10 @@ 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 = n • r := by
-  simp only [nsmul_eq_mul, Nat.cast_eq_ofNat]
-lemma mul_nat_lit_eq_nsmul [n.AtLeastTwo] : r * no_index (OfNat.ofNat n) = n • r := by
-  simp only [nsmul_eq_mul', Nat.cast_eq_ofNat]
+lemma nat_lit_mul_eq_nsmul [n.AtLeastTwo] : no_index (OfNat.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
+  simp only [nsmul_eq_mul', Nat.cast_ofNat]
 
 end nat_lit_mul