apply Iff.intro
a b c : ℤ
⊢ (∃ x y, a * x + b * y = c) ↔ ↑(Int.gcd a b) ∣ c
case mp
a b c : ℤ
⊢ (∃ x y, a * x + b * y = c) → ↑(Int.gcd a b) ∣ c

case mpr
a b c : ℤ
⊢ ↑(Int.gcd a b) ∣ c → ∃ x y, a * x + b * y = c