f : ℕ →₀ ℕ
hf : ∀ (p : ℕ), p ∈ f.support → Prime p
h : ∀ (x : ℕ), x ∈ f.support → x ^ ↑f x ≠ 0
⊢ factorization (Finsupp.prod f fun x x_1 => x ^ x_1) = f
f : ℕ →₀ ℕ
hf : ∀ (p : ℕ), p ∈ f.support → Prime p
⊢ factorization (Finsupp.prod f fun x x_1 => x ^ x_1) = f
have h : ∀ x : ℕ, x ∈ f.support → x ^ f x ≠ 0 := fun p hp =>
  pow_ne_zero _ (Prime.ne_zero (hf p hp))
f : ℕ →₀ ℕ
hf : ∀ (p : ℕ), p ∈ f.support → Prime p
h : ∀ (x : ℕ), x ∈ f.support → x ^ ↑f x ≠ 0
⊢ ∑ x in f.support, factorization (x ^ ↑f x) = f
f : ℕ →₀ ℕ
hf : ∀ (p : ℕ), p ∈ f.support → Prime p
h : ∀ (x : ℕ), x ∈ f.support → x ^ ↑f x ≠ 0
⊢ factorization (Finsupp.prod f fun x x_1 => x ^ x_1) = f
simp only [Finsupp.prod, factorization_prod h]
f : ℕ →₀ ℕ
hf : ∀ (p : ℕ), p ∈ f.support → Prime p
h : ∀ (x : ℕ), x ∈ f.support → x ^ ↑f x ≠ 0
⊢ ∑ x in f.support, factorization (x ^ ↑f x) = Finsupp.sum f single
f : ℕ →₀ ℕ
hf : ∀ (p : ℕ), p ∈ f.support → Prime p
h : ∀ (x : ℕ), x ∈ f.support → x ^ ↑f x ≠ 0
⊢ ∑ x in f.support, factorization (x ^ ↑f x) = f
conv =>
  rhs
  rw [(sum_single f).symm]
no goals
f : ℕ →₀ ℕ
hf : ∀ (p : ℕ), p ∈ f.support → Prime p
h : ∀ (x : ℕ), x ∈ f.support → x ^ ↑f x ≠ 0
⊢ ∑ x in f.support, factorization (x ^ ↑f x) = Finsupp.sum f single
exact sum_congr rfl fun p hp => Prime.factorization_pow (hf p hp)