rw [mem_finMulAntidiagonal] at hf
d n p : ℕ
hn : Squarefree n
hp : p ∈ n.factors
f : Fin d → ℕ
hf : f ∈ d.finMulAntidiagonal n
⊢ ∃! i, p ∣ f i
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