∀ {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} {toFun : G → E} {rightInverse_rightHom : Function.RightInverse toFun ⇑S.rightHom}
  {toFun_1 : G → E} {rightInverse_rightHom_1 : Function.RightInverse toFun_1 ⇑S.rightHom},
  { toFun := toFun, rightInverse_rightHom := rightInverse_rightHom } =
      { toFun := toFun_1, rightInverse_rightHom := rightInverse_rightHom_1 } →
    toFun = toFun_1