chore: add lemmas for nat literals corresponding to lemmas for nat ca…

…sts (#8006)

I loogled for every occurrence of `"cast", Nat` and `"natCast"` and where the casted nat was `n`, and made sure there were corresponding `@[simp]` lemmas for `0`, `1`, and `OfNat.ofNat n`. This is necessary in general for simp confluence. Example:

```lean
import Mathlib

variable {α : Type*} [LinearOrderedRing α] (m n : ℕ) [m.AtLeastTwo] [n.AtLeastTwo]

example : ((OfNat.ofNat m : ℕ) : α) ≤ ((OfNat.ofNat n : ℕ) : α) ↔ (OfNat.ofNat m : ℕ) ≤ (OfNat.ofNat n : ℕ) := by
  simp only [Nat.cast_le] -- this `@[simp]` lemma can apply

example : ((OfNat.ofNat m : ℕ) : α) ≤ ((OfNat.ofNat n : ℕ) : α) ↔ (OfNat.ofNat m : α) ≤ (OfNat.ofNat n : α) := by
  simp only [Nat.cast_ofNat] -- and so can this one

example : (OfNat.ofNat m : α) ≤ (OfNat.ofNat n : α) ↔ (OfNat.ofNat m : ℕ) ≤ (OfNat.ofNat n : ℕ) := by
  simp -- fails! `simp` doesn't have a lemma to bridge their results. confluence issue.
```

As far as I know, the only file this PR leaves with `ofNat` gaps is `PartENat.lean`. #8002 is addressing that file in parallel.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Archive/Imo/Imo1969Q1.lean

@@ -68,7 +68,7 @@ theorem not_prime_of_int_mul' {m n : ℤ} {c : ℕ} (hm : 1 < m) (hn : 1 < n) (h
 
 /-- Every natural number of the form `n^4 + 4*m^4` is not prime. -/
 theorem polynomial_not_prime {m : ℕ} (h1 : 1 < m) (n : ℕ) : ¬Nat.Prime (n ^ 4 + 4 * m ^ 4) := by
-  have h2 : 1 < (m : ℤ) := ofNat_lt.mpr h1
+  have h2 : 1 < (m : ℤ) := Int.ofNat_lt.mpr h1
   refine' not_prime_of_int_mul' (left_factor_large (n : ℤ) h2) (right_factor_large (n : ℤ) h2) _
   apply factorization
 #align imo1969_q1.polynomial_not_prime Imo1969Q1.polynomial_not_prime

Mathlib/Algebra/CharP/Basic.lean

@@ -120,6 +120,17 @@ theorem CharP.cast_eq_zero [AddMonoidWithOne R] (p : ℕ) [CharP R p] : (p : R)
   (CharP.cast_eq_zero_iff R p p).2 (dvd_refl p)
 #align char_p.cast_eq_zero CharP.cast_eq_zero
 
+-- 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 lean4#2867 is fixed in a performant way, this can be made `@[simp]`.
+--
+-- @[simp]
+theorem CharP.ofNat_eq_zero [AddMonoidWithOne R] (p : ℕ) [p.AtLeastTwo] [CharP R p] :
+    (no_index (OfNat.ofNat p : R)) = 0 :=
+  cast_eq_zero R p
+
 @[simp]
 theorem CharP.cast_card_eq_zero [AddGroupWithOne R] [Fintype R] : (Fintype.card R : R) = 0 := by
   rw [← nsmul_one, card_nsmul_eq_zero]

Mathlib/Algebra/DirectSum/Ring.lean

@@ -457,11 +457,19 @@ theorem of_zero_pow (a : A 0) : ∀ n : ℕ, of A 0 (a ^ n) = of A 0 a ^ n
 instance : NatCast (A 0) :=
   ⟨GSemiring.natCast⟩
 
+
+-- TODO: These could be replaced by the general lemmas for `AddMonoidHomClass` (`map_natCast'` and
+-- `map_ofNat'`) if those were marked `@[simp low]`.
 @[simp]
 theorem of_natCast (n : ℕ) : of A 0 n = n :=
   rfl
 #align direct_sum.of_nat_cast DirectSum.of_natCast
 
+-- 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 :=
+  of_natCast A n
+
 /-- The `Semiring` structure derived from `GSemiring A`. -/
 instance GradeZero.semiring : Semiring (A 0) :=
   Function.Injective.semiring (of A 0) DFinsupp.single_injective (of A 0).map_zero (of_zero_one A)

Mathlib/Algebra/Group/Hom/Instances.lean

@@ -93,6 +93,20 @@ theorem AddMonoid.End.natCast_apply [AddCommMonoid M] (n : ℕ) (m : M) :
   rfl
 #align add_monoid.End.nat_cast_apply AddMonoid.End.natCast_apply
 
+@[simp]
+theorem AddMonoid.End.zero_apply [AddCommMonoid M] (m : M) : (0 : AddMonoid.End M) m = 0 :=
+  rfl
+
+-- Note: `@[simp]` omitted because `(1 : AddMonoid.End M) = id` by `AddMonoid.coe_one`
+theorem AddMonoid.End.one_apply [AddCommMonoid M] (m : M) : (1 : AddMonoid.End M) m = m :=
+  rfl
+
+-- See note [no_index around OfNat.ofNat]
+@[simp]
+theorem AddMonoid.End.ofNat_apply [AddCommMonoid M] (n : ℕ) [n.AtLeastTwo] (m : M) :
+    (no_index (OfNat.ofNat n : AddMonoid.End M)) m = n • m :=
+  rfl
+
 instance AddMonoid.End.instAddCommGroup [AddCommGroup M] : AddCommGroup (AddMonoid.End M) :=
   AddMonoidHom.addCommGroup
 

Mathlib/Algebra/Group/Opposite.lean

@@ -210,6 +210,12 @@ theorem op_natCast [NatCast α] (n : ℕ) : op (n : α) = n :=
 #align mul_opposite.op_nat_cast MulOpposite.op_natCast
 #align add_opposite.op_nat_cast AddOpposite.op_natCast
 
+-- 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 :=
+  rfl
+
 @[to_additive (attr := simp, norm_cast)]
 theorem op_intCast [IntCast α] (n : ℤ) : op (n : α) = n :=
   rfl
@@ -222,6 +228,12 @@ theorem unop_natCast [NatCast α] (n : ℕ) : unop (n : αᵐᵒᵖ) = n :=
 #align mul_opposite.unop_nat_cast MulOpposite.unop_natCast
 #align add_opposite.unop_nat_cast AddOpposite.unop_natCast
 
+-- 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 :=
+  rfl
+
 @[to_additive (attr := simp, norm_cast)]
 theorem unop_intCast [IntCast α] (n : ℤ) : unop (n : αᵐᵒᵖ) = n :=
   rfl

Mathlib/Algebra/Group/ULift.lean

@@ -153,6 +153,12 @@ theorem up_natCast [NatCast α] (n : ℕ) : up (n : α) = n :=
   rfl
 #align ulift.up_nat_cast ULift.up_natCast
 
+-- See note [no_index around OfNat.ofNat]
+@[simp]
+theorem up_ofNat [NatCast α] (n : ℕ) [n.AtLeastTwo] :
+    up (no_index (OfNat.ofNat n : α)) = OfNat.ofNat n :=
+  rfl
+
 @[simp, norm_cast]
 theorem up_intCast [IntCast α] (n : ℤ) : up (n : α) = n :=
   rfl
@@ -163,6 +169,12 @@ theorem down_natCast [NatCast α] (n : ℕ) : down (n : ULift α) = n :=
   rfl
 #align ulift.down_nat_cast ULift.down_natCast
 
+-- 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 :=
+  rfl
+
 @[simp, norm_cast]
 theorem down_intCast [IntCast α] (n : ℤ) : down (n : ULift α) = n :=
   rfl

Mathlib/Algebra/Order/Ring/Abs.lean

@@ -37,7 +37,7 @@ variable [LinearOrderedRing α] {n : ℕ} {a b c : α}
 @[simp] lemma abs_one : |(1 : α)| = 1 := abs_of_pos zero_lt_one
 #align abs_one abs_one
 
-@[simp] lemma abs_two : |(2 : α)| = 2 := abs_of_pos zero_lt_two
+lemma abs_two : |(2 : α)| = 2 := abs_of_pos zero_lt_two
 #align abs_two abs_two
 
 lemma abs_mul (a b : α) : |a * b| = |a| * |b| := by

Mathlib/Algebra/Star/SelfAdjoint.lean

@@ -218,6 +218,12 @@ theorem _root_.isSelfAdjoint_natCast (n : ℕ) : IsSelfAdjoint (n : R) :=
   star_natCast _
 #align is_self_adjoint_nat_cast isSelfAdjoint_natCast
 
+-- See note [no_index around OfNat.ofNat]
+@[simp]
+theorem _root_.isSelfAdjoint_ofNat (n : ℕ) [n.AtLeastTwo] :
+    IsSelfAdjoint (no_index (OfNat.ofNat n : R)) :=
+  _root_.isSelfAdjoint_natCast n
+
 end Semiring
 
 section CommSemigroup

Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean

@@ -181,7 +181,7 @@ theorem integral_Ioi_cpow_of_lt {a : ℂ} (ha : a.re < -1) {c : ℝ} (hc : 0 < c
 
 theorem integrable_inv_one_add_sq : Integrable fun (x : ℝ) ↦ (1 + x ^ 2)⁻¹ := by
   suffices Integrable fun (x : ℝ) ↦ (1 + ‖x‖ ^ 2) ^ ((-2 : ℝ) / 2) by simpa [rpow_neg_one]
-  exact integrable_rpow_neg_one_add_norm_sq (by simpa using by norm_num)
+  exact integrable_rpow_neg_one_add_norm_sq (by simp)
 
 @[simp]
 theorem integral_Iic_inv_one_add_sq {i : ℝ} :

Mathlib/Data/ENNReal/Basic.lean

@@ -455,9 +455,7 @@ theorem toReal_eq_toReal_iff' {x y : ℝ≥0∞} (hx : x ≠ ⊤) (hy : y ≠ 
   simp only [ENNReal.toReal, NNReal.coe_inj, toNNReal_eq_toNNReal_iff' hx hy]
 #align ennreal.to_real_eq_to_real_iff' ENNReal.toReal_eq_toReal_iff'
 
-@[simp]
-nonrec theorem one_lt_two : (1 : ℝ≥0∞) < 2 :=
-  coe_one ▸ coe_two ▸ mod_cast (one_lt_two : 1 < 2)
+theorem one_lt_two : (1 : ℝ≥0∞) < 2 := Nat.one_lt_ofNat
 #align ennreal.one_lt_two ENNReal.one_lt_two
 
 @[simp] theorem two_ne_top : (2 : ℝ≥0∞) ≠ ∞ := coe_ne_top

Mathlib/Data/ENat/Basic.lean

@@ -109,6 +109,11 @@ theorem toNat_coe (n : ℕ) : toNat n = n :=
   rfl
 #align enat.to_nat_coe ENat.toNat_coe
 
+-- See note [no_index around OfNat.ofNat]
+@[simp]
+theorem toNat_ofNat (n : ℕ) [n.AtLeastTwo] : toNat (no_index (OfNat.ofNat n)) = n :=
+  rfl
+
 @[simp]
 theorem toNat_top : toNat ⊤ = 0 :=
   rfl
@@ -135,21 +140,54 @@ theorem recTopCoe_coe {C : ℕ∞ → Sort*} (d : C ⊤) (f : ∀ a : ℕ, C a)
     @recTopCoe C d f ↑x = f x :=
   rfl
 
+@[simp]
+theorem recTopCoe_zero {C : ℕ∞ → Sort*} (d : C ⊤) (f : ∀ a : ℕ, C a) : @recTopCoe C d f 0 = f 0 :=
+  rfl
+
+@[simp]
+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) :=
+  rfl
+
 --Porting note: new theorem copied from `WithTop`
 @[simp]
 theorem top_ne_coe (a : ℕ) : ⊤ ≠ (a : ℕ∞) :=
   fun.
 
+-- See note [no_index around OfNat.ofNat]
+@[simp]
+theorem top_ne_ofNat (a : ℕ) [a.AtLeastTwo] : ⊤ ≠ (no_index (OfNat.ofNat a : ℕ∞)) :=
+  fun.
+
 --Porting note: new theorem copied from `WithTop`
 @[simp]
 theorem coe_ne_top (a : ℕ) : (a : ℕ∞) ≠ ⊤ :=
   fun.
 
+-- See note [no_index around OfNat.ofNat]
+@[simp]
+theorem ofNat_ne_top (a : ℕ) [a.AtLeastTwo] : (no_index (OfNat.ofNat a : ℕ∞)) ≠ ⊤ :=
+  fun.
+
 --Porting note: new theorem copied from `WithTop`
 @[simp]
 theorem top_sub_coe (a : ℕ) : (⊤ : ℕ∞) - a = ⊤ :=
   WithTop.top_sub_coe
 
+@[simp]
+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)) = ⊤ :=
+  top_sub_coe a
+
 @[simp]
 theorem zero_lt_top : (0 : ℕ∞) < ⊤ :=
   WithTop.zero_lt_top
