[Merged by Bors] - feat: port Data.Int.Cast.Basic

Mathlib/Algebra/Ring/Basic.lean

@@ -1,6 +1,6 @@
 import Mathlib.Algebra.Group.Commute
 import Mathlib.Algebra.GroupWithZero.Defs
-import Mathlib.Data.Int.Cast.Defs
+import Mathlib.Data.Int.Cast.Basic
 import Mathlib.Tactic.Spread
 import Mathlib.Algebra.Ring.Defs
 
@@ -115,7 +115,7 @@ instance : CommRing ℤ where
 
 @[simp, norm_cast]
 lemma cast_Nat_cast [AddGroupWithOne R] : (Int.cast (Nat.cast n) : R) = Nat.cast n :=
-  Int.cast_ofNat
+  Int.cast_ofNat _
 
 @[simp, norm_cast]
 lemma cast_eq_cast_iff_Nat (m n : ℕ) : (m : ℤ) = (n : ℤ) ↔ m = n := ofNat_inj

Mathlib/Data/Int/Cast/Basic.lean

@@ -7,59 +7,149 @@ import Mathlib.Data.Int.Cast.Defs
 import Mathlib.Algebra.Group.Basic
 
 /-!
-# Cast of integers
+# Cast of integers (additional theorems)
 
-This file defines the *canonical* homomorphism from the integers into an
-additive group with a one (typically a `ring`).  In additive groups with a one
-element, there exists a unique such homomorphism and we store it in the
-`int_cast : ℤ → R` field.
+This file proves additional properties about the *canonical* homomorphism from
+the integers into an additive group with a one (`int.cast`).
 
-Preferentially, the homomorphism is written as a coercion.
+There is also `Data.Int.Cast.Lemmas`,
+which includes lemmas stated in terms of algebraic homomorphisms,
+and results involving the order structure of `ℤ`.
 
-## Main declarations
-
-* `int.cast`: Canonical homomorphism `ℤ → R`.
-* `add_group_with_one`: Type class for `int.cast`.
+By contrast, this file's only import beyond `Data.Int.Cast.Defs` is `Algebra.Group.Basic`.
 -/
 
+
+universe u
+
 namespace Nat
-variable [AddGroupWithOne R]
+
+variable {R : Type u} [AddGroupWithOne R]
 
 @[simp, norm_cast]
 theorem cast_sub {m n} (h : m ≤ n) : ((n - m : ℕ) : R) = n - m :=
   eq_sub_of_add_eq <| by rw [← cast_add, Nat.sub_add_cancel h]
+#align nat.cast_sub Nat.cast_subₓ
+-- `HasLiftT` appeared in the type signature
+
+@[simp, norm_cast]
+theorem cast_pred : ∀ {n}, 0 < n → ((n - 1 : ℕ) : R) = n - 1
+  | 0, h => by cases h
+  | n + 1, _ => by rw [cast_succ, add_sub_cancel]; rfl
+#align nat.cast_pred Nat.cast_pred
 
 end Nat
 
+open Nat
+
 namespace Int
-variable [AddGroupWithOne R]
+
+variable {R : Type u} [AddGroupWithOne R]
+
+@[simp, norm_cast]
+theorem cast_negSucc (n : ℕ) : (-[n+1] : R) = -(n + 1 : ℕ) :=
+  AddGroupWithOne.intCast_negSucc n
+#align int.cast_neg_succ_of_nat Int.cast_negSuccₓ
+-- expected `n` to be implicit, and `HasLiftT`
+
+@[simp, norm_cast]
+theorem cast_zero : ((0 : ℤ) : R) = 0 :=
+  (AddGroupWithOne.intCast_ofNat 0).trans Nat.cast_zero
+#align int.cast_zero Int.cast_zeroₓ
+-- type had `HasLiftT`
+
+@[simp high, nolint simpNF] -- this lemma competes with `Int.ofNat_eq_cast` to come later
+theorem cast_ofNat (n : ℕ) : ((n : ℤ) : R) = n :=
+  AddGroupWithOne.intCast_ofNat _
+#align int.cast_coe_nat Int.cast_ofNatₓ
+-- expected `n` to be implicit, and `HasLiftT`
+
+@[simp, norm_cast]
+theorem cast_one : ((1 : ℤ) : R) = 1 := by
+  erw [cast_ofNat, Nat.cast_one]
+#align int.cast_one Int.cast_oneₓ
+-- type had `HasLiftT`
 
 @[simp, norm_cast]
