chore(data/int/gcd): streamline imports (#16811)

The file on gcds of integers is fundamentally very elementary, but it contained two lemmas about prime numbers, and `data.nat.prime` seems to import everything (modules! half the order library!).



Co-authored-by: Andrew Yang <the.erd.one@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
Co-authored-by: Junyan Xu <junyanxumath@gmail.com>

src/combinatorics/pigeonhole.lean

@@ -6,6 +6,7 @@ Authors: Kyle Miller, Yury Kudryashov
 import data.set.finite
 import data.nat.modeq
 import algebra.big_operators.order
+import algebra.module.basic
 
 /-!
 # Pigeonhole principles

src/data/int/gcd.lean

@@ -3,8 +3,8 @@ Copyright (c) 2018 Guy Leroy. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sangwoo Jo (aka Jason), Guy Leroy, Johannes Hölzl, Mario Carneiro
 -/
-import data.nat.prime
-import data.int.order
+import data.nat.gcd.basic
+import tactic.norm_num
 
 /-!
 # Extended GCD and divisibility over ℤ
@@ -160,31 +160,12 @@ begin
     ... = nat_abs a / nat_abs b : by rw int.div_mul_cancel H,
 end
 
-lemma succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul {p : ℕ} (p_prime : nat.prime p) {m n : ℤ} {k l : ℕ}
-      (hpm : ↑(p ^ k) ∣ m)
-      (hpn : ↑(p ^ l) ∣ n) (hpmn : ↑(p ^ (k+l+1)) ∣ m*n) : ↑(p ^ (k+1)) ∣ m ∨ ↑(p ^ (l+1)) ∣ n :=
-have hpm' : p ^ k ∣ m.nat_abs, from int.coe_nat_dvd.1 $ int.dvd_nat_abs.2 hpm,
-have hpn' : p ^ l ∣ n.nat_abs, from int.coe_nat_dvd.1 $ int.dvd_nat_abs.2 hpn,
-have hpmn' : (p ^ (k+l+1)) ∣ m.nat_abs*n.nat_abs,
-  by rw ←int.nat_abs_mul; apply (int.coe_nat_dvd.1 $ int.dvd_nat_abs.2 hpmn),
-let hsd := nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul p_prime hpm' hpn' hpmn' in
-hsd.elim
-  (λ hsd1, or.inl begin apply int.dvd_nat_abs.1, apply int.coe_nat_dvd.2 hsd1 end)
-  (λ hsd2, or.inr begin apply int.dvd_nat_abs.1, apply int.coe_nat_dvd.2 hsd2 end)
-
 theorem dvd_of_mul_dvd_mul_left {i j k : ℤ} (k_non_zero : k ≠ 0) (H : k * i ∣ k * j) : i ∣ j :=
 dvd.elim H (λl H1, by rw mul_assoc at H1; exact ⟨_, mul_left_cancel₀ k_non_zero H1⟩)
 
 theorem dvd_of_mul_dvd_mul_right {i j k : ℤ} (k_non_zero : k ≠ 0) (H : i * k ∣ j * k) : i ∣ j :=
 by rw [mul_comm i k, mul_comm j k] at H; exact dvd_of_mul_dvd_mul_left k_non_zero H
 
-lemma prime.dvd_nat_abs_of_coe_dvd_sq {p : ℕ} (hp : p.prime) (k : ℤ) (h : ↑p ∣ k ^ 2) :
-  p ∣ k.nat_abs :=
-begin
-  apply @nat.prime.dvd_of_dvd_pow _ _ 2 hp,
-  rwa [sq, ← nat_abs_mul, ← coe_nat_dvd_left, ← sq]
-end
-
 /-- ℤ specific version of least common multiple. -/
 def lcm (i j : ℤ) : ℕ := nat.lcm (nat_abs i) (nat_abs j)
 

src/data/int/nat_prime.lean

@@ -17,4 +17,23 @@ lemma not_prime_of_int_mul {a b : ℤ} {c : ℕ}
   (ha : 1 < a.nat_abs) (hb : 1 < b.nat_abs) (hc : a*b = (c : ℤ)) : ¬ nat.prime c :=
 not_prime_mul' (nat_abs_mul_nat_abs_eq hc) ha hb
 
+lemma succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul {p : ℕ} (p_prime : nat.prime p) {m n : ℤ} {k l : ℕ}
+      (hpm : ↑(p ^ k) ∣ m)
+      (hpn : ↑(p ^ l) ∣ n) (hpmn : ↑(p ^ (k+l+1)) ∣ m*n) : ↑(p ^ (k+1)) ∣ m ∨ ↑(p ^ (l+1)) ∣ n :=
+have hpm' : p ^ k ∣ m.nat_abs, from int.coe_nat_dvd.1 $ int.dvd_nat_abs.2 hpm,
+have hpn' : p ^ l ∣ n.nat_abs, from int.coe_nat_dvd.1 $ int.dvd_nat_abs.2 hpn,
+have hpmn' : (p ^ (k+l+1)) ∣ m.nat_abs*n.nat_abs,
+  by rw ←int.nat_abs_mul; apply (int.coe_nat_dvd.1 $ int.dvd_nat_abs.2 hpmn),
+let hsd := nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul p_prime hpm' hpn' hpmn' in
+hsd.elim
+  (λ hsd1, or.inl begin apply int.dvd_nat_abs.1, apply int.coe_nat_dvd.2 hsd1 end)
+  (λ hsd2, or.inr begin apply int.dvd_nat_abs.1, apply int.coe_nat_dvd.2 hsd2 end)
+
+lemma prime.dvd_nat_abs_of_coe_dvd_sq {p : ℕ} (hp : p.prime) (k : ℤ) (h : ↑p ∣ k ^ 2) :
+  p ∣ k.nat_abs :=
+begin
+  apply @nat.prime.dvd_of_dvd_pow _ _ 2 hp,
+  rwa [sq, ← nat_abs_mul, ← coe_nat_dvd_left, ← sq]
+end
+
 end int

src/data/nat/modeq.lean

@@ -309,13 +309,13 @@ lemma modeq_and_modeq_iff_modeq_mul {a b m n : ℕ} (hmn : coprime m n) :
 λ h, ⟨h.of_modeq_mul_right _, h.of_modeq_mul_left _⟩⟩
 
 lemma coprime_of_mul_modeq_one (b : ℕ) {a n : ℕ} (h : a * b ≡ 1 [MOD n]) : coprime a n :=
-nat.coprime_of_dvd' (λ k kp ⟨ka, hka⟩ ⟨kb, hkb⟩, int.coe_nat_dvd.1 begin
-  rw [hka, hkb, modeq_iff_dvd] at h,
-  cases h with z hz,
-  rw [sub_eq_iff_eq_add] at hz,
-  rw [hz, int.coe_nat_mul, mul_assoc, mul_assoc, int.coe_nat_mul, ← mul_add],
-  exact dvd_mul_right _ _,
-end)
+begin
+  obtain ⟨g, hh⟩ := nat.gcd_dvd_right a n,
+  rw [nat.coprime_iff_gcd_eq_one, ← nat.dvd_one, ← nat.modeq_zero_iff_dvd],
+  calc 1 ≡ a * b [MOD a.gcd n] : nat.modeq.of_modeq_mul_right g (hh.subst h).symm
+  ... ≡ 0 * b [MOD a.gcd n] : (nat.modeq_zero_iff_dvd.mpr (nat.gcd_dvd_left _ _)).mul_right b
+  ... = 0 : by rw zero_mul,
+end
 
 @[simp] lemma mod_mul_right_mod (a b c : ℕ) : a % (b * c) % b = a % b :=
 (mod_modeq _ _).of_modeq_mul_right _

src/data/nat/parity.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Benjamin Davidson
 -/
 import data.nat.modeq
+import data.nat.prime
 import algebra.parity
 
 /-!

src/number_theory/pythagorean_triples.lean

@@ -9,6 +9,7 @@ import algebra.group_with_zero.power
 import tactic.ring
 import tactic.ring_exp
 import tactic.field_simp
+import data.int.nat_prime
 import data.zmod.basic
 
 /-!

src/ring_theory/int/basic.lean

@@ -3,6 +3,7 @@ Copyright (c) 2018 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Jens Wagemaker, Aaron Anderson
 -/
+import data.nat.prime
 import ring_theory.coprime.basic
 import ring_theory.principal_ideal_domain