case h.mk
G : Type u
inst✝³ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝² : Group H
G' : Subgroup G
H' : Subgroup H
inst✝¹ : Subgroup.Normal G'
inst✝ : Subgroup.Normal H'
he : optParam (Subgroup.map (↑(MulEquiv.refl G)) G' = G') (_ : Subgroup.map (MonoidHom.id G) G' = G')
x✝ : G ⧸ G'
x : G
⊢ ↑(congr G' G' (MulEquiv.refl G) he) (Quot.mk Setoid.r x) = ↑(MulEquiv.refl (G ⧸ G')) (Quot.mk Setoid.r x)
G : Type u
inst✝³ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝² : Group H
G' : Subgroup G
H' : Subgroup H
inst✝¹ : Subgroup.Normal G'
inst✝ : Subgroup.Normal H'
he : optParam (Subgroup.map (↑(MulEquiv.refl G)) G' = G') (_ : Subgroup.map (MonoidHom.id G) G' = G')
⊢ congr G' G' (MulEquiv.refl G) he = MulEquiv.refl (G ⧸ G')
ext ⟨x⟩
no goals
case h.mk
G : Type u
inst✝³ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝² : Group H
G' : Subgroup G
H' : Subgroup H
inst✝¹ : Subgroup.Normal G'
inst✝ : Subgroup.Normal H'
he : optParam (Subgroup.map (↑(MulEquiv.refl G)) G' = G') (_ : Subgroup.map (MonoidHom.id G) G' = G')
x✝ : G ⧸ G'
x : G
⊢ ↑(congr G' G' (MulEquiv.refl G) he) (Quot.mk Setoid.r x) = ↑(MulEquiv.refl (G ⧸ G')) (Quot.mk Setoid.r x)
rfl