G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H✝ : Type v
inst✝ : Group H✝
φ : G →* H✝
H : Subgroup G
h : Subsingleton (G ⧸ H)
x : G
x✝ : x ∈ ⊤
this : 1⁻¹ * x ∈ H
⊢ x ∈ H
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H✝ : Type v
inst✝ : Group H✝
φ : G →* H✝
H : Subgroup G
h : Subsingleton (G ⧸ H)
x : G
x✝ : x ∈ ⊤
⊢ x ∈ H
have this : 1⁻¹ * x ∈ H := QuotientGroup.eq.1 (Subsingleton.elim _ _)
no goals
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H✝ : Type v
inst✝ : Group H✝
φ : G →* H✝
H : Subgroup G
h : Subsingleton (G ⧸ H)
x : G
x✝ : x ∈ ⊤
this : 1⁻¹ * x ∈ H
⊢ x ∈ H
rwa [inv_one, one_mul] at this