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