no goals
F : Type ?u.829527
α : Type u_2
β : Type u_1
γ : Type ?u.829536
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
b : β
⊢ a⁻¹ • b ∈ s ↔ b ∈ a • s
rw [← smul_mem_smul_finset_iff a, smul_inv_smul]