{N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} →
      [inst : Group N] →
        [inst_1 : Group E] →
          [inst_2 : Group G] →
            {S : GroupExtension N E G} →
              {E' : Type u_4} →
                [inst_3 : Group E'] →
                  {S' : GroupExtension N E' G} →
                    (toFun : E → E') →
                      (invFun : E' → E) →
                        (left_inv : autoParam (Function.LeftInverse invFun toFun) Equiv.left_inv._autoParam) →
                          (right_inv : autoParam (Function.RightInverse invFun toFun) Equiv.right_inv._autoParam) →
                            (map_mul' : ∀ (x y : E), toFun (x * y) = toFun x * toFun y) →
                              ⇑{ toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv,
                                        map_mul' := map_mul' } ∘
                                    ⇑S.inl =
                                  ⇑S'.inl →
                                ⇑S'.rightHom ∘
                                      ⇑{ toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv,
                                          map_mul' := map_mul' } =
                                    ⇑S.rightHom →
                                  S.Equiv S'