calc
  (#{x | ∃ a b : G, (a ∈ A ∧ b ∈ B) ∧ a * b = x}) =
      (#(⋃ (a ∈ A) (b ∈ B), ({(a : G) * (b : G)} : Set G))) := ?_
  _ = (#(⋃ (a : A) (b : B), ({(a : G) * (b : G)} : Set G))) := ?_
  _ ≤ Cardinal.sum fun a : A => Cardinal.sum fun b : B => #({(a : G) * (b : G)} : Set G) := ?_
  _ = (#A) * (#B) := ?_
G : Type u_1
inst✝ : Group G
A B : Set G
⊢ #↑{x | ∃ a b, (a ∈ A ∧ b ∈ B) ∧ a * b = x} ≤ #↑A * #↑B
case calc_1
G : Type u_1
inst✝ : Group G
A B : Set G
⊢ #↑{x | ∃ a b, (a ∈ A ∧ b ∈ B) ∧ a * b = x} = #↑(⋃ a ∈ A, ⋃ b ∈ B, {a * b})

case calc_2
G : Type u_1
inst✝ : Group G
A B : Set G
⊢ #↑(⋃ a ∈ A, ⋃ b ∈ B, {a * b}) = #↑(⋃ a, ⋃ b, {↑a * ↑b})

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}

case calc_4
G : Type u_1
inst✝ : Group G
A B : Set G
⊢ (Cardinal.sum fun a => Cardinal.sum fun b => #↑{↑a * ↑b}) = #↑A * #↑B