case empty
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : Nontrivial α
⊢ lcm 0 = 0 ↔ 0 ∈ 0

case cons
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : Nontrivial α
a : α
s : Multiset α
ihs : lcm s = 0 ↔ 0 ∈ s
⊢ lcm (a ::ₘ s) = 0 ↔ 0 ∈ a ::ₘ s
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : Nontrivial α
s : Multiset α
⊢ lcm s = 0 ↔ 0 ∈ s
induction' s using Multiset.induction_on with a s ihs
no goals
case empty
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : Nontrivial α
⊢ lcm 0 = 0 ↔ 0 ∈ 0
simp only [lcm_zero, one_ne_zero, not_mem_zero]
no goals
case cons
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : Nontrivial α
a : α
s : Multiset α
ihs : lcm s = 0 ↔ 0 ∈ s
⊢ lcm (a ::ₘ s) = 0 ↔ 0 ∈ a ::ₘ s
simp only [mem_cons, lcm_cons, lcm_eq_zero_iff, ihs, @eq_comm _ a]