α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
h : gcd a b = 0
ca : α
ha : a = gcd a b * ca
⊢ a = 0 ∧ b = 0
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
h : gcd a b = 0
⊢ a = 0 ∧ b = 0
let ⟨ca, ha⟩ := gcd_dvd_left a b
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
h : gcd a b = 0
ca : α
ha : a = gcd a b * ca
cb : α
hb : b = gcd a b * cb
⊢ a = 0 ∧ b = 0
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
h : gcd a b = 0
ca : α
ha : a = gcd a b * ca
⊢ a = 0 ∧ b = 0
let ⟨cb, hb⟩ := gcd_dvd_right a b
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
h : gcd a b = 0
ca : α
ha : a = 0
cb : α
hb : b = 0
⊢ a = 0 ∧ b = 0
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
h : gcd a b = 0
ca : α
ha : a = gcd a b * ca
cb : α
hb : b = gcd a b * cb
⊢ a = 0 ∧ b = 0
rw [h, zero_mul] at ha hb
no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
h : gcd a b = 0
ca : α
ha : a = 0
cb : α
hb : b = 0
⊢ a = 0 ∧ b = 0
exact ⟨ha, hb⟩
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
x✝ : a = 0 ∧ b = 0
ha : a = 0
hb : b = 0
⊢ 0 ∣ gcd 0 0
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
x✝ : a = 0 ∧ b = 0
ha : a = 0
hb : b = 0
⊢ gcd a b = 0
rw [ha, hb, ← zero_dvd_iff]
no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
x✝ : a = 0 ∧ b = 0
ha : a = 0
hb : b = 0
⊢ 0 ∣ gcd 0 0
apply dvd_gcd <;> rfl