G : Type u
inst✝¹ : Group G
N✝ : Subgroup G
nN✝ : Subgroup.Normal N✝
H : Type v
inst✝ : Group H
N : Subgroup G
nN : Subgroup.Normal N
x y : G
⊢ y⁻¹ * x ∈ N ↔ x / y ∈ N
G : Type u
inst✝¹ : Group G
N✝ : Subgroup G
nN✝ : Subgroup.Normal N✝
H : Type v
inst✝ : Group H
N : Subgroup G
nN : Subgroup.Normal N
x y : G
⊢ ↑x = ↑y ↔ x / y ∈ N
refine' eq_comm.trans (QuotientGroup.eq.trans _)
no goals
G : Type u
inst✝¹ : Group G
N✝ : Subgroup G
nN✝ : Subgroup.Normal N✝
H : Type v
inst✝ : Group H
N : Subgroup G
nN : Subgroup.Normal N
x y : G
⊢ y⁻¹ * x ∈ N ↔ x / y ∈ N
rw [nN.mem_comm_iff, div_eq_mul_inv]