α : Type u_1
inst✝ : Group α
s : Subgroup α
h : ∀ (g : α), g *l ↑s = ↑s *r g
a : α
ha : a ∈ s
g : α
⊢ g * a ∈ g *l ↑s
α : Type u_1
inst✝ : Group α
s : Subgroup α
h : ∀ (g : α), g *l ↑s = ↑s *r g
a : α
ha : a ∈ s
g : α
⊢ g * a * g⁻¹ ∈ ↑s
rw [← mem_rightCoset_iff, ← h]
no goals
α : Type u_1
inst✝ : Group α
s : Subgroup α
h : ∀ (g : α), g *l ↑s = ↑s *r g
a : α
ha : a ∈ s
g : α
⊢ g * a ∈ g *l ↑s
exact mem_leftCoset g ha