From 0de61bdb4bfcb9f17d4614d610d858bd9de39643 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Thu, 18 Apr 2024 10:42:19 +0000 Subject: [PATCH] chore: Rename `isnatCast`, delete `Int.cast_Nat_cast` (#12236) `Int.cast_Nat_cast` dates back to the ad-hoc port, in #206. --- Mathlib/Algebra/Ring/Int.lean | 6 ------ Mathlib/Tactic/NormNum/Basic.lean | 4 ++-- Mathlib/Tactic/ReduceModChar.lean | 2 +- 3 files changed, 3 insertions(+), 9 deletions(-) diff --git a/Mathlib/Algebra/Ring/Int.lean b/Mathlib/Algebra/Ring/Int.lean index 01746f3d383c3..cfd2afd14c0df 100644 --- 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 index 8d6c3569e41b5..154938bf1ba6e 100644 --- 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 index b9acab8a03476..9e91bd6131f34 100644 --- 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)