no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s t : Multiset α
hs : ∃ x, x ∈ s ∧ x ≠ 0
ht : s = map ((fun x x_1 => x * x_1) (gcd s)) t
⊢ gcd s * gcd t = gcd s
conv_lhs => rw [← normalize_gcd, ← gcd_map_mul, ← ht]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s t : Multiset α
ht : s = map ((fun x x_1 => x * x_1) (gcd s)) t
hs : gcd s = 0
⊢ ∀ (x : α), x ∈ s → x = 0
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s t : Multiset α
hs : ∃ x, x ∈ s ∧ x ≠ 0
ht : s = map ((fun x x_1 => x * x_1) (gcd s)) t
⊢ ¬gcd s = 0
contrapose! hs
no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s t : Multiset α
ht : s = map ((fun x x_1 => x * x_1) (gcd s)) t
hs : gcd s = 0
⊢ ∀ (x : α), x ∈ s → x = 0
exact s.gcd_eq_zero_iff.1 hs