n : ℕ+
⊢ ↑(PrimeMultiset.prod (PrimeMultiset.ofNatList (Nat.factors ↑n) (_ : ∀ {p : ℕ}, p ∈ Nat.factors ↑n → Nat.Prime p))) =
    ↑n
n : ℕ+
⊢ ↑(PrimeMultiset.prod (factorMultiset n)) = ↑n
dsimp [factorMultiset]
n : ℕ+
⊢ List.prod (Nat.factors ↑n) = ↑n
n : ℕ+
⊢ ↑(PrimeMultiset.prod (PrimeMultiset.ofNatList (Nat.factors ↑n) (_ : ∀ {p : ℕ}, p ∈ Nat.factors ↑n → Nat.Prime p))) =
    ↑n
rw [PrimeMultiset.prod_ofNatList]
no goals
n : ℕ+
⊢ List.prod (Nat.factors ↑n) = ↑n
exact Nat.prod_factors n.ne_zero