Theorem: Nat.card_finMulAntidiagonal_pi (PrimeNumberTheoremAnd/Mathlib/Data/Nat/FinMulAntidiagonal.lean)

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