simp [Set.setOf_exists, Set.setOf_and, and_assoc]
case calc_1.e_a.e_s.h
G : Type u_1
inst✝ : Group G
A B : Set G
x : G
⊢ x ∈ {x | ∃ a b, (a ∈ A ∧ b ∈ B) ∧ a * b = x} ↔ x ∈ ⋃ a ∈ A, ⋃ b ∈ B, {a * b}
no goals