α : Type u_1
inst✝ : Group α
s : Subgroup α
N : Normal s
g a : α
⊢ g⁻¹ * a ∈ s ↔ a * g⁻¹ ∈ s
α : Type u_1
inst✝ : Group α
s : Subgroup α
N : Normal s
g a : α
⊢ a ∈ g *l ↑s ↔ a ∈ ↑s *r g
simp [mem_leftCoset_iff, mem_rightCoset_iff]
no goals
α : Type u_1
inst✝ : Group α
s : Subgroup α
N : Normal s
g a : α
⊢ g⁻¹ * a ∈ s ↔ a * g⁻¹ ∈ s
rw [N.mem_comm_iff]