exact
  Cardinal.mk_iUnion_le_sum_mk.trans
    (Cardinal.sum_le_sum _ _ fun a => Cardinal.mk_iUnion_le_sum_mk)
case calc_3
G : Type u_1
inst✝ : Group G
A B : Set G
⊢ #↑(⋃ a, ⋃ b, {↑a * ↑b}) ≤ Cardinal.sum fun a => Cardinal.sum fun b => #↑{↑a * ↑b}
no goals