rw [mem_finMulAntidiagonal]
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
⊢ Nat.primeFactorsPiBij d n f hf ∈ d.finMulAntidiagonal n
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 ∧ n ≠ 0