no goals
F : Type ?u.153411
α : Type u_2
β : Type u_1
γ : Type ?u.153420
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t A B : Set β
a : α
x : β
s : Set β
⊢ (⋃ (g : α), g • s) = {a | ∃ g, g • a ∈ s}
simp_rw [← iUnion_setOf, ← iUnion_inv_smul, ← preimage_smul, preimage]