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

State before:
d n : ℕ
hn : Squarefree n
⊢ (d.finMulAntidiagonal n).card = d ^ ω n
Tactic:
rw [←card_finMulAntidiagonal_pi d n hn, Finset.card_pi, Finset.prod_const,
  ArithmeticFunction.cardDistinctFactors_apply, List.card_toFinset, Finset.card_fin]
State after:
no goals