∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : FiniteDimensional K V] (f : V →ₗ[K] V) (h_inj : Function.Injective ⇑f),
  ⇑(LinearEquiv.ofInjectiveEndo f h_inj) = ⇑f