apply Finset.card_bij (Nat.primeFactorsPiBij d n) (primeFactorsPiBij_img d n hn)
  (primeFactorsPiBij_inj d n) (primeFactorsPiBij_surj d n hn)
d n : ℕ
hn : Squarefree n
⊢ (n.factors.toFinset.pi fun x => univ).card = (d.finMulAntidiagonal n).card
no goals