case top
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Nontrivial α
⊢ prod ⊤ = 0 ↔ ⊤ = ⊤

case coe
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
⊢ prod ↑a✝ = 0 ↔ ↑a✝ = ⊤
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Nontrivial α
p : FactorSet α
⊢ prod p = 0 ↔ p = ⊤
induction p using WithTop.recTopCoe
no goals
case coe
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
⊢ prod ↑a✝ = 0 ↔ ↑a✝ = ⊤
. rw [prod_coe, Multiset.prod_eq_zero_iff, Multiset.mem_map, eq_false WithTop.coe_ne_top,
    iff_false_iff, not_exists]
  exact fun a => not_and_of_not_right _ a.prop.ne_zero
no goals
case top
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Nontrivial α
⊢ prod ⊤ = 0 ↔ ⊤ = ⊤
simp only [iff_self_iff, eq_self_iff_true, Associates.prod_top]
case coe
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
⊢ ∀ (x : { a // Irreducible a }), ¬(x ∈ a✝ ∧ ↑x = 0)
case coe
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
⊢ prod ↑a✝ = 0 ↔ ↑a✝ = ⊤
rw [prod_coe, Multiset.prod_eq_zero_iff, Multiset.mem_map, eq_false WithTop.coe_ne_top,
  iff_false_iff, not_exists]
no goals
case coe
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
⊢ ∀ (x : { a // Irreducible a }), ¬(x ∈ a✝ ∧ ↑x = 0)
exact fun a => not_and_of_not_right _ a.prop.ne_zero