d x y a b : ℕ
hu : x % d = 0
hv : y % d = 0
h : x * a = y * b + d
⊢ Int.gcd ↑x ↑y = d
d x y a b : ℕ
hu : x % d = 0
hv : y % d = 0
h : x * a = y * b + d
⊢ Nat.gcd x y = d
rw [← Int.coe_nat_gcd]
d x y a b : ℕ
hu : x % d = 0
hv : y % d = 0
h : x * a = y * b + d
⊢ ↑x * ↑a + ↑y * -↑b = ↑d
d x y a b : ℕ
hu : x % d = 0
hv : y % d = 0
h : x * a = y * b + d
⊢ Int.gcd ↑x ↑y = d
apply int_gcd_helper' a (-b)
  (Int.coe_nat_dvd.mpr (Nat.dvd_of_mod_eq_zero hu))
  (Int.coe_nat_dvd.mpr (Nat.dvd_of_mod_eq_zero hv))
d x y a b : ℕ
hu : x % d = 0
hv : y % d = 0
h : x * a = y * b + d
⊢ ↑x * ↑a = ↑y * ↑b + ↑d
d x y a b : ℕ
hu : x % d = 0
hv : y % d = 0
h : x * a = y * b + d
⊢ ↑x * ↑a + ↑y * -↑b = ↑d
rw [mul_neg, ← sub_eq_add_neg, sub_eq_iff_eq_add']
no goals
d x y a b : ℕ
hu : x % d = 0
hv : y % d = 0
h : x * a = y * b + d
⊢ ↑x * ↑a = ↑y * ↑b + ↑d
exact_mod_cast h