case zero

⊢ normalizedFactors zero = ↑(factors zero)

case succ
n✝ : ℕ
⊢ normalizedFactors (succ n✝) = ↑(factors (succ n✝))
n : ℕ
⊢ normalizedFactors n = ↑(factors n)
cases n
case succ
n✝ : ℕ
⊢ normalizedFactors (succ n✝) = ↑(factors (succ n✝))
case zero

⊢ normalizedFactors zero = ↑(factors zero)

case succ
n✝ : ℕ
⊢ normalizedFactors (succ n✝) = ↑(factors (succ n✝))
case zero => simp
no goals
⊢ normalizedFactors zero = ↑(factors zero)
simp
n : ℕ
⊢ Multiset.Rel (fun x x_1 => Associated x x_1) (normalizedFactors (succ n)) ↑(factors (succ n))
n : ℕ
⊢ normalizedFactors (succ n) = ↑(factors (succ n))
rw [← Multiset.rel_eq, ← associated_eq_eq]
n : ℕ
⊢ Associated (Multiset.prod (normalizedFactors (succ n))) (Multiset.prod ↑(factors (succ n)))

n : ℕ
⊢ ∀ (x : ℕ), x ∈ ↑(factors (succ n)) → Irreducible x
n : ℕ
⊢ Multiset.Rel (fun x x_1 => Associated x x_1) (normalizedFactors (succ n)) ↑(factors (succ n))
apply UniqueFactorizationMonoid.factors_unique irreducible_of_normalized_factor _
n : ℕ
⊢ Associated (Multiset.prod (normalizedFactors (succ n))) (succ n)
n : ℕ
⊢ Associated (Multiset.prod (normalizedFactors (succ n))) (Multiset.prod ↑(factors (succ n)))
rw [Multiset.coe_prod, Nat.prod_factors n.succ_ne_zero]
no goals
n : ℕ
⊢ Associated (Multiset.prod (normalizedFactors (succ n))) (succ n)
apply normalizedFactors_prod (Nat.succ_ne_zero _)
n x : ℕ
hx : x ∈ ↑(factors (succ n))
⊢ Irreducible x
n : ℕ
⊢ ∀ (x : ℕ), x ∈ ↑(factors (succ n)) → Irreducible x
intro x hx
n x : ℕ
hx : x ∈ ↑(factors (succ n))
⊢ Prime x
n x : ℕ
hx : x ∈ ↑(factors (succ n))
⊢ Irreducible x
rw [Nat.irreducible_iff_prime, ← Nat.prime_iff]
no goals
n x : ℕ
hx : x ∈ ↑(factors (succ n))
⊢ Prime x
exact Nat.prime_of_mem_factors hx