unfold Nat.primeFactorsPiBij
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
⊢ ∏ i : Fin d, Nat.primeFactorsPiBij d n f hf i = n
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
⊢ ∏ i : Fin d, ∏ p ∈ filter (fun p => f ↑p ⋯ = i) n.primeFactors.attach, ↑p = n