case h
N : Type u_1
G : Type u_2
H : Type ?u.105269
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
x✝ : N
⊢ ↑(MonoidHom.comp rightHom inl) x✝ = ↑1 x✝
N : Type u_1
G : Type u_2
H : Type ?u.105269
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
⊢ MonoidHom.comp rightHom inl = 1
ext
no goals
case h
N : Type u_1
G : Type u_2
H : Type ?u.105269
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
x✝ : N
⊢ ↑(MonoidHom.comp rightHom inl) x✝ = ↑1 x✝
simp [rightHom]