G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
⊢ Subsingleton (Quot Setoid.r)
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
⊢ Subsingleton (G ⧸ ⊤)
dsimp [HasQuotient.Quotient, QuotientGroup.instHasQuotientSubgroup, Quotient]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
⊢ Subsingleton (Quot fun x y => x⁻¹ * y ∈ ⊤)
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
⊢ Subsingleton (Quot Setoid.r)
rw [leftRel_eq]
no goals
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
⊢ Subsingleton (Quot fun x y => x⁻¹ * y ∈ ⊤)
exact Trunc.instSubsingletonTrunc