-- 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
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:
exact ConcreteCategory.congr_hom ((forget (FGModuleCat R)).congr_map (f.comm g)) x

Premises used: CategoryTheory.forget, CategoryTheory.Functor.congr_map, FGModuleCat, CategoryTheory.ConcreteCategory.congr_hom, Action.Hom.comm