s : Multiset ℕ
h : ∀ (x : ℕ), x ∈ s → Irreducible x
⊢ Multiset.Rel (fun x x_1 => Associated x x_1) (normalizedFactors (Multiset.prod s)) s
s : Multiset ℕ
h : ∀ (x : ℕ), x ∈ s → Irreducible x
⊢ normalizedFactors (Multiset.prod s) = s
rw [← Multiset.rel_eq, ← associated_eq_eq]
s : Multiset ℕ
h : ∀ (x : ℕ), x ∈ s → Irreducible x
⊢ Multiset.prod s ≠ 0
s : Multiset ℕ
h : ∀ (x : ℕ), x ∈ s → Irreducible x
⊢ Multiset.Rel (fun x x_1 => Associated x x_1) (normalizedFactors (Multiset.prod s)) s
apply
  UniqueFactorizationMonoid.factors_unique irreducible_of_normalized_factor h
    (normalizedFactors_prod _)
s : Multiset ℕ
h : ∀ (x : ℕ), x ∈ s → Irreducible x
⊢ ¬0 ∈ s
s : Multiset ℕ
h : ∀ (x : ℕ), x ∈ s → Irreducible x
⊢ Multiset.prod s ≠ 0
rw [Ne.def, Multiset.prod_eq_zero_iff]
s : Multiset ℕ
h : ∀ (x : ℕ), x ∈ s → Irreducible x
con : 0 ∈ s
⊢ False
s : Multiset ℕ
h : ∀ (x : ℕ), x ∈ s → Irreducible x
⊢ ¬0 ∈ s
intro con
no goals
s : Multiset ℕ
h : ∀ (x : ℕ), x ∈ s → Irreducible x
con : 0 ∈ s
⊢ False
exact not_irreducible_zero (h 0 con)