-- Module: Mathlib.RepresentationTheory.FDRep
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
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))
⊢ 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))

Tactic:
ext x