use d * (Int.gcdA a b), d * (Int.gcdB a b)
case mpr
a b c : ℤ
h : ↑(Int.gcd a b) ∣ c
d : ℤ := c / ↑(Int.gcd a b)
h' : ↑(Int.gcd a b) * d = c := Int.mul_ediv_cancel_of_emod_eq_zero (Int.emod_eq_zero_of_dvd h)
⊢ ∃ x y, a * x + b * y = c
case h
a b c : ℤ
h : ↑(Int.gcd a b) ∣ c
d : ℤ := c / ↑(Int.gcd a b)
h' : ↑(Int.gcd a b) * d = c := Int.mul_ediv_cancel_of_emod_eq_zero (Int.emod_eq_zero_of_dvd h)
⊢ a * (d * Int.gcdA a b) + b * (d * Int.gcdB a b) = c