no goals
N : Type u_4
G : Type u_1
H : Type ?u.270290
inst✝⁴ : Group N
inst✝³ : Group G
inst✝² : Group H
φ : G →* MulAut N
N₁ : Type u_2
G₁ : Type u_3
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₁
⊢ MonoidHom.comp (map f₁ f₂ h) inr = MonoidHom.comp inr f₂
ext <;> simp [map]