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