case mp
a b : ℤ
n : ℕ
⊢ gcd a b ∣ n → ∃ x y, ↑n = a * x + b * y

case mpr
a b : ℤ
n : ℕ
⊢ (∃ x y, ↑n = a * x + b * y) → gcd a b ∣ n
a b : ℤ
n : ℕ
⊢ gcd a b ∣ n ↔ ∃ x y, ↑n = a * x + b * y
constructor
case mp
a b : ℤ
n : ℕ
h : gcd a b ∣ n
⊢ ∃ x y, ↑n = a * x + b * y
case mp
a b : ℤ
n : ℕ
⊢ gcd a b ∣ n → ∃ x y, ↑n = a * x + b * y
intro h
case mp
a b : ℤ
n : ℕ
h : gcd a b ∣ n
⊢ ∃ x y, a * (gcdA a b * ↑(n / gcd a b)) + b * (gcdB a b * ↑(n / gcd a b)) = a * x + b * y
case mp
a b : ℤ
n : ℕ
h : gcd a b ∣ n
⊢ ∃ x y, ↑n = a * x + b * y
rw [← Nat.mul_div_cancel' h, Int.ofNat_mul, gcd_eq_gcd_ab, add_mul, mul_assoc, mul_assoc]
no goals
case mp
a b : ℤ
n : ℕ
h : gcd a b ∣ n
⊢ ∃ x y, a * (gcdA a b * ↑(n / gcd a b)) + b * (gcdB a b * ↑(n / gcd a b)) = a * x + b * y
exact ⟨_, _, rfl⟩
case mpr.intro.intro
a b : ℤ
n : ℕ
x y : ℤ
h : ↑n = a * x + b * y
⊢ gcd a b ∣ n
case mpr
a b : ℤ
n : ℕ
⊢ (∃ x y, ↑n = a * x + b * y) → gcd a b ∣ n
rintro ⟨x, y, h⟩
case mpr.intro.intro
a b : ℤ
n : ℕ
x y : ℤ
h : ↑n = a * x + b * y
⊢ ↑(gcd a b) ∣ a * x + b * y
case mpr.intro.intro
a b : ℤ
n : ℕ
x y : ℤ
h : ↑n = a * x + b * y
⊢ gcd a b ∣ n
rw [← Int.coe_nat_dvd, h]
no goals
case mpr.intro.intro
a b : ℤ
n : ℕ
x y : ℤ
h : ↑n = a * x + b * y
⊢ ↑(gcd a b) ∣ a * x + b * y
exact
  dvd_add (dvd_mul_of_dvd_left (gcd_dvd_left a b) _) (dvd_mul_of_dvd_left (gcd_dvd_right a b) y)