-- Lean 4 proof step from Mathlib.RepresentationTheory.FDRep (goal)
Goal:
R k : Type u
G : Type v
inst : CommRing R
inst_1 : Field k
inst_2 : Monoid G
X Y : FDRep R G
f : X ⟶ Y
g : G
⊢ Eq (α :=
    (↑(Action.V
            (Functor.obj
              (Functor.mapAction
                (forget₂ (FGModuleCat R) (FC :=
                  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)) (CC :=
                  fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
                  (↑(X.obj (P := ModuleCat.isFG R)) : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
                  (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                G)
              X)) :
        Type u) →ₗ[R]
      (↑(Action.V
            (Functor.obj
              (Functor.mapAction
                (forget₂ (FGModuleCat R) (FC :=
                  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)) (CC :=
                  fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
                  (↑(X.obj (P := ModuleCat.isFG R)) : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
                  (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                G)
              Y)) :
        Type u))
    (ModuleCat.Hom.hom
          (CategoryTheory.Functor.map
            (forget₂ (FGModuleCat R) (FC :=
              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)) (CC :=
              fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
              (↑(X.obj (P := ModuleCat.isFG R)) : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
              (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
            f.hom) ∘ₗ
        ((Action.V
                      (Functor.obj
                        (Functor.mapAction
                          (forget₂ (FGModuleCat R) (FC :=
                            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))
                            (CC := fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
                            (↑(X.obj (P := ModuleCat.isFG R)) : Type u)) (ModuleCat R) (FD :=
                            fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                          G)
                        X)).endRingEquiv.toMonoidHom.comp
              (Action.ρ
                (Functor.obj
                  (Functor.mapAction
                    (forget₂ (FGModuleCat R) (FC :=
                      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))
                      (CC := fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
                      (↑(X.obj (P := ModuleCat.isFG R)) : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
                      (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                    G)
                  X)) :
            (a : G) →
              (↑(((forget₂ (FGModuleCat R) (ModuleCat R)).mapAction G).obj X).V : Type u) →ₗ[R]
                (↑(((forget₂ (FGModuleCat R) (ModuleCat R)).mapAction G).obj X).V : Type u))
          g :
      (↑(Action.V
              (Functor.obj
                (Functor.mapAction
                  (forget₂ (FGModuleCat R) (FC :=
                    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))
                    (CC := fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
                    (↑(X.obj (P := ModuleCat.isFG R)) : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
                    (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                  G)
                X)) :
          Type u) →ₗ[R]
        (↑(Action.V
              (Functor.obj
                (Functor.mapAction
                  (forget₂ (FGModuleCat R) (FC :=
                    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))
                    (CC := fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
                    (↑(X.obj (P := ModuleCat.isFG R)) : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
                    (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                  G)
                Y)) :
          Type u))
    (((Action.V
                      (Functor.obj
                        (Functor.mapAction
                          (forget₂ (FGModuleCat R) (FC :=
                            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))
                            (CC := fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
                            (↑(X.obj (P := ModuleCat.isFG R)) : Type u)) (ModuleCat R) (FD :=
                            fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                          G)
                        Y)).endRingEquiv.toMonoidHom.comp
              (Action.ρ
                (Functor.obj
                  (Functor.mapAction
                    (forget₂ (FGModuleCat R) (FC :=
                      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))
                      (CC := fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
                      (↑(X.obj (P := ModuleCat.isFG R)) : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
                      (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                    G)
                  Y)) :
            (a : G) →
              (↑(((forget₂ (FGModuleCat R) (ModuleCat R)).mapAction G).obj Y).V : Type u) →ₗ[R]
                (↑(((forget₂ (FGModuleCat R) (ModuleCat R)).mapAction G).obj Y).V : Type u))
          g ∘ₗ
        ModuleCat.Hom.hom
          (CategoryTheory.Functor.map
            (forget₂ (FGModuleCat R) (FC :=
              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)) (CC :=
              fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
              (↑(X.obj (P := ModuleCat.isFG R)) : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
              (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
            f.hom) :
      (↑(Action.V
              (Functor.obj
                (Functor.mapAction
                  (forget₂ (FGModuleCat R) (FC :=
                    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))
                    (CC := fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
                    (↑(X.obj (P := ModuleCat.isFG R)) : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
                    (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                  G)
                X)) :
          Type u) →ₗ[R]
        (↑(Action.V
              (Functor.obj
                (Functor.mapAction
                  (forget₂ (FGModuleCat R) (FC :=
                    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))
                    (CC := fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
                    (↑(X.obj (P := ModuleCat.isFG R)) : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
                    (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                  G)
                Y)) :
          Type u))
have h : ∀
  (x :
    (↑(Action.V
          (Functor.obj
            (Functor.mapAction
              (forget₂ (FGModuleCat R) (FC :=
                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)) (CC :=
                fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
                (↑(X.obj (P := ModuleCat.isFG R)) : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
                (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
              G)
            X)) :
      Type u)),
  Eq (α :=
    (↑(Action.V
          (Functor.obj
            (Functor.mapAction
              (forget₂ (FGModuleCat R) (FC :=
                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)) (CC :=
                fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
                (↑(X.obj (P := ModuleCat.isFG R)) : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
                (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
              G)
            Y)) :
      Type u))
    (((ModuleCat.Hom.hom
                (CategoryTheory.Functor.map
                  (forget₂ (FGModuleCat R) (FC :=
                    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))
                    (CC := fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
                    (↑(X.obj (P := ModuleCat.isFG R)) : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
                    (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                  f.hom) ∘ₗ
              ((Action.V
                            (Functor.obj
                              (Functor.mapAction
                                (forget₂ (FGModuleCat R) (FC :=
                                  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))
                                  (CC :=
                                  fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
                                  (↑(X.obj (P := ModuleCat.isFG R)) : Type u)) (ModuleCat R) (FD :=
                                  fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD :=
                                  ModuleCat.carrier))
                                G)
                              X)).endRingEquiv.toMonoidHom.comp
                    (Action.ρ
                      (Functor.obj
                        (Functor.mapAction
                          (forget₂ (FGModuleCat R) (FC :=
                            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))
                            (CC := fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
                            (↑(X.obj (P := ModuleCat.isFG R)) : Type u)) (ModuleCat R) (FD :=
                            fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                          G)
                        X)) :
                  (a : G) →
                    (↑(((forget₂ (FGModuleCat R) (ModuleCat R)).mapAction G).obj X).V : Type u) →ₗ[R]
                      (↑(((forget₂ (FGModuleCat R) (ModuleCat R)).mapAction G).obj X).V : Type u))
                g :
            (↑(Action.V
                    (Functor.obj
                      (Functor.mapAction
                        (forget₂ (FGModuleCat R) (FC :=
                          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))
                          (CC := fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
                          (↑(X.obj (P := ModuleCat.isFG R)) : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
                          (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                        G)
                      X)) :
                Type u) →ₗ[R]
              (↑(Action.V
                    (Functor.obj
                      (Functor.mapAction
                        (forget₂ (FGModuleCat R) (FC :=
                          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))
                          (CC := fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
                          (↑(X.obj (P := ModuleCat.isFG R)) : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
                          (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                        G)
                      Y)) :
                Type u)) :
          (a : (↑(((forget₂ (FGModuleCat R) (ModuleCat R)).mapAction G).obj X).V : Type u)) →
            (↑(((forget₂ (FGModuleCat R) (ModuleCat R)).mapAction G).obj Y).V : Type u))
        x :
      (↑(Action.V
            (Functor.obj
              (Functor.mapAction
                (forget₂ (FGModuleCat R) (FC :=
                  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)) (CC :=
                  fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
                  (↑(X.obj (P := ModuleCat.isFG R)) : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
                  (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                G)
              Y)) :
        Type u))
    (((((Action.V
                            (Functor.obj
                              (Functor.mapAction
                                (forget₂ (FGModuleCat R) (FC :=
                                  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))
                                  (CC :=
                                  fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
                                  (↑(X.obj (P := ModuleCat.isFG R)) : Type u)) (ModuleCat R) (FD :=
                                  fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD :=
                                  ModuleCat.carrier))
                                G)
                              Y)).endRingEquiv.toMonoidHom.comp
                    (Action.ρ
                      (Functor.obj
                        (Functor.mapAction
                          (forget₂ (FGModuleCat R) (FC :=
                            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))
                            (CC := fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
                            (↑(X.obj (P := ModuleCat.isFG R)) : Type u)) (ModuleCat R) (FD :=
                            fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                          G)
                        Y)) :
                  (a : G) →
                    (↑(((forget₂ (FGModuleCat R) (ModuleCat R)).mapAction G).obj Y).V : Type u) →ₗ[R]
                      (↑(((forget₂ (FGModuleCat R) (ModuleCat R)).mapAction G).obj Y).V : Type u))
                g ∘ₗ
              ModuleCat.Hom.hom
                (CategoryTheory.Functor.map
                  (forget₂ (FGModuleCat R) (FC :=
                    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))
                    (CC := fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
                    (↑(X.obj (P := ModuleCat.isFG R)) : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
                    (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                  f.hom) :
            (↑(Action.V
                    (Functor.obj
                      (Functor.mapAction
                        (forget₂ (FGModuleCat R) (FC :=
                          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))
                          (CC := fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
                          (↑(X.obj (P := ModuleCat.isFG R)) : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
                          (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                        G)
                      X)) :
                Type u) →ₗ[R]
              (↑(Action.V
                    (Functor.obj
                      (Functor.mapAction
                        (forget₂ (FGModuleCat R) (FC :=
                          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))
                          (CC := fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
                          (↑(X.obj (P := ModuleCat.isFG R)) : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
                          (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                        G)
                      Y)) :
                Type u)) :
          (a : (↑(((forget₂ (FGModuleCat R) (ModuleCat R)).mapAction G).obj X).V : Type u)) →
            (↑(((forget₂ (FGModuleCat R) (ModuleCat R)).mapAction G).obj Y).V : Type u))
        x :
      (↑(Action.V
            (Functor.obj
              (Functor.mapAction
                (forget₂ (FGModuleCat R) (FC :=
                  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)) (CC :=
                  fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
                  (↑(X.obj (P := ModuleCat.isFG R)) : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
                  (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                G)
              Y)) :
        Type u))
Tactic: ext x