rw [← h', Int.gcd_eq_gcd_ab]
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
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) = (a * Int.gcdA a b + b * Int.gcdB a b) * d