∀ {N : Type u_3} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {E : Type u_1} [inst_2 : Group E]
  {S : GroupExtension N E G} {E' : Type u_4} [inst_3 : Group E'] {S' : GroupExtension N E' G} (f : E →* E'),
  f.comp S.inl = S'.inl →
    S'.rightHom.comp f = S.rightHom →
      ∀ (e : E),
        (fun e' =>
              let e := Function.surjInv ⋯ (S'.rightHom e');
              e * S.inl (Function.invFun (⇑S'.inl) ((f e)⁻¹ * e')))
            ((↑f).toFun e) =
          e