-- Module: Mathlib.RepresentationTheory.FDRep
Goal:
R : Type u
G : Type v
inst : CommRing R
inst_1 : Monoid G
V : FDRep R G
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))
⊢ (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.ρ

Tactic:
ext g v