no goals
N : Type u_3
G : Type u_4
H : Type ?u.259984
inst✝⁴ : Group N
inst✝³ : Group G
inst✝² : Group H
φ : G →* MulAut N
N₁ : Type u_1
G₁ : Type u_2
inst✝¹ : Group N₁
inst✝ : Group G₁
φ₁ : G₁ →* MulAut N₁
f₁ : N →* N₁
f₂ : G →* G₁
h : ∀ (g : G), MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑φ₁ (↑f₂ g))) f₁
g : G
⊢ ↑(map f₁ f₂ h) (↑inr g) = ↑inr (↑f₂ g)
simp [map]