∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} {inst : AddGroup N} {inst_1 : AddGroup E} {inst_2 : AddGroup G}
  {S : AddGroupExtension N E G} {E' : Type u_4} {inst_3 : AddGroup E'} {S' : AddGroupExtension N E' G}
  {toAddEquiv : E ≃+ E'} {inl_comm : ⇑toAddEquiv ∘ ⇑S.inl = ⇑S'.inl}
  {rightHom_comm : ⇑S'.rightHom ∘ ⇑toAddEquiv = ⇑S.rightHom} {toAddEquiv_1 : E ≃+ E'}
  {inl_comm_1 : ⇑toAddEquiv_1 ∘ ⇑S.inl = ⇑S'.inl} {rightHom_comm_1 : ⇑S'.rightHom ∘ ⇑toAddEquiv_1 = ⇑S.rightHom},
  { toAddEquiv := toAddEquiv, inl_comm := inl_comm, rightHom_comm := rightHom_comm } =
      { toAddEquiv := toAddEquiv_1, inl_comm := inl_comm_1, rightHom_comm := rightHom_comm_1 } →
    toAddEquiv = toAddEquiv_1