x is product of its prime factors with correct exponents

Stream: new members

[Ilmārs Cīrulis]

I'm stuck on this, because my brain doesn't work today. I'm trying to find better proof, if possible.

import Mathlib

theorem THM (x: ℕ) (Hx: x ≠ 0): x = (∏ i ∈ x.primeFactors, i ^ (x.factorization i)) := by
  have H := Nat.prod_pow_factorization_eq_self (f := x.factorization)
  have H0 := H (fun p Hp => Nat.prime_of_mem_primeFactors Hp)
  have H1 := Nat.factorization_inj
  apply H1 at H0
  . simp [Finsupp.prod] at H0
    exact H0.symm
  . simp
    intros p Hp H0 H1 h2
    subst p
    omega
  . simp
    exact Hx

Thanks for any hints!

[Sabbir Rahman]

I had just asked about the prime factorization recently. learnt this thanks to Yaël Dillies.

import Mathlib

theorem THM (x: ℕ) (Hx: x ≠ 0): x = (∏ i ∈ x.primeFactors, i ^ (x.factorization i)) :=
   (Nat.factorization_prod_pow_eq_self Hx).symm

[Ilmārs Cīrulis]

Thank you very much!