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 : G
⊢ x⁻¹ * 1 ∈ N ↔ x ∈ 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 : G
⊢ ↑x = 1 ↔ x ∈ N
refine' 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 : G
⊢ x⁻¹ * 1 ∈ N ↔ x ∈ N
rw [mul_one, Subgroup.inv_mem_iff]