no goals
α : Type u_1
inst✝ : Group α
s : Set α
x a : α
x✝ : x ∈ a *l s
b : α
hb : b ∈ s
Eq : (fun x => a * x) b = x
⊢ a⁻¹ * x ∈ s
simp [Eq.symm, hb]
no goals
α : Type u_1
inst✝ : Group α
s : Set α
x a : α
h : a⁻¹ * x ∈ s
⊢ (fun x => a * x) (a⁻¹ * x) = x
simp