rw [mem_factors hf.2, ← hf.1, hp.1.prime.dvd_finset_prod_iff] at hp
d n p : ℕ
hn : Squarefree n
hp : p ∈ n.factors
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
⊢ ∃! i, p ∣ f i
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : p.Prime ∧ ∃ a ∈ univ, p ∣ f a
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
⊢ ∃! i, p ∣ f i