[GOAL]
d : ℕ
x y a b : ℤ
h₁ : ↑d ∣ x
h₂ : ↑d ∣ y
h₃ : x * a + y * b = ↑d
⊢ Int.gcd x y = d
[PROOFSTEP]
refine Nat.dvd_antisymm ?_ (Int.coe_nat_dvd.1 (Int.dvd_gcd h₁ h₂))
[GOAL]
d : ℕ
x y a b : ℤ
h₁ : ↑d ∣ x
h₂ : ↑d ∣ y
h₃ : x * a + y * b = ↑d
⊢ Int.gcd x y ∣ d
[PROOFSTEP]
rw [← Int.coe_nat_dvd, ← h₃]
[GOAL]
d : ℕ
x y a b : ℤ
h₁ : ↑d ∣ x
h₂ : ↑d ∣ y
h₃ : x * a + y * b = ↑d
⊢ ↑(Int.gcd x y) ∣ x * a + y * b
[PROOFSTEP]
apply dvd_add
[GOAL]
case h₁
d : ℕ
x y a b : ℤ
h₁ : ↑d ∣ x
h₂ : ↑d ∣ y
h₃ : x * a + y * b = ↑d
⊢ ↑(Int.gcd x y) ∣ x * a
[PROOFSTEP]
exact (Int.gcd_dvd_left _ _).mul_right _
[GOAL]
case h₂
d : ℕ
x y a b : ℤ
h₁ : ↑d ∣ x
h₂ : ↑d ∣ y
h₃ : x * a + y * b = ↑d
⊢ ↑(Int.gcd x y) ∣ y * b
[PROOFSTEP]
exact (Int.gcd_dvd_right _ _).mul_right _
[GOAL]
d x y a b : ℕ
hu : x % d = 0
hv : y % d = 0
h : x * a = y * b + d
⊢ Nat.gcd x y = d
[PROOFSTEP]
rw [← Int.coe_nat_gcd]
[GOAL]
d x y a b : ℕ
hu : x % d = 0
hv : y % d = 0
h : x * a = y * b + d
⊢ Int.gcd ↑x ↑y = d
[PROOFSTEP]
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))
[GOAL]
d x y a b : ℕ
hu : x % d = 0
hv : y % d = 0
h : x * a = y * b + d
⊢ ↑x * ↑a + ↑y * -↑b = ↑d
[PROOFSTEP]
rw [mul_neg, ← sub_eq_add_neg, sub_eq_iff_eq_add']
[GOAL]
d x y a b : ℕ
hu : x % d = 0
hv : y % d = 0
h : x * a = y * b + d
⊢ ↑x * ↑a = ↑y * ↑b + ↑d
[PROOFSTEP]
exact_mod_cast h
[GOAL]
x y d m : ℕ
hd : Nat.gcd x y = d
d0 : Nat.beq d 0 = false
dm : x * y = d * m
⊢ (fun x x_1 => x * x_1) d (Nat.lcm x y) = (fun x x_1 => x * x_1) d m
[PROOFSTEP]
dsimp only
  -- Porting note: the `dsimp only` was not necessary in Lean3.
[GOAL]
x y d m : ℕ
hd : Nat.gcd x y = d
d0 : Nat.beq d 0 = false
dm : x * y = d * m
⊢ d * Nat.lcm x y = d * m
[PROOFSTEP]
rw [← dm, ← hd, Nat.gcd_mul_lcm]
[GOAL]
x y : ℤ
x' y' d : ℕ
hx : Int.natAbs x = x'
hy : Int.natAbs y = y'
h : Nat.gcd x' y' = d
⊢ Int.gcd x y = d
[PROOFSTEP]
subst_vars
[GOAL]
x y : ℤ
⊢ Int.gcd x y = Nat.gcd (Int.natAbs x) (Int.natAbs y)
[PROOFSTEP]
rw [Int.gcd_def]
[GOAL]
x y : ℤ
x' y' d : ℕ
hx : Int.natAbs x = x'
hy : Int.natAbs y = y'
h : Nat.lcm x' y' = d
⊢ Int.lcm x y = d
[PROOFSTEP]
subst_vars
[GOAL]
x y : ℤ
⊢ Int.lcm x y = Nat.lcm (Int.natAbs x) (Int.natAbs y)
[PROOFSTEP]
rw [Int.lcm_def]
