simp only [ex124', Set.mem_prod, exists_prop, Prod.exists]
G : Type u_1
inst✝ : Group G
A B : Set G
⊢ #↑{x | ∃ x_1 ∈ A ×ˢ B, ex124' x_1 = x} ≤ #↑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