apply Int.mul_ediv_cancel_of_emod_eq_zero
a b c : ℤ
h : ↑(Int.gcd a b) ∣ c
d : ℤ := c / ↑(Int.gcd a b)
⊢ ↑(Int.gcd a b) * d = c
case H
a b c : ℤ
h : ↑(Int.gcd a b) ∣ c
d : ℤ := c / ↑(Int.gcd a b)
⊢ c % ↑(Int.gcd a b) = 0