chore: Move lemmas about Int.natAbs and zpowersHom (#9806)

These can be defined earlier for free.

Part of #9411

Mathlib/Algebra/GroupPower/Lemmas.lean

@@ -3,7 +3,7 @@ Copyright (c) 2015 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Robert Y. Lewis
 -/
-import Mathlib.Data.Int.Cast.Lemmas
+import Mathlib.Data.Nat.Order.Basic
 
 #align_import algebra.group_power.lemmas from "leanprover-community/mathlib"@"a07d750983b94c530ab69a726862c2ab6802b38c"
 
@@ -21,42 +21,6 @@ universe u v w x y z u₁ u₂
 variable {α : Type*} {M : Type u} {N : Type v} {G : Type w} {H : Type x} {A : Type y} {B : Type z}
   {R : Type u₁} {S : Type u₂}
 
-section bit0_bit1
-
-set_option linter.deprecated false
-
--- The next four lemmas allow us to replace multiplication by a numeral with a `zsmul` expression.
--- They are used by the `noncomm_ring` tactic, to normalise expressions before passing to `abel`.
-theorem bit0_mul [NonUnitalNonAssocRing R] {n r : R} : bit0 n * r = (2 : ℤ) • (n * r) := by
-  dsimp [bit0]
-  rw [add_mul, ← one_add_one_eq_two, add_zsmul, one_zsmul]
-#align bit0_mul bit0_mul
-
-theorem mul_bit0 [NonUnitalNonAssocRing R] {n r : R} : r * bit0 n = (2 : ℤ) • (r * n) := by
-  dsimp [bit0]
-  rw [mul_add, ← one_add_one_eq_two, add_zsmul, one_zsmul]
-#align mul_bit0 mul_bit0
-
-theorem bit1_mul [NonAssocRing R] {n r : R} : bit1 n * r = (2 : ℤ) • (n * r) + r := by
-  dsimp [bit1]
-  rw [add_mul, bit0_mul, one_mul]
-#align bit1_mul bit1_mul
-
-theorem mul_bit1 [NonAssocRing R] {n r : R} : r * bit1 n = (2 : ℤ) • (r * n) + r := by
-  dsimp [bit1]
-  rw [mul_add, mul_bit0, mul_one]
-#align mul_bit1 mul_bit1
-
-end bit0_bit1
-
-/-- Note this holds in marginally more generality than `Int.cast_mul` -/
-theorem Int.cast_mul_eq_zsmul_cast [AddCommGroupWithOne α] :
-    ∀ m n, ((m * n : ℤ) : α) = m • (n : α) :=
-  fun m =>
-  Int.inductionOn' m 0 (by simp) (fun k _ ih n => by simp [add_mul, add_zsmul, ih]) fun k _ ih n =>
-    by simp [sub_mul, sub_zsmul, ih, ← sub_eq_add_neg]
-#align int.cast_mul_eq_zsmul_cast Int.cast_mul_eq_zsmul_cast
-
 section OrderedSemiring
 
 variable [OrderedSemiring R] {a : R}
@@ -98,130 +62,3 @@ set_option linter.uppercaseLean3 false in
 #align sign_cases_of_C_mul_pow_nonneg sign_cases_of_C_mul_pow_nonneg
 
 end LinearOrderedSemiring
-
-namespace Int
-
-lemma natAbs_sq (x : ℤ) : (x.natAbs : ℤ) ^ 2 = x ^ 2 := by rw [sq, Int.natAbs_mul_self', sq]
-#align int.nat_abs_sq Int.natAbs_sq
-
-alias natAbs_pow_two := natAbs_sq
-#align int.nat_abs_pow_two Int.natAbs_pow_two
-
-theorem natAbs_le_self_sq (a : ℤ) : (Int.natAbs a : ℤ) ≤ a ^ 2 := by
-  rw [← Int.natAbs_sq a, sq]
-  norm_cast
-  apply Nat.le_mul_self
-#align int.abs_le_self_sq Int.natAbs_le_self_sq
-
-alias natAbs_le_self_pow_two := natAbs_le_self_sq
-
-theorem le_self_sq (b : ℤ) : b ≤ b ^ 2 :=
-  le_trans le_natAbs (natAbs_le_self_sq _)
-#align int.le_self_sq Int.le_self_sq
-
-alias le_self_pow_two := le_self_sq
-#align int.le_self_pow_two Int.le_self_pow_two
-
-end Int
-
-variable (M G A)
-
-/-- Additive homomorphisms from `ℤ` are defined by the image of `1`. -/
-def zmultiplesHom [AddGroup A] :
-    A ≃ (ℤ →+ A) where
-  toFun x :=
-  { toFun := fun n => n • x
-    map_zero' := zero_zsmul x
-    map_add' := fun _ _ => add_zsmul _ _ _ }
-  invFun f := f 1
-  left_inv := one_zsmul
-  right_inv f := AddMonoidHom.ext_int <| one_zsmul (f 1)
-#align zmultiples_hom zmultiplesHom
-
-/-- Monoid homomorphisms from `Multiplicative ℤ` are defined by the image
-of `Multiplicative.ofAdd 1`. -/
-def zpowersHom [Group G] : G ≃ (Multiplicative ℤ →* G) :=
-  Additive.ofMul.trans <| (zmultiplesHom _).trans <| AddMonoidHom.toMultiplicative''
-#align zpowers_hom zpowersHom
-
-attribute [to_additive existing zmultiplesHom] zpowersHom
-
-variable {M G A}
-
-theorem zpowersHom_apply [Group G] (x : G) (n : Multiplicative ℤ) :
-    zpowersHom G x n = x ^ (Multiplicative.toAdd n) :=
-  rfl
-#align zpowers_hom_apply zpowersHom_apply
-
-theorem zpowersHom_symm_apply [Group G] (f : Multiplicative ℤ →* G) :
-    (zpowersHom G).symm f = f (Multiplicative.ofAdd 1) :=
-  rfl
-#align zpowers_hom_symm_apply zpowersHom_symm_apply
-
--- todo: can `to_additive` generate the following lemmas automatically?
-
-theorem zmultiplesHom_apply [AddGroup A] (x : A) (n : ℤ) : zmultiplesHom A x n = n • x :=
-  rfl
-#align zmultiples_hom_apply zmultiplesHom_apply
-
-attribute [to_additive existing (attr := simp) zmultiplesHom_apply] zpowersHom_apply
-
-theorem zmultiplesHom_symm_apply [AddGroup A] (f : ℤ →+ A) : (zmultiplesHom A).symm f = f 1 :=
-  rfl
-#align zmultiples_hom_symm_apply zmultiplesHom_symm_apply
-
-attribute [to_additive existing (attr := simp) zmultiplesHom_symm_apply] zpowersHom_symm_apply
-
-theorem MonoidHom.apply_mint [Group M] (f : Multiplicative ℤ →* M) (n : Multiplicative ℤ) :
-    f n = f (Multiplicative.ofAdd 1) ^ (Multiplicative.toAdd n) := by
-  rw [← zpowersHom_symm_apply, ← zpowersHom_apply, Equiv.apply_symm_apply]
-#align monoid_hom.apply_mint MonoidHom.apply_mint
-
-/-! `MonoidHom.ext_mint` is defined in `Data.Int.Cast` -/
-
-/-! `AddMonoidHom.ext_nat` is defined in `Data.Nat.Cast` -/
-
-theorem AddMonoidHom.apply_int [AddGroup M] (f : ℤ →+ M) (n : ℤ) : f n = n • f 1 := by
-  rw [← zmultiplesHom_symm_apply, ← zmultiplesHom_apply, Equiv.apply_symm_apply]
-#align add_monoid_hom.apply_int AddMonoidHom.apply_int
-
-/-! `AddMonoidHom.ext_int` is defined in `Data.Int.Cast` -/
-
-variable (M G A)
-
-/-- If `M` is commutative, `zpowersHom` is a multiplicative equivalence. -/
-def zpowersMulHom [CommGroup G] : G ≃* (Multiplicative ℤ →* G) :=
-  { zpowersHom G with map_mul' := fun a b => MonoidHom.ext fun n => by simp [mul_zpow] }
-#align zpowers_mul_hom zpowersMulHom
-
-/-- If `M` is commutative, `zmultiplesHom` is an additive equivalence. -/
-def zmultiplesAddHom [AddCommGroup A] : A ≃+ (ℤ →+ A) :=
-  { zmultiplesHom A with map_add' := fun a b => AddMonoidHom.ext fun n => by simp [zsmul_add] }
-#align zmultiples_add_hom zmultiplesAddHom
-
-variable {M G A}
-
-@[simp]
-theorem zpowersMulHom_apply [CommGroup G] (x : G) (n : Multiplicative ℤ) :
-    zpowersMulHom G x n = x ^ (Multiplicative.toAdd n) :=
-  rfl
-#align zpowers_mul_hom_apply zpowersMulHom_apply
-
-@[simp]
-theorem zpowersMulHom_symm_apply [CommGroup G] (f : Multiplicative ℤ →* G) :
-    (zpowersMulHom G).symm f = f (Multiplicative.ofAdd 1) :=
-  rfl
-#align zpowers_mul_hom_symm_apply zpowersMulHom_symm_apply
-
-@[simp]
-theorem zmultiplesAddHom_apply [AddCommGroup A] (x : A) (n : ℤ) :
-    zmultiplesAddHom A x n = n • x :=
-  rfl
-#align zmultiples_add_hom_apply zmultiplesAddHom_apply
-
-@[simp]
-theorem zmultiplesAddHom_symm_apply [AddCommGroup A] (f : ℤ →+ A) :
-    (zmultiplesAddHom A).symm f = f 1 :=
-  rfl
-#align zmultiples_add_hom_symm_apply zmultiplesAddHom_symm_apply
-@[simp] theorem pow_eq {m : ℤ} {n : ℕ} : m.pow n = m ^ n := by simp

Mathlib/Data/Int/Cast/Lemmas.lean

@@ -389,6 +389,86 @@ theorem ext_int' [MonoidWithZero α] [MonoidWithZeroHomClass F ℤ α] {f g : F}
     this
 #align ext_int' ext_int'
 
+section Group
+variable (α) [Group α] [AddGroup α]
+
+/-- Additive homomorphisms from `ℤ` are defined by the image of `1`. -/
+def zmultiplesHom : α ≃ (ℤ →+ α) where
+  toFun x :=
+  { toFun := fun n => n • x
+    map_zero' := zero_zsmul x
+    map_add' := fun _ _ => add_zsmul _ _ _ }
+  invFun f := f 1
+  left_inv := one_zsmul
+  right_inv f := AddMonoidHom.ext_int <| one_zsmul (f 1)
+#align zmultiples_hom zmultiplesHom
+#align powers_hom powersHom
+
+/-- Monoid homomorphisms from `Multiplicative ℤ` are defined by the image
+of `Multiplicative.ofAdd 1`. -/
+@[to_additive existing zmultiplesHom]
+def zpowersHom : α ≃ (Multiplicative ℤ →* α) :=
+  ofMul.trans <| (zmultiplesHom _).trans <| AddMonoidHom.toMultiplicative''
+#align zpowers_hom zpowersHom
+
+lemma zmultiplesHom_apply (x : α) (n : ℤ) : zmultiplesHom α x n = n • x := rfl
+#align zmultiples_hom_apply zmultiplesHom_apply
+
+lemma zmultiplesHom_symm_apply (f : ℤ →+ α) : (zmultiplesHom α).symm f = f 1 := rfl
+#align zmultiples_hom_symm_apply zmultiplesHom_symm_apply
+
+@[to_additive existing (attr := simp) zmultiplesHom_apply]
+lemma zpowersHom_apply (x : α) (n : Multiplicative ℤ) :zpowersHom α x n = x ^ toAdd n := rfl
+#align zpowers_hom_apply zpowersHom_apply
+
+@[to_additive existing (attr := simp) zmultiplesHom_symm_apply]
+lemma zpowersHom_symm_apply (f : Multiplicative ℤ →* α) :
+    (zpowersHom α).symm f = f (ofAdd 1) := rfl
+#align zpowers_hom_symm_apply zpowersHom_symm_apply
+
+lemma MonoidHom.apply_mint (f : Multiplicative ℤ →* α) (n : Multiplicative ℤ) :
+    f n = f (ofAdd 1) ^ (toAdd n) := by
+  rw [← zpowersHom_symm_apply, ← zpowersHom_apply, Equiv.apply_symm_apply]
+#align monoid_hom.apply_mint MonoidHom.apply_mint
+
+lemma AddMonoidHom.apply_int (f : ℤ →+ α) (n : ℤ) : f n = n • f 1 := by
+  rw [← zmultiplesHom_symm_apply, ← zmultiplesHom_apply, Equiv.apply_symm_apply]
+#align add_monoid_hom.apply_int AddMonoidHom.apply_int
+
+end Group
+
+section CommGroup
+variable (α) [CommGroup α] [AddCommGroup α]
+
+/-- If `α` is commutative, `zmultiplesHom` is an additive equivalence. -/
+def zmultiplesAddHom : α ≃+ (ℤ →+ α) :=
+  { zmultiplesHom α with map_add' := fun a b => AddMonoidHom.ext fun n => by simp [zsmul_add] }
+#align zmultiples_add_hom zmultiplesAddHom
+
+/-- If `α` is commutative, `zpowersHom` is a multiplicative equivalence. -/
+def zpowersMulHom : α ≃* (Multiplicative ℤ →* α) :=
+  { zpowersHom α with map_mul' := fun a b => MonoidHom.ext fun n => by simp [mul_zpow] }
+#align zpowers_mul_hom zpowersMulHom
+
+variable {α}
+
+@[simp]
+lemma zpowersMulHom_apply (x : α) (n : Multiplicative ℤ) : zpowersMulHom α x n = x ^ toAdd n := rfl
+#align zpowers_mul_hom_apply zpowersMulHom_apply
+
+@[simp]
+lemma zpowersMulHom_symm_apply (f : Multiplicative ℤ →* α) :
+    (zpowersMulHom α).symm f = f (ofAdd 1) := rfl
+#align zpowers_mul_hom_symm_apply zpowersMulHom_symm_apply
+
+@[simp] lemma zmultiplesAddHom_apply (x : α) (n : ℤ) : zmultiplesAddHom α x n = n • x := rfl
+#align zmultiples_add_hom_apply zmultiplesAddHom_apply
+
+@[simp] lemma zmultiplesAddHom_symm_apply (f : ℤ →+ α) : (zmultiplesAddHom α).symm f = f 1 := rfl
+#align zmultiples_add_hom_symm_apply zmultiplesAddHom_symm_apply
+
+end CommGroup
+
 section NonAssocRing
 
 variable [NonAssocRing α] [NonAssocRing β]

Mathlib/Data/Int/Dvd/Basic.lean

@@ -32,11 +32,11 @@ theorem coe_nat_dvd {m n : ℕ} : (↑m : ℤ) ∣ ↑n ↔ m ∣ n :=
 #align int.coe_nat_dvd Int.coe_nat_dvd
 
 theorem coe_nat_dvd_left {n : ℕ} {z : ℤ} : (↑n : ℤ) ∣ z ↔ n ∣ z.natAbs := by
-  rcases natAbs_eq z with (eq | eq) <;> rw [eq] <;> simp [← coe_nat_dvd]
+  rcases natAbs_eq z with (eq | eq) <;> rw [eq] <;> simp [← coe_nat_dvd, Int.dvd_neg]
 #align int.coe_nat_dvd_left Int.coe_nat_dvd_left
 
 theorem coe_nat_dvd_right {n : ℕ} {z : ℤ} : z ∣ (↑n : ℤ) ↔ z.natAbs ∣ n := by
-  rcases natAbs_eq z with (eq | eq) <;> rw [eq] <;> simp [← coe_nat_dvd]
+  rcases natAbs_eq z with (eq | eq) <;> rw [eq] <;> simp [← coe_nat_dvd, Int.neg_dvd]
 #align int.coe_nat_dvd_right Int.coe_nat_dvd_right
 
 #align int.le_of_dvd Int.le_of_dvd

Mathlib/Data/Int/Order/Basic.lean

@@ -3,12 +3,11 @@ Copyright (c) 2016 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad
 -/
-
-import Mathlib.Data.Int.Basic
+import Mathlib.Algebra.Divisibility.Basic
 import Mathlib.Algebra.Order.Group.Abs
 import Mathlib.Algebra.Order.Ring.CharZero
-import Mathlib.Algebra.Divisibility.Basic
-import Mathlib.Data.Int.Defs
+import Mathlib.Data.Int.Basic
+import Mathlib.Data.Nat.Order.Basic
 
 #align_import data.int.order.basic from "leanprover-community/mathlib"@"e8638a0fcaf73e4500469f368ef9494e495099b3"
 
@@ -29,7 +28,7 @@ This file contains:
   induction on numbers less than `b`.
 -/
 
-open Nat
+open Function Nat
 
 namespace Int
 
@@ -73,6 +72,26 @@ theorem sign_mul_abs (a : ℤ) : sign a * |a| = a := by
   rw [abs_eq_natAbs, sign_mul_natAbs a]
 #align int.sign_mul_abs Int.sign_mul_abs
 
+lemma natAbs_sq (x : ℤ) : (x.natAbs : ℤ) ^ 2 = x ^ 2 := by rw [sq, Int.natAbs_mul_self', sq]
+#align int.nat_abs_sq Int.natAbs_sq
+
+alias natAbs_pow_two := natAbs_sq
+#align int.nat_abs_pow_two Int.natAbs_pow_two
+
+lemma natAbs_le_self_sq (a : ℤ) : (Int.natAbs a : ℤ) ≤ a ^ 2 := by
+  rw [← Int.natAbs_sq a, sq]
+  norm_cast
+  apply Nat.le_mul_self
+#align int.abs_le_self_sq Int.natAbs_le_self_sq
+
+alias natAbs_le_self_pow_two := natAbs_le_self_sq
+
+lemma le_self_sq (b : ℤ) : b ≤ b ^ 2 := le_trans le_natAbs (natAbs_le_self_sq _)
+#align int.le_self_sq Int.le_self_sq
+
+alias le_self_pow_two := le_self_sq
+#align int.le_self_pow_two Int.le_self_pow_two
+
 theorem coe_nat_eq_zero {n : ℕ} : (n : ℤ) = 0 ↔ n = 0 :=
   Nat.cast_eq_zero
 #align int.coe_nat_eq_zero Int.coe_nat_eq_zero
@@ -95,6 +114,14 @@ theorem sign_add_eq_of_sign_eq : ∀ {m n : ℤ}, m.sign = n.sign → (m + n).si
   apply Int.add_pos <;> · exact zero_lt_one.trans_le (le_add_of_nonneg_left <| coe_nat_nonneg _)
 #align int.sign_add_eq_of_sign_eq Int.sign_add_eq_of_sign_eq
 
+/-- Note this holds in marginally more generality than `Int.cast_mul` -/
+lemma cast_mul_eq_zsmul_cast {α : Type*} [AddCommGroupWithOne α] :
+    ∀ m n : ℤ, ↑(m * n) = m • (n : α) :=
+  fun m ↦ Int.induction_on m (by simp) (fun _ ih ↦ by simp [add_mul, add_zsmul, ih]) fun _ ih ↦ by
+    simp only [sub_mul, one_mul, cast_sub, ih, sub_zsmul, one_zsmul, ← sub_eq_add_neg, forall_const]
+#align int.cast_mul_eq_zsmul_cast Int.cast_mul_eq_zsmul_cast
+
+
 /-! ### succ and pred -/
 
 
@@ -551,5 +578,37 @@ theorem toNat_sub_of_le {a b : ℤ} (h : b ≤ a) : (toNat (a - b) : ℤ) = a -
 
 end Int
 
+section bit0_bit1
+variable {R}
+set_option linter.deprecated false
+
+-- The next four lemmas allow us to replace multiplication by a numeral with a `zsmul` expression.
+
+section NonUnitalNonAssocRing
+variable [NonUnitalNonAssocRing R] (n r : R)
+
+lemma bit0_mul : bit0 n * r = (2 : ℤ) • (n * r) := by
+  rw [bit0, add_mul, ← one_add_one_eq_two, add_zsmul, one_zsmul]
+#align bit0_mul bit0_mul
+
+lemma mul_bit0 : r * bit0 n = (2 : ℤ) • (r * n) := by
+  rw [bit0, mul_add, ← one_add_one_eq_two, add_zsmul, one_zsmul]
+#align mul_bit0 mul_bit0
+
+end NonUnitalNonAssocRing
+
+section NonAssocRing
+variable [NonAssocRing R] (n r : R)
+
+lemma bit1_mul : bit1 n * r = (2 : ℤ) • (n * r) + r := by rw [bit1, add_mul, bit0_mul, one_mul]
+#align bit1_mul bit1_mul
+
+lemma mul_bit1 [NonAssocRing R] {n r : R} : r * bit1 n = (2 : ℤ) • (r * n) + r := by
+  rw [bit1, mul_add, mul_bit0, mul_one]
+#align mul_bit1 mul_bit1
+
+end NonAssocRing
+end bit0_bit1
+
 -- We should need only a minimal development of sets in order to get here.
 assert_not_exists Set.range