case mp
a b : ℤ
⊢ gcd a b = 1 → IsCoprime a b

case mpr
a b : ℤ
⊢ IsCoprime a b → gcd a b = 1
a b : ℤ
⊢ gcd a b = 1 ↔ IsCoprime a b
constructor
case mp
a b : ℤ
hg : gcd a b = 1
⊢ IsCoprime a b
case mp
a b : ℤ
⊢ gcd a b = 1 → IsCoprime a b
intro hg
case mp.intro.intro
a b : ℤ
hg : gcd a b = 1
ua : ℤ
ha : ↑(natAbs a) = ua * a
⊢ IsCoprime a b
case mp
a b : ℤ
hg : gcd a b = 1
⊢ IsCoprime a b
obtain ⟨ua, -, ha⟩ := exists_unit_of_abs a
case mp.intro.intro.intro.intro
a b : ℤ
hg : gcd a b = 1
ua : ℤ
ha : ↑(natAbs a) = ua * a
ub : ℤ
hb : ↑(natAbs b) = ub * b
⊢ IsCoprime a b
case mp.intro.intro
a b : ℤ
hg : gcd a b = 1
ua : ℤ
ha : ↑(natAbs a) = ua * a
⊢ IsCoprime a b
obtain ⟨ub, -, hb⟩ := exists_unit_of_abs b
case mp.intro.intro.intro.intro
a b : ℤ
hg : gcd a b = 1
ua : ℤ
ha : ↑(natAbs a) = ua * a
ub : ℤ
hb : ↑(natAbs b) = ub * b
⊢ Nat.gcdA (natAbs a) (natAbs b) * ua * a + Nat.gcdB (natAbs a) (natAbs b) * ub * b = 1
case mp.intro.intro.intro.intro
a b : ℤ
hg : gcd a b = 1
ua : ℤ
ha : ↑(natAbs a) = ua * a
ub : ℤ
hb : ↑(natAbs b) = ub * b
⊢ IsCoprime a b
use Nat.gcdA (Int.natAbs a) (Int.natAbs b) * ua, Nat.gcdB (Int.natAbs a) (Int.natAbs b) * ub
no goals
case mp.intro.intro.intro.intro
a b : ℤ
hg : gcd a b = 1
ua : ℤ
ha : ↑(natAbs a) = ua * a
ub : ℤ
hb : ↑(natAbs b) = ub * b
⊢ Nat.gcdA (natAbs a) (natAbs b) * ua * a + Nat.gcdB (natAbs a) (natAbs b) * ub * b = 1
rw [mul_assoc, ← ha, mul_assoc, ← hb, mul_comm, mul_comm _ (Int.natAbs b : ℤ), ←
  Nat.gcd_eq_gcd_ab, ← gcd_eq_natAbs, hg, Int.ofNat_one]
case mpr.intro.intro
a b r s : ℤ
h : r * a + s * b = 1
⊢ gcd a b = 1
case mpr
a b : ℤ
⊢ IsCoprime a b → gcd a b = 1
rintro ⟨r, s, h⟩
case mpr.intro.intro
a b r s : ℤ
h : r * a + s * b = 1
hg : ¬gcd a b = 1
⊢ False
case mpr.intro.intro
a b r s : ℤ
h : r * a + s * b = 1
⊢ gcd a b = 1
by_contra hg
case mpr.intro.intro.intro.intro.intro
a b r s : ℤ
h : r * a + s * b = 1
hg : ¬gcd a b = 1
p : ℕ
hp : Nat.Prime p
ha : p ∣ natAbs a
hb : p ∣ natAbs b
⊢ False
case mpr.intro.intro
a b r s : ℤ
h : r * a + s * b = 1
hg : ¬gcd a b = 1
⊢ False
obtain ⟨p, ⟨hp, ha, hb⟩⟩ := Nat.Prime.not_coprime_iff_dvd.mp hg
case mpr.intro.intro.intro.intro.intro
a b r s : ℤ
h : r * a + s * b = 1
hg : ¬gcd a b = 1
p : ℕ
hp : Nat.Prime p
ha : p ∣ natAbs a
hb : p ∣ natAbs b
⊢ p ∣ 1
case mpr.intro.intro.intro.intro.intro
a b r s : ℤ
h : r * a + s * b = 1
hg : ¬gcd a b = 1
p : ℕ
hp : Nat.Prime p
ha : p ∣ natAbs a
hb : p ∣ natAbs b
⊢ False
apply Nat.Prime.not_dvd_one hp
case mpr.intro.intro.intro.intro.intro
a b r s : ℤ
h : r * a + s * b = 1
hg : ¬gcd a b = 1
p : ℕ
hp : Nat.Prime p
ha : p ∣ natAbs a
hb : p ∣ natAbs b
⊢ ↑p ∣ r * a + s * b
case mpr.intro.intro.intro.intro.intro
a b r s : ℤ
h : r * a + s * b = 1
hg : ¬gcd a b = 1
p : ℕ
hp : Nat.Prime p
ha : p ∣ natAbs a
hb : p ∣ natAbs b
⊢ p ∣ 1
rw [← coe_nat_dvd, Int.ofNat_one, ← h]
no goals
case mpr.intro.intro.intro.intro.intro
a b r s : ℤ
h : r * a + s * b = 1
hg : ¬gcd a b = 1
p : ℕ
hp : Nat.Prime p
ha : p ∣ natAbs a
hb : p ∣ natAbs b
⊢ ↑p ∣ r * a + s * b
exact dvd_add ((coe_nat_dvd_left.mpr ha).mul_left _) ((coe_nat_dvd_left.mpr hb).mul_left _)