a b c : ℤ
habc : a ∣ b * c
hab : gcd a c = 1
this : ↑(gcd a c) = a * gcdA a c + c * gcdB a c
⊢ a ∣ b
a b c : ℤ
habc : a ∣ b * c
hab : gcd a c = 1
⊢ a ∣ b
have := gcd_eq_gcd_ab a c
a b c : ℤ
habc : a ∣ b * c
hab : gcd a c = 1
this : 1 = a * gcdA a c + c * gcdB a c
⊢ a ∣ b
a b c : ℤ
habc : a ∣ b * c
hab : gcd a c = 1
this : ↑(gcd a c) = a * gcdA a c + c * gcdB a c
⊢ a ∣ b
simp only [hab, Int.ofNat_zero, Int.ofNat_succ, zero_add] at this
a b c : ℤ
habc : a ∣ b * c
hab : gcd a c = 1
this✝ : 1 = a * gcdA a c + c * gcdB a c
this : b * a * gcdA a c + b * c * gcdB a c = b
⊢ a ∣ b
a b c : ℤ
habc : a ∣ b * c
hab : gcd a c = 1
this : 1 = a * gcdA a c + c * gcdB a c
⊢ a ∣ b
have : b * a * gcdA a c + b * c * gcdB a c = b := by simp [mul_assoc, ← mul_add, ← this]
a b c : ℤ
habc : a ∣ b * c
hab : gcd a c = 1
this✝ : 1 = a * gcdA a c + c * gcdB a c
this : b * a * gcdA a c + b * c * gcdB a c = b
⊢ a ∣ b * a * gcdA a c + b * c * gcdB a c
a b c : ℤ
habc : a ∣ b * c
hab : gcd a c = 1
this✝ : 1 = a * gcdA a c + c * gcdB a c
this : b * a * gcdA a c + b * c * gcdB a c = b
⊢ a ∣ b
rw [← this]
no goals
a b c : ℤ
habc : a ∣ b * c
hab : gcd a c = 1
this✝ : 1 = a * gcdA a c + c * gcdB a c
this : b * a * gcdA a c + b * c * gcdB a c = b
⊢ a ∣ b * a * gcdA a c + b * c * gcdB a c
exact dvd_add (dvd_mul_of_dvd_left (dvd_mul_left a b) _) (dvd_mul_of_dvd_left habc _)
no goals
a b c : ℤ
habc : a ∣ b * c
hab : gcd a c = 1
this : 1 = a * gcdA a c + c * gcdB a c
⊢ b * a * gcdA a c + b * c * gcdB a c = b
simp [mul_assoc, ← mul_add, ← this]