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