-- Lean 4 proof step from Mathlib.RepresentationTheory.FDRep (goal)
Goal:
k : Type u
G : Type v
V : Type u
inst : Field k
inst_1 : Group G
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : FiniteDimensional k V
ρV : Representation k G V
W : FDRep k G
g : G
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V ⟶
      (of (ρV.linHom W.ρ)).V)
    (CategoryStruct.comp (Y :=
        (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V)
        (((MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).ρ :
              (a : G) → End (of ρV.dual ⊗ W).V)
            g :
          End (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V)
        (Iso.hom (dualTensorIsoLinHomAux ρV W) :
          (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V ⟶
            (of (ρV.linHom W.ρ)).V) :
      (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V ⟶
        (of (ρV.linHom W.ρ)).V)
    (CategoryStruct.comp (Y := (of (ρV.linHom W.ρ)).V)
        (Iso.hom (dualTensorIsoLinHomAux ρV W) :
          (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V ⟶
            (of (ρV.linHom W.ρ)).V)
        (((of (ρV.linHom W.ρ)).ρ : (a : G) → End (of (ρV.linHom W.ρ)).V) g : End (of (ρV.linHom W.ρ)).V) :
      (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V ⟶
        (of (ρV.linHom W.ρ)).V)
have h : Eq (α :=
  (↑((MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V.obj (P :=
          ModuleCat.isFG k)) :
      Type u) →ₗ[k]
    (↑((of (ρV.linHom W.ρ)).V.obj (P := ModuleCat.isFG k)) : Type u))
  (ModuleCat.Hom.hom
      (InducedCategory.Hom.hom
        (CategoryStruct.comp (Y :=
          (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V)
          (((MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).ρ :
                (a : G) → End (of ρV.dual ⊗ W).V)
              g :
            End (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V)
          (Iso.hom (dualTensorIsoLinHomAux ρV W) :
            (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V ⟶
              (of (ρV.linHom W.ρ)).V))) :
    (↑((MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V.obj (P :=
            ModuleCat.isFG k)) :
        Type u) →ₗ[k]
      (↑((of (ρV.linHom W.ρ)).V.obj (P := ModuleCat.isFG k)) : Type u))
  (ModuleCat.Hom.hom
      (InducedCategory.Hom.hom
        (CategoryStruct.comp (Y := (of (ρV.linHom W.ρ)).V)
          (Iso.hom (dualTensorIsoLinHomAux ρV W) :
            (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V ⟶
              (of (ρV.linHom W.ρ)).V)
          (((of (ρV.linHom W.ρ)).ρ : (a : G) → End (of (ρV.linHom W.ρ)).V) g : End (of (ρV.linHom W.ρ)).V))) :
    (↑((MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V.obj (P :=
            ModuleCat.isFG k)) :
        Type u) →ₗ[k]
      (↑((of (ρV.linHom W.ρ)).V.obj (P := ModuleCat.isFG k)) : Type u))
Tactic: ext : 1