∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  (inl inl_1 : N →* E) (e_inl : inl = inl_1) (rightHom rightHom_1 : E →* G) (e_rightHom : rightHom = rightHom_1)
  (inl_injective : Function.Injective ⇑inl) (range_inl_eq_ker_rightHom : inl.range = rightHom.ker)
  (rightHom_surjective : Function.Surjective ⇑rightHom),
  { inl := inl, rightHom := rightHom, inl_injective := inl_injective,
      range_inl_eq_ker_rightHom := range_inl_eq_ker_rightHom, rightHom_surjective := rightHom_surjective } =
    { inl := inl_1, rightHom := rightHom_1, inl_injective := ⋯, range_inl_eq_ker_rightHom := ⋯,
      rightHom_surjective := ⋯ }