no goals
F : Type ?u.107575
α : Type u_2
β : Type u_1
γ : Type ?u.107584
inst✝¹ : Group α
inst✝ : MulAction α β
s t A B : Set β
a : α
x : β
⊢ x ∈ a⁻¹ • A ↔ a • x ∈ A
simp only [← image_smul, mem_image, inv_smul_eq_iff, exists_eq_right]