∀ {N : Type u_2} {G : Type u_3} {H : Type u_1} [inst : Group N] [inst_1 : Group G] [inst_2 : Group H]
  {φ : G →* MulAut N} (fn : N →* H) (fg : G →* H),
  (∀ (g : G), fn.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (fg g))).comp fn) →
    ∀ (a b : N ⋊[φ] G), fn (a * b).left * fg (a * b).right = fn a.left * fg a.right * (fn b.left * fg b.right)