-theorem cast_neg [AddGroupWithOne R] : ∀ n:ℤ, ((-n : ℤ) : R) = -↑n
+theorem cast_neg : ∀ n, ((-n : ℤ) : R) = -n
   | (0 : ℕ) => by erw [cast_zero, neg_zero]
   | (n + 1 : ℕ) => by erw [cast_ofNat, cast_negSucc]
-  | -[n +1] => by erw [cast_ofNat, cast_negSucc, neg_neg]
+  | -[n+1] => by erw [cast_ofNat, cast_negSucc, neg_neg]
+#align int.cast_neg Int.cast_negₓ
+-- type had `HasLiftT`
 
-@[simp]
-theorem cast_subNatNat [AddGroupWithOne R] (m n) : ((subNatNat m n : ℤ) : R) = m - n := by
-  unfold Int.subNatNat
+@[simp, norm_cast]
+theorem cast_subNatNat (m n) : ((Int.subNatNat m n : ℤ) : R) = m - n := by
+  unfold subNatNat
   cases e : n - m
-  · simp only [subNatNat, cast_ofNat]
+  · rw [cast_ofNat]
     simp [e, Nat.le_of_sub_eq_zero e]
   · rw [cast_negSucc, Nat.add_one, ← e, Nat.cast_sub <| _root_.le_of_lt <| Nat.lt_of_sub_eq_succ e,
       neg_sub]
-#align int.cast_sub_nat_nat Int.cast_subNatNat
+#align int.cast_sub_nat_nat Int.cast_subNatNatₓ
+-- type had `HasLiftT`
+
+#align int.neg_of_nat_eq Int.negOfNat_eq
+
+@[simp]
+theorem cast_negOfNat (n : ℕ) : ((negOfNat n : ℤ) : R) = -n := by simp [Int.cast_neg, negOfNat_eq]
+#align int.cast_neg_of_nat Int.cast_negOfNat
 
 @[simp, norm_cast]
-theorem cast_add [AddGroupWithOne R] : ∀ m n, ((m + n : ℤ) : R) = m + n
-  | (m : ℕ), (n : ℕ) => by simp [← ofNat_add]
+theorem cast_add : ∀ m n, ((m + n : ℤ) : R) = m + n
+  | (m : ℕ), (n : ℕ) => by simp [← Int.ofNat_add, Nat.cast_add]
   | (m : ℕ), -[n+1] => by erw [cast_subNatNat, cast_ofNat, cast_negSucc, sub_eq_add_neg]
   | -[m+1], (n : ℕ) => by
-    erw [cast_subNatNat, cast_ofNat, cast_negSucc, sub_eq_iff_eq_add,
-      add_assoc, eq_neg_add_iff_add_eq, ← Nat.cast_add, ← Nat.cast_add, Nat.add_comm]
-  | -[m+1], -[n+1] => show (-[m + n + 1 +1] : R) = _ by
-    rw [cast_negSucc, cast_negSucc, cast_negSucc, ← neg_add_rev, ← Nat.cast_add,
-      Nat.add_right_comm m n 1, Nat.add_assoc, Nat.add_comm]
+    erw [cast_subNatNat, cast_ofNat, cast_negSucc, sub_eq_iff_eq_add, add_assoc,
+      eq_neg_add_iff_add_eq, ← Nat.cast_add, ← Nat.cast_add, Nat.add_comm]
+  | -[m+1], -[n+1] =>
+    show (-[m + n + 1+1] : R) = _ by
+      rw [cast_negSucc, cast_negSucc, cast_negSucc, ← neg_add_rev, ← Nat.cast_add,
+        Nat.add_right_comm m n 1, Nat.add_assoc, Nat.add_comm]
+#align int.cast_add Int.cast_addₓ
+-- type had `HasLiftT`
 
 @[simp, norm_cast]
