apply prod_primeFactors_of_squarefree hn
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
⊢ ∏ x ∈ n.primeFactors, x = n

case h
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
⊢ ∀ i ∈ n.primeFactors.attach, f ↑i ⋯ ∈ univ
case h
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
⊢ ∀ i ∈ n.primeFactors.attach, f ↑i ⋯ ∈ univ