∀ {α : Sort u_1} {β : Sort u_2} {toFun : α → β} {inj' : Function.Injective toFun} {toFun_1 : α → β}
  {inj'_1 : Function.Injective toFun_1},
  { toFun := toFun, inj' := inj' } = { toFun := toFun_1, inj' := inj'_1 } → toFun = toFun_1