application type mismatch with exact/refine

Stream: mathlib4

[Gareth Ma]

This seems very weird... the commented versions don't work

import Mathlib.Algebra.Category.FGModuleCat.Basic

open CategoryTheory FGModuleCat MonoidalCategory
open scoped TensorProduct

universe u
variable (k : Type u) [Field k] (V : FGModuleCat k)

noncomputable example : 𝟙_ (FGModuleCat k) ⟶ FGModuleCatDual k V ⊗ V :=
  /- by refine (coevaluation k V) ≫ (β_ V (FGModuleCatDual k V)).hom -/
  by refine ?_ ≫ (β_ V (FGModuleCatDual k V)).hom; exact coevaluation k V
  /- (coevaluation k V) ≫ (β_ V (FGModuleCatDual k V)).hom -/

[Gareth Ma]

Another version that works:

noncomputable def asdf' : 𝟙_ (FGModuleCat k) ⟶ FGModuleCatDual k V ⊗ V :=
  (FGModuleCatCoevaluation k V) ≫ (β_ V (FGModuleCatDual k V)).hom