G : Type u
inst✝⁴ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝³ : Group H
I : Type u_1
inst✝² : Group I
M : Subgroup H
O : Subgroup I
inst✝¹ : Subgroup.Normal M
inst✝ : Subgroup.Normal O
f : G →* H
g : H →* I
hf : N ≤ Subgroup.comap f M
hg : M ≤ Subgroup.comap g O
hgf : optParam (N ≤ Subgroup.comap (MonoidHom.comp g f) O) (_ : N ≤ Subgroup.comap (MonoidHom.comp g f) O)
x✝ : G ⧸ N
x : G
⊢ ↑(map M O g hg) (↑(map N M f hf) ↑x) = ↑(map N O (MonoidHom.comp g f) hgf) ↑x
G : Type u
inst✝⁴ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝³ : Group H
I : Type u_1
inst✝² : Group I
M : Subgroup H
O : Subgroup I
inst✝¹ : Subgroup.Normal M
inst✝ : Subgroup.Normal O
f : G →* H
g : H →* I
hf : N ≤ Subgroup.comap f M
hg : M ≤ Subgroup.comap g O
hgf : optParam (N ≤ Subgroup.comap (MonoidHom.comp g f) O) (_ : N ≤ Subgroup.comap (MonoidHom.comp g f) O)
x : G ⧸ N
⊢ ↑(map M O g hg) (↑(map N M f hf) x) = ↑(map N O (MonoidHom.comp g f) hgf) x
refine' induction_on' x fun x => _
no goals
G : Type u
inst✝⁴ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝³ : Group H
I : Type u_1
inst✝² : Group I
M : Subgroup H
O : Subgroup I
inst✝¹ : Subgroup.Normal M
inst✝ : Subgroup.Normal O
f : G →* H
g : H →* I
hf : N ≤ Subgroup.comap f M
hg : M ≤ Subgroup.comap g O
hgf : optParam (N ≤ Subgroup.comap (MonoidHom.comp g f) O) (_ : N ≤ Subgroup.comap (MonoidHom.comp g f) O)
x✝ : G ⧸ N
x : G
⊢ ↑(map M O g hg) (↑(map N M f hf) ↑x) = ↑(map N O (MonoidHom.comp g f) hgf) ↑x
simp only [map_mk, MonoidHom.comp_apply]