-theorem cast_sub (m n) : ((m - n : ℤ) : R) = m - n := by simp [Int.sub_eq_add_neg, sub_eq_add_neg]
+theorem cast_sub (m n) : ((m - n : ℤ) : R) = m - n := by
+  simp [Int.sub_eq_add_neg, sub_eq_add_neg, Int.cast_neg, Int.cast_add]
+#align int.cast_sub Int.cast_subₓ
+-- type had `HasLiftT`
+
+section deprecated
+set_option linter.deprecated false
+
+@[norm_cast, deprecated]
+theorem ofNat_bit0 (n : ℕ) : (↑(bit0 n) : ℤ) = bit0 ↑n :=
+  rfl
+#align int.coe_nat_bit0 Int.ofNat_bit0
+
+@[norm_cast, deprecated]
+theorem ofNat_bit1 (n : ℕ) : (↑(bit1 n) : ℤ) = bit1 ↑n :=
+  rfl
+#align int.coe_nat_bit1 Int.ofNat_bit1
+
+@[norm_cast, deprecated]
+theorem cast_bit0 (n : ℤ) : ((bit0 n : ℤ) : R) = bit0 (n : R) :=
+  Int.cast_add _ _
+#align int.cast_bit0 Int.cast_bit0
+
+@[norm_cast, deprecated]
+theorem cast_bit1 (n : ℤ) : ((bit1 n : ℤ) : R) = bit1 (n : R) :=
+  by rw [bit1, Int.cast_add, Int.cast_one, cast_bit0]; rfl
+#align int.cast_bit1 Int.cast_bit1
+
+end deprecated
+
+theorem cast_two : ((2 : ℤ) : R) = 2 :=
+  show (((2 : ℕ) : ℤ) : R) = ((2 : ℕ) : R) by rw [cast_ofNat, Nat.cast_ofNat]
+#align int.cast_two Int.cast_two
+
+theorem cast_three : ((3 : ℤ) : R) = 3 :=
+  show (((3 : ℕ) : ℤ) : R) = ((3 : ℕ) : R) by rw [cast_ofNat, Nat.cast_ofNat]
+#align int.cast_three Int.cast_three
+
+theorem cast_four : ((4 : ℤ) : R) = 4 :=
+  show (((4 : ℕ) : ℤ) : R) = ((4 : ℕ) : R) by rw [cast_ofNat, Nat.cast_ofNat]
+#align int.cast_four Int.cast_four
+
+end Int

Mathlib/Data/Int/Cast/Defs.lean

@@ -65,23 +65,6 @@ namespace Int
 
 instance [IntCast R] : CoeTail ℤ R where coe := cast
 
-@[simp high, nolint simpNF] -- this lemma competes with `Int.ofNat_eq_cast` to come later
-theorem cast_ofNat [AddGroupWithOne R] : (cast (ofNat n) : R) = Nat.cast n :=
-  AddGroupWithOne.intCast_ofNat _
-#align int.cast_coe_nat Int.cast_ofNat
-
-@[simp, norm_cast]
-theorem cast_negSucc [AddGroupWithOne R] : (cast (negSucc n) : R) = (-(Nat.cast (n + 1)) : R) :=
-  AddGroupWithOne.intCast_negSucc _
-#align int.cast_neg_succ_of_nat Int.cast_negSucc
-
-@[simp, norm_cast] theorem cast_zero [AddGroupWithOne R] : ((0 : ℤ) : R) = 0 := by
-  erw [cast_ofNat, Nat.cast_zero]
-#align int.cast_zero Int.cast_zero
-@[simp, norm_cast] theorem cast_one [AddGroupWithOne R] : ((1 : ℤ) : R) = 1 := by
-  erw [cast_ofNat, Nat.cast_one]
-#align int.cast_one Int.cast_one
-
 end Int
 
 /-- An `AddCommGroupWithOne` is an `AddGroupWithOne` satisfying `a + b = b + a`. -/