feat(data/int): various lemmas (#10862)

Author: Ruben-VandeVelde

src/data/int/basic.lean

@@ -884,6 +884,9 @@ lemma nat_abs_sign_of_nonzero {z : ℤ} (hz : z ≠ 0) :
   z.sign.nat_abs = 1 :=
 by rw [int.nat_abs_sign, if_neg hz]
 
+lemma abs_sign_of_nonzero {z : ℤ} (hz : z ≠ 0) : |z.sign| = 1 :=
+by rw [abs_eq_nat_abs, nat_abs_sign_of_nonzero hz, int.coe_nat_one]
+
 lemma sign_coe_nat_of_nonzero {n : ℕ} (hn : n ≠ 0) :
   int.sign n = 1 :=
 begin
@@ -1231,6 +1234,13 @@ end
 theorem is_unit_iff_nat_abs_eq {n : ℤ} : is_unit n ↔ n.nat_abs = 1 :=
 by simp [nat_abs_eq_iff, is_unit_iff]
 
+lemma is_unit_iff_abs_eq {x : ℤ} : is_unit x ↔ abs x = 1 :=
+by rw [is_unit_iff_nat_abs_eq, abs_eq_nat_abs, ←int.coe_nat_one, coe_nat_inj']
+
+@[norm_cast]
+lemma of_nat_is_unit {n : ℕ} : is_unit (n : ℤ) ↔ is_unit n :=
+by rw [nat.is_unit_iff, is_unit_iff_nat_abs_eq, nat_abs_of_nat]
+
 lemma units_inv_eq_self (u : units ℤ) : u⁻¹ = u :=
 (units_eq_one_or u).elim (λ h, h.symm ▸ rfl) (λ h, h.symm ▸ rfl)
 

src/data/int/parity.lean

@@ -200,6 +200,26 @@ coe_nat_dvd_left.symm
 @[simp] theorem nat_abs_odd : odd n.nat_abs ↔ odd n :=
 by rw [odd_iff_not_even, nat.odd_iff_not_even, nat_abs_even]
 
+lemma four_dvd_add_or_sub_of_odd {a b : ℤ} (ha : odd a) (hb : odd b) : 4 ∣ a + b ∨ 4 ∣ a - b :=
+begin
+  obtain ⟨m, rfl⟩ := ha,
+  obtain ⟨n, rfl⟩ := hb,
+  obtain h|h := int.even_or_odd (m + n),
+  { right,
+    rw [int.even_add, ←int.even_sub] at h,
+    obtain ⟨k, hk⟩ := h,
+    convert dvd_mul_right 4 k,
+    rw [eq_add_of_sub_eq hk, mul_add, add_assoc, add_sub_cancel, ←mul_assoc],
+    norm_num },
+  { left,
+    obtain ⟨k, hk⟩ := h,
+    convert dvd_mul_right 4 (k + 1),
+    rw [eq_sub_of_add_eq hk, add_right_comm, ←add_sub, mul_add, mul_sub, add_assoc, add_assoc,
+      sub_add, add_assoc, ←sub_sub (2 * n), sub_self, zero_sub, sub_neg_eq_add, ←mul_assoc,
+      mul_add],
+    norm_num },
+end
+
 -- Here are examples of how `parity_simps` can be used with `int`.
 
 example (m n : ℤ) (h : even m) : ¬ even (n + 3) ↔ even (m^2 + m + n) :=

src/ring_theory/int/basic.lean

@@ -316,6 +316,12 @@ begin
     exact (or_self _).mp ((nat.prime.dvd_mul hp).mp hpp)}
 end
 
+lemma int.exists_prime_and_dvd {n : ℤ} (n2 : 2 ≤ n.nat_abs) : ∃ p, prime p ∧ p ∣ n :=
+begin
+  obtain ⟨p, pp, pd⟩ := nat.exists_prime_and_dvd n2,
+  exact ⟨p, nat.prime_iff_prime_int.mp pp, int.coe_nat_dvd_left.mpr pd⟩,
+end
+
 open unique_factorization_monoid
 
 theorem nat.factors_eq {n : ℕ} : normalized_factors n = n.factors :=