feat(data/nat/gcd, ring_theory/int/basic): add some basic lemmas (#7314)

This also reduces the dependency on definitional equalities a but

src/data/nat/gcd.lean

@@ -212,10 +212,14 @@ See also `nat.coprime_of_dvd` and `nat.coprime_of_dvd'` to prove `nat.coprime m
 
 instance (m n : ℕ) : decidable (coprime m n) := by unfold coprime; apply_instance
 
+theorem coprime_iff_gcd_eq_one {m n : ℕ} : coprime m n ↔ gcd m n = 1 := iff.rfl
+
 theorem coprime.gcd_eq_one {m n : ℕ} : coprime m n → gcd m n = 1 := id
 
 theorem coprime.symm {m n : ℕ} : coprime n m → coprime m n := (gcd_comm m n).trans
 
+theorem coprime_comm {m n : ℕ} : coprime n m ↔ coprime m n := ⟨coprime.symm, coprime.symm⟩
+
 theorem coprime.dvd_of_dvd_mul_right {m n k : ℕ} (H1 : coprime k n) (H2 : k ∣ m * n) : k ∣ m :=
 let t := dvd_gcd (dvd_mul_left k m) H2 in
 by rwa [gcd_mul_left, H1.gcd_eq_one, mul_one] at t
@@ -245,12 +249,11 @@ by rw [mul_comm n k, H.gcd_mul_left_cancel_right n]
 
 theorem coprime_div_gcd_div_gcd {m n : ℕ} (H : 0 < gcd m n) :
   coprime (m / gcd m n) (n / gcd m n) :=
-by delta coprime; rw [gcd_div (gcd_dvd_left m n) (gcd_dvd_right m n), nat.div_self H]
+by rw [coprime_iff_gcd_eq_one, gcd_div (gcd_dvd_left m n) (gcd_dvd_right m n), nat.div_self H]
 
 theorem not_coprime_of_dvd_of_dvd {m n d : ℕ} (dgt1 : 1 < d) (Hm : d ∣ m) (Hn : d ∣ n) :
   ¬ coprime m n :=
-λ (co : gcd m n = 1),
-not_lt_of_ge (le_of_dvd zero_lt_one $ by rw ←co; exact dvd_gcd Hm Hn) dgt1
+λ co, not_lt_of_ge (le_of_dvd zero_lt_one $ by rw [←co.gcd_eq_one]; exact dvd_gcd Hm Hn) dgt1
 
 theorem exists_coprime {m n : ℕ} (H : 0 < gcd m n) :
   ∃ m' n', coprime m' n' ∧ m = m' * gcd m n ∧ n = n' * gcd m n :=
@@ -304,10 +307,10 @@ theorem coprime.coprime_div_right {m n a : ℕ} (cmn : coprime m n) (dvd : a ∣
 
 lemma coprime_mul_iff_left {k m n : ℕ} : coprime (m * n) k ↔ coprime m k ∧ coprime n k :=
 ⟨λ h, ⟨coprime.coprime_mul_right h, coprime.coprime_mul_left h⟩,
-  λ ⟨h, _⟩, by rwa [coprime, coprime.gcd_mul_left_cancel n h]⟩
+  λ ⟨h, _⟩, by rwa [coprime_iff_gcd_eq_one, coprime.gcd_mul_left_cancel n h]⟩
 
 lemma coprime_mul_iff_right {k m n : ℕ} : coprime k (m * n) ↔ coprime k m ∧ coprime k n :=
-by { repeat { rw [coprime, nat.gcd_comm k] }, exact coprime_mul_iff_left }
+by simpa only [coprime_comm] using coprime_mul_iff_left
 
 lemma coprime.gcd_left (k : ℕ) {m n : ℕ} (hmn : coprime m n) : coprime (gcd k m) n :=
 hmn.coprime_dvd_left $ gcd_dvd_right k m

src/ring_theory/int/basic.lean

@@ -153,6 +153,8 @@ begin
     simp only [neg_mul_eq_neg_mul_symm, one_mul] }
 end
 
+lemma gcd_eq_nat_abs {a b : ℤ} : int.gcd a b = nat.gcd a.nat_abs b.nat_abs := rfl
+
 lemma gcd_eq_one_iff_coprime {a b : ℤ} : int.gcd a b = 1 ↔ is_coprime a b :=
 begin
   split,
@@ -162,21 +164,19 @@ begin
     use [(nat.gcd_a (int.nat_abs a) (int.nat_abs b)) * ua,
         (nat.gcd_b (int.nat_abs a) (int.nat_abs b)) * ub],
     rw [mul_assoc, ← ha, mul_assoc, ← hb, mul_comm, mul_comm _ (int.nat_abs b : ℤ),
-      ← nat.gcd_eq_gcd_ab],
-    norm_cast,
-    exact hg },
+      ← nat.gcd_eq_gcd_ab, ←gcd_eq_nat_abs, hg, int.coe_nat_one] },
   { rintro ⟨r, s, h⟩,
     by_contradiction hg,
     obtain ⟨p, ⟨hp, ha, hb⟩⟩ := nat.prime.not_coprime_iff_dvd.mp hg,
     apply nat.prime.not_dvd_one hp,
-    apply coe_nat_dvd.mp,
-    change (p : ℤ) ∣ 1,
-    rw [← h],
+    rw [←coe_nat_dvd, int.coe_nat_one, ← h],
     exact dvd_add (dvd_mul_of_dvd_right (coe_nat_dvd_left.mpr ha) _)
-      (dvd_mul_of_dvd_right (coe_nat_dvd_left.mpr hb) _),
-  }
+      (dvd_mul_of_dvd_right (coe_nat_dvd_left.mpr hb) _) }
 end
 
+lemma coprime_iff_nat_coprime {a b : ℤ} : is_coprime a b ↔ nat.coprime a.nat_abs b.nat_abs :=
+by rw [←gcd_eq_one_iff_coprime, nat.coprime_iff_gcd_eq_one, gcd_eq_nat_abs]
+
 lemma sqr_of_gcd_eq_one {a b c : ℤ} (h : int.gcd a b = 1) (heq : a * b = c ^ 2) :
   ∃ (a0 : ℤ), a = a0 ^ 2 ∨ a = - (a0 ^ 2) :=
 begin