chore: Rename isnatCast, delete Int.cast_Nat_cast (#12236)

`Int.cast_Nat_cast` dates back to the ad-hoc port, in #206.
leanprover-community · Apr 18, 2024 · 838bc13 · 838bc13
1 parent e6ebf6f
commit 838bc13
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 9 deletions.
diff --git a/Mathlib/Algebra/Ring/Int.lean b/Mathlib/Algebra/Ring/Int.lean
@@ -70,12 +70,6 @@ instance instDistrib      : Distrib ℤ      := inferInstance
 instance instCharZero : CharZero ℤ where
   cast_injective _ _ := ofNat.inj
 
-/-! ### Miscellaneous lemmas -/
-
-lemma cast_Nat_cast {n : ℕ} {R : Type*} [AddGroupWithOne R] :
-    (Int.cast (Nat.cast n) : R) = Nat.cast n :=
-  Int.cast_natCast _
-
 end Int
 
 assert_not_exists Set.range
diff --git a/Mathlib/Tactic/NormNum/Basic.lean b/Mathlib/Tactic/NormNum/Basic.lean
@@ -101,7 +101,7 @@ theorem isNat_natAbs_neg : {n : ℤ} → {a : ℕ} → IsInt n (.negOfNat a) →
 
 /-! # Casts -/
 
-theorem isnatCast {R} [AddMonoidWithOne R] (n m : ℕ) :
+theorem isNat_natCast {R} [AddMonoidWithOne R] (n m : ℕ) :
     IsNat n m → IsNat (n : R) m := by rintro ⟨⟨⟩⟩; exact ⟨rfl⟩
 
 /-- The `norm_num` extension which identifies an expression `Nat.cast n`, returning `n`. -/
@@ -111,7 +111,7 @@ theorem isnatCast {R} [AddMonoidWithOne R] (n m : ℕ) :
   guard <|← withNewMCtxDepth <| isDefEq n q(Nat.cast (R := $α))
   let ⟨na, pa⟩ ← deriveNat a q(instAddMonoidWithOneNat)
   haveI' : $e =Q $a := ⟨⟩
-  return .isNat sα na q(isnatCast $a $na $pa)
+  return .isNat sα na q(isNat_natCast $a $na $pa)
 
 theorem isNat_intCast {R} [Ring R] (n : ℤ) (m : ℕ) :
     IsNat n m → IsNat (n : R) m := by rintro ⟨⟨⟩⟩; exact ⟨by simp⟩

diff --git a/Mathlib/Tactic/ReduceModChar.lean b/Mathlib/Tactic/ReduceModChar.lean
@@ -61,7 +61,7 @@ partial def normIntNumeral {α : Q(Type u)} (n : Q(ℕ)) (e : Q($α)) (instRing
   let ⟨ze, ne, pe⟩ ← Result.toInt instRing (← Mathlib.Meta.NormNum.derive e)
   let ⟨n', pn⟩ ← deriveNat n q(instAddMonoidWithOneNat)
   let rr ← evalIntMod.go _ _ ze q(IsInt.raw_refl $ne) _ <|
-    .isNat q(instAddMonoidWithOne) _ q(isnatCast _ _ (IsNat.raw_refl $n'))
+    .isNat q(instAddMonoidWithOne) _ q(isNat_natCast _ _ (IsNat.raw_refl $n'))
   let ⟨zr, nr, pr⟩ ← rr.toInt q(Int.instRingInt)
   return .isInt instRing nr zr q(CharP.isInt_of_mod $instCharP $pe $pn $pr)