let h' : Int.gcd a b * d = c := by 
  apply Int.mul_ediv_cancel_of_emod_eq_zero
  apply Int.emod_eq_zero_of_dvd
  assumption
case mpr
a b c : ℤ
h : ↑(Int.gcd a b) ∣ c
d : ℤ := c / ↑(Int.gcd a b)
⊢ ∃ x y, a * x + b * y = c
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