-- Lean 4 proof step from Mathlib.RepresentationTheory.FDRep (goal)
Goal:
R : Type u
G : Type v
inst : CommRing R
inst_1 : Monoid G
V : FDRep R G
⊢ (Functor.obj
        (forget₂ (FDRep R G) (FC :=
          Action.HomSubtype (FGModuleCat R) G (FV :=
            fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
            (↑(X.obj (P := ModuleCat.isFG R)) : Type u) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type u)) (CV :=
            fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
            (↑(X.obj (P := ModuleCat.isFG R)) : Type u)))
          (CC := fun (X : Action.{u, u + 1, v} (FGModuleCat R) G) ↦ (↑(X.V.obj (P := ModuleCat.isFG R)) : Type u))
          (Rep R G) (FD := fun (A B : Rep R G) ↦ A.ρ.IntertwiningMap B.ρ) (CD := Rep.V))
        V).ρ =
    V.ρ
have h : ∀ (g : G)
  (v :
    (↑(Functor.obj
          (forget₂ (FDRep R G) (FC :=
            Action.HomSubtype (FGModuleCat R) G (FV :=
              fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
              (↑(X.obj (P := ModuleCat.isFG R)) : Type u) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type u)) (CV :=
              fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
              (↑(X.obj (P := ModuleCat.isFG R)) : Type u)))
            (CC := fun (X : Action.{u, u + 1, v} (FGModuleCat R) G) ↦ (↑(X.V.obj (P := ModuleCat.isFG R)) : Type u))
            (Rep R G) (FD := fun (A B : Rep R G) ↦ A.ρ.IntertwiningMap B.ρ) (CD := Rep.V))
          V) :
      Type u)),
  Eq (α :=
    (↑(Functor.obj
          (forget₂ (FDRep R G) (FC :=
            Action.HomSubtype (FGModuleCat R) G (FV :=
              fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
              (↑(X.obj (P := ModuleCat.isFG R)) : Type u) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type u)) (CV :=
              fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
              (↑(X.obj (P := ModuleCat.isFG R)) : Type u)))
            (CC := fun (X : Action.{u, u + 1, v} (FGModuleCat R) G) ↦ (↑(X.V.obj (P := ModuleCat.isFG R)) : Type u))
            (Rep R G) (FD := fun (A B : Rep R G) ↦ A.ρ.IntertwiningMap B.ρ) (CD := Rep.V))
          V) :
      Type u))
    (((((Functor.obj
                    (forget₂ (FDRep R G) (FC :=
                      Action.HomSubtype (FGModuleCat R) G (FV :=
                        fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
                        (↑(X.obj (P := ModuleCat.isFG R)) : Type u) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type u))
                        (CV := fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
                        (↑(X.obj (P := ModuleCat.isFG R)) : Type u)))
                      (CC := fun (X : Action.{u, u + 1, v} (FGModuleCat R) G) ↦
                      (↑(X.V.obj (P := ModuleCat.isFG R)) : Type u)) (Rep R G) (FD := fun (A B : Rep R G) ↦
                      A.ρ.IntertwiningMap B.ρ) (CD := Rep.V))
                    V).ρ :
                (a : G) →
                  (↑((forget₂ (FDRep R G) (Rep R G)).obj V) : Type u) →ₗ[R]
                    (↑((forget₂ (FDRep R G) (Rep R G)).obj V) : Type u))
              g :
            (↑(Functor.obj
                    (forget₂ (FDRep R G) (FC :=
                      Action.HomSubtype (FGModuleCat R) G (FV :=
                        fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
                        (↑(X.obj (P := ModuleCat.isFG R)) : Type u) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type u))
                        (CV := fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
                        (↑(X.obj (P := ModuleCat.isFG R)) : Type u)))
                      (CC := fun (X : Action.{u, u + 1, v} (FGModuleCat R) G) ↦
                      (↑(X.V.obj (P := ModuleCat.isFG R)) : Type u)) (Rep R G) (FD := fun (A B : Rep R G) ↦
                      A.ρ.IntertwiningMap B.ρ) (CD := Rep.V))
                    V) :
                Type u) →ₗ[R]
              (↑(Functor.obj
                    (forget₂ (FDRep R G) (FC :=
                      Action.HomSubtype (FGModuleCat R) G (FV :=
                        fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
                        (↑(X.obj (P := ModuleCat.isFG R)) : Type u) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type u))
                        (CV := fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
                        (↑(X.obj (P := ModuleCat.isFG R)) : Type u)))
                      (CC := fun (X : Action.{u, u + 1, v} (FGModuleCat R) G) ↦
                      (↑(X.V.obj (P := ModuleCat.isFG R)) : Type u)) (Rep R G) (FD := fun (A B : Rep R G) ↦
                      A.ρ.IntertwiningMap B.ρ) (CD := Rep.V))
                    V) :
                Type u)) :
          (a : (↑((forget₂ (FDRep R G) (Rep R G)).obj V) : Type u)) →
            (↑((forget₂ (FDRep R G) (Rep R G)).obj V) : Type u))
        v :
      (↑(Functor.obj
            (forget₂ (FDRep R G) (FC :=
              Action.HomSubtype (FGModuleCat R) G (FV :=
                fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
                (↑(X.obj (P := ModuleCat.isFG R)) : Type u) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type u)) (CV :=
                fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
                (↑(X.obj (P := ModuleCat.isFG R)) : Type u)))
              (CC := fun (X : Action.{u, u + 1, v} (FGModuleCat R) G) ↦ (↑(X.V.obj (P := ModuleCat.isFG R)) : Type u))
              (Rep R G) (FD := fun (A B : Rep R G) ↦ A.ρ.IntertwiningMap B.ρ) (CD := Rep.V))
            V) :
        Type u))
    ((((V.ρ :
                (a : G) →
                  (↑((forget₂ (FDRep R G) (Rep R G)).obj V) : Type u) →ₗ[R]
                    (↑((forget₂ (FDRep R G) (Rep R G)).obj V) : Type u))
              g :
            (↑(Functor.obj
                    (forget₂ (FDRep R G) (FC :=
                      Action.HomSubtype (FGModuleCat R) G (FV :=
                        fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
                        (↑(X.obj (P := ModuleCat.isFG R)) : Type u) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type u))
                        (CV := fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
                        (↑(X.obj (P := ModuleCat.isFG R)) : Type u)))
                      (CC := fun (X : Action.{u, u + 1, v} (FGModuleCat R) G) ↦
                      (↑(X.V.obj (P := ModuleCat.isFG R)) : Type u)) (Rep R G) (FD := fun (A B : Rep R G) ↦
                      A.ρ.IntertwiningMap B.ρ) (CD := Rep.V))
                    V) :
                Type u) →ₗ[R]
              (↑(Functor.obj
                    (forget₂ (FDRep R G) (FC :=
                      Action.HomSubtype (FGModuleCat R) G (FV :=
                        fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
                        (↑(X.obj (P := ModuleCat.isFG R)) : Type u) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type u))
                        (CV := fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
                        (↑(X.obj (P := ModuleCat.isFG R)) : Type u)))
                      (CC := fun (X : Action.{u, u + 1, v} (FGModuleCat R) G) ↦
                      (↑(X.V.obj (P := ModuleCat.isFG R)) : Type u)) (Rep R G) (FD := fun (A B : Rep R G) ↦
                      A.ρ.IntertwiningMap B.ρ) (CD := Rep.V))
                    V) :
                Type u)) :
          (a : (↑((forget₂ (FDRep R G) (Rep R G)).obj V) : Type u)) →
            (↑((forget₂ (FDRep R G) (Rep R G)).obj V) : Type u))
        v :
      (↑(Functor.obj
            (forget₂ (FDRep R G) (FC :=
              Action.HomSubtype (FGModuleCat R) G (FV :=
                fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
                (↑(X.obj (P := ModuleCat.isFG R)) : Type u) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type u)) (CV :=
                fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
                (↑(X.obj (P := ModuleCat.isFG R)) : Type u)))
              (CC := fun (X : Action.{u, u + 1, v} (FGModuleCat R) G) ↦ (↑(X.V.obj (P := ModuleCat.isFG R)) : Type u))
              (Rep R G) (FD := fun (A B : Rep R G) ↦ A.ρ.IntertwiningMap B.ρ) (CD := Rep.V))
            V) :
        Type u))
Tactic: ext g v