@@ -159,7 +197,7 @@ theorem sub_top (a : ℕ∞) : a - ⊤ = 0 :=
   WithTop.sub_top
 
 @[simp]
-theorem coe_toNat_eq_self : ENat.toNat (n : ℕ∞) = n ↔ n ≠ ⊤ :=
+theorem coe_toNat_eq_self : ENat.toNat n = n ↔ n ≠ ⊤ :=
   ENat.recTopCoe (by decide) (fun _ => by simp [toNat_coe]) n
 #align enat.coe_to_nat_eq_self ENat.coe_toNat_eq_self
 

Mathlib/Data/Int/Log.lean

@@ -78,6 +78,12 @@ theorem log_natCast (b : ℕ) (n : ℕ) : log b (n : R) = Nat.log b n := by
     simp
 #align int.log_nat_cast Int.log_natCast
 
+-- 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_natCast b n
+
 theorem log_of_left_le_one {b : ℕ} (hb : b ≤ 1) (r : R) : log b r = 0 := by
   rcases le_total 1 r with h | h
   · rw [log_of_one_le_right _ h, Nat.log_of_left_le_one hb, Int.ofNat_zero]
@@ -232,6 +238,12 @@ theorem clog_natCast (b : ℕ) (n : ℕ) : clog b (n : R) = Nat.clog b n := by
   · rw [clog_of_one_le_right, (Nat.ceil_eq_iff (Nat.succ_ne_zero n)).mpr] <;> simp
 #align int.clog_nat_cast Int.clog_natCast
 
