∀ (K : Type u) [inst : Field K] (V : FGModuleCat K) (f : ↑(FGModuleCat.FGModuleCatDual K V)) (x : ↑V),
  (CategoryTheory.ConcreteCategory.hom (FGModuleCat.FGModuleCatEvaluation K V).hom) (f ⊗ₜ[K] x) = f.toFun x