+-- 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_natCast b n
+
 theorem clog_of_left_le_one {b : ℕ} (hb : b ≤ 1) (r : R) : clog b r = 0 := by
   rw [← neg_log_inv_eq_clog, log_of_left_le_one hb, neg_zero]
 #align int.clog_of_left_le_one Int.clog_of_left_le_one

Mathlib/Data/Matrix/Basic.lean

@@ -2265,6 +2265,13 @@ theorem conjTranspose_natCast_smul [Semiring R] [AddCommMonoid α] [StarAddMonoi
   Matrix.ext <| by simp
 #align matrix.conj_transpose_nat_cast_smul Matrix.conjTranspose_natCast_smul
 
+-- See note [no_index around OfNat.ofNat]
+@[simp]
+theorem conjTranspose_ofNat_smul [Semiring R] [AddCommMonoid α] [StarAddMonoid α] [Module R α]
+    (c : ℕ) [c.AtLeastTwo] (M : Matrix m n α) :
+    ((no_index (OfNat.ofNat c : R)) • M)ᴴ = (OfNat.ofNat c : R) • Mᴴ :=
+  conjTranspose_natCast_smul c M
+
 @[simp]
 theorem conjTranspose_intCast_smul [Ring R] [AddCommGroup α] [StarAddMonoid α] [Module R α] (c : ℤ)
     (M : Matrix m n α) : ((c : R) • M)ᴴ = (c : R) • Mᴴ :=
@@ -2277,6 +2284,13 @@ theorem conjTranspose_inv_natCast_smul [DivisionSemiring R] [AddCommMonoid α] [
   Matrix.ext <| by simp
 #align matrix.conj_transpose_inv_nat_cast_smul Matrix.conjTranspose_inv_natCast_smul
 
+-- See note [no_index around OfNat.ofNat]
+@[simp]
+theorem conjTranspose_inv_ofNat_smul [DivisionSemiring R] [AddCommMonoid α] [StarAddMonoid α]
+    [Module R α] (c : ℕ) [c.AtLeastTwo] (M : Matrix m n α) :
+    ((no_index (OfNat.ofNat c : R))⁻¹ • M)ᴴ = (OfNat.ofNat c : R)⁻¹ • Mᴴ :=
+  conjTranspose_inv_natCast_smul c M
+
 @[simp]
 theorem conjTranspose_inv_intCast_smul [DivisionRing R] [AddCommGroup α] [StarAddMonoid α]
     [Module R α] (c : ℤ) (M : Matrix m n α) : ((c : R)⁻¹ • M)ᴴ = (c : R)⁻¹ • Mᴴ :=

Mathlib/Data/NNRat/Defs.lean

@@ -194,12 +194,13 @@ def coeHom : ℚ≥0 →+* ℚ where
 
 @[simp, norm_cast]
 theorem coe_natCast (n : ℕ) : (↑(↑n : ℚ≥0) : ℚ) = n :=
-  map_natCast coeHom n
+  rfl
 #align nnrat.coe_nat_cast NNRat.coe_natCast
 
+-- See note [no_index around OfNat.ofNat]
 @[simp]
 theorem mk_coe_nat (n : ℕ) : @Eq ℚ≥0 (⟨(n : ℚ), n.cast_nonneg⟩ : ℚ≥0) n :=
-  ext (coe_natCast n).symm
+  rfl
 #align nnrat.mk_coe_nat NNRat.mk_coe_nat
 
 @[simp]

Mathlib/Data/Nat/Cast/Basic.lean

@@ -127,6 +127,10 @@ theorem map_natCast' {A} [AddMonoidWithOne A] [FunLike F A B] [AddMonoidHomClass
     rw [Nat.cast_add, map_add, Nat.cast_add, map_natCast' f h n, Nat.cast_one, h, Nat.cast_one]
 #align map_nat_cast' map_natCast'
 
+theorem map_ofNat' {A} [AddMonoidWithOne A] [FunLike F A B] [AddMonoidHomClass F A B]
+    (f : F) (h : f 1 = 1) (n : ℕ) [n.AtLeastTwo] : f (OfNat.ofNat n) = OfNat.ofNat n :=
+  map_natCast' f h n
+
 @[simp] lemma nsmul_one {A} [AddMonoidWithOne A] : ∀ n : ℕ, n • (1 : A) = n := by
   let f : ℕ →+ A :=
   { toFun := fun n ↦ n • (1 : A)