-- Module: Mathlib.Algebra.Category.ModuleCat.Tannaka
Goal:
R : Type u
inst : Ring R
φ :
  End (C := ModuleCat R ⥤+ AddCommGrpCat)
    (AdditiveFunctor.of
      (forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
        ModuleCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
        (CD := AddCommGrpCat.carrier)))
M : ModuleCat R
x : (↑M : Type u)
w :
  Eq (α :=
    (↑(Functor.obj
          (ObjectProperty.FullSubcategory.obj (P := additiveFunctor (ModuleCat R) AddCommGrpCat)
            (AdditiveFunctor.of
              (forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                (↑x1 : Type u) →+ (↑x2 : Type u)) (CD := AddCommGrpCat.carrier))))
          (ModuleCat.of R (↑M : Type u))) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) (X :=
            Functor.obj
              (ObjectProperty.FullSubcategory.obj (P := additiveFunctor (ModuleCat R) AddCommGrpCat)
                (AdditiveFunctor.of
                  (forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
                    ModuleCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                    (↑x1 : Type u) →+ (↑x2 : Type u)) (CD := AddCommGrpCat.carrier))))
              (ModuleCat.of R R))
            (Y :=
            Functor.obj
              (ObjectProperty.FullSubcategory.obj (P := additiveFunctor (ModuleCat R) AddCommGrpCat)
                (AdditiveFunctor.of
                  (forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
                    ModuleCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                    (↑x1 : Type u) →+ (↑x2 : Type u)) (CD := AddCommGrpCat.carrier))))
              (ModuleCat.of R (↑M : Type u)))
            (CategoryTheory.Functor.map
                (ObjectProperty.FullSubcategory.obj (P := additiveFunctor (ModuleCat R) AddCommGrpCat)
                  (AdditiveFunctor.of
                    (forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
                      (CC := ModuleCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                      (↑x1 : Type u) →+ (↑x2 : Type u)) (CD := AddCommGrpCat.carrier))))
                (ModuleCat.ofHom (LinearMap.toSpanSingleton R (↑M : Type u) x)) ≫
              φ.hom.app (ModuleCat.of R (↑M : Type u))) :
          (a : (↑((AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGrpCat)).obj.obj (ModuleCat.of R R)) : Type u)) →
            (↑((AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGrpCat)).obj.obj (ModuleCat.of R (↑M : Type u))) :
              Type u))
        1 :
      (↑(Functor.obj
            (ObjectProperty.FullSubcategory.obj (P := additiveFunctor (ModuleCat R) AddCommGrpCat)
              (AdditiveFunctor.of
                (forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
                  ModuleCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                  (↑x1 : Type u) →+ (↑x2 : Type u)) (CD := AddCommGrpCat.carrier))))
            (ModuleCat.of R (↑M : Type u))) :
        Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) (X :=
            Functor.obj
              (ObjectProperty.FullSubcategory.obj (P := additiveFunctor (ModuleCat R) AddCommGrpCat)
                (AdditiveFunctor.of
                  (forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
                    ModuleCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                    (↑x1 : Type u) →+ (↑x2 : Type u)) (CD := AddCommGrpCat.carrier))))
              (ModuleCat.of R R))
            (Y :=
            Functor.obj
              (ObjectProperty.FullSubcategory.obj (P := additiveFunctor (ModuleCat R) AddCommGrpCat)
                (AdditiveFunctor.of
                  (forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
                    ModuleCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                    (↑x1 : Type u) →+ (↑x2 : Type u)) (CD := AddCommGrpCat.carrier))))
              (ModuleCat.of R (↑M : Type u)))
            (φ.hom.app (ModuleCat.of R R) ≫
              CategoryTheory.Functor.map
                (ObjectProperty.FullSubcategory.obj (P := additiveFunctor (ModuleCat R) AddCommGrpCat)
                  (AdditiveFunctor.of
                    (forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
                      (CC := ModuleCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                      (↑x1 : Type u) →+ (↑x2 : Type u)) (CD := AddCommGrpCat.carrier))))
                (ModuleCat.ofHom (LinearMap.toSpanSingleton R (↑M : Type u) x))) :
          (a : (↑((AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGrpCat)).obj.obj (ModuleCat.of R R)) : Type u)) →
            (↑((AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGrpCat)).obj.obj (ModuleCat.of R (↑M : Type u))) :
              Type u))
        1 :
      (↑(Functor.obj
            (ObjectProperty.FullSubcategory.obj (P := additiveFunctor (ModuleCat R) AddCommGrpCat)
              (AdditiveFunctor.of
                (forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
                  ModuleCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                  (↑x1 : Type u) →+ (↑x2 : Type u)) (CD := AddCommGrpCat.carrier))))
            (ModuleCat.of R (↑M : Type u))) :
        Type u))
⊢ Eq (α :=
    (↑(Functor.obj
          (ObjectProperty.FullSubcategory.obj (P := additiveFunctor (ModuleCat R) AddCommGrpCat)
            (AdditiveFunctor.of
              (forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                (↑x1 : Type u) →+ (↑x2 : Type u)) (CD := AddCommGrpCat.carrier))))
          M) :
      Type u))
    ((AddCommGrpCat.Hom.hom
            (NatTrans.app
              (InducedCategory.Hom.hom
                (End.asHom
                  ((fun (r : R) ↦
                      (ObjectProperty.homMk (P := additiveFunctor (ModuleCat R) AddCommGrpCat)
                          {
                            app := fun (M : ModuleCat R) ↦
                              AddCommGrpCat.ofHom (DistribSMul.toAddMonoidHom (↑M : Type u) r),
                            naturality := ⋯ } :
                        Quiver.Hom (V :=
                          ObjectProperty.FullSubcategory (C := ModuleCat R ⥤ AddCommGrpCat)
                            (additiveFunctor (ModuleCat R) AddCommGrpCat))
                          (AdditiveFunctor.of
                            (forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
                              (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := ModuleCat.carrier) AddCommGrpCat (FD :=
                              fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
                              AddCommGrpCat.carrier)))
                          (AdditiveFunctor.of
                            (forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
                              (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := ModuleCat.carrier) AddCommGrpCat (FD :=
                              fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
                              AddCommGrpCat.carrier)))))
                    ((fun
                          (φ :
                            End (C := ModuleCat R ⥤+ AddCommGrpCat)
                              (AdditiveFunctor.of
                                (forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
                                  (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := ModuleCat.carrier) AddCommGrpCat (FD :=
                                  fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
                                  AddCommGrpCat.carrier)))) ↦
                        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                                (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := AddCommGrpCat.carrier) (X :=
                                Functor.obj
                                  (ObjectProperty.FullSubcategory.obj (P := additiveFunctor (ModuleCat R) AddCommGrpCat)
                                    (AdditiveFunctor.of
                                      (forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
                                        (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := ModuleCat.carrier) AddCommGrpCat
                                        (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
                                        (CD := AddCommGrpCat.carrier))))
                                  (ModuleCat.of R R))
                                (φ.hom.app (ModuleCat.of R R)) :
                              (a :
                                  (↑((AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGrpCat)).obj.obj
                                        (ModuleCat.of R R)) :
                                    Type u)) →
                                (↑((AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGrpCat)).obj.obj
                                      (ModuleCat.of R R)) :
                                  Type u))
                            1 :
                          (↑(Functor.obj
                                (ObjectProperty.FullSubcategory.obj (P := additiveFunctor (ModuleCat R) AddCommGrpCat)
                                  (AdditiveFunctor.of
                                    (forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
                                      (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := ModuleCat.carrier) AddCommGrpCat
                                      (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
                                      AddCommGrpCat.carrier))))
                                (ModuleCat.of R R)) :
                            Type u)))
                      φ))))
              M) :
          (a : (↑((AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGrpCat)).obj.obj M) : Type u)) →
            (↑((AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGrpCat)).obj.obj M) : Type u))
        x :
      (↑(Functor.obj
            (ObjectProperty.FullSubcategory.obj (P := additiveFunctor (ModuleCat R) AddCommGrpCat)
              (AdditiveFunctor.of
                (forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
                  ModuleCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                  (↑x1 : Type u) →+ (↑x2 : Type u)) (CD := AddCommGrpCat.carrier))))
            M) :
        Type u))
    ((AddCommGrpCat.Hom.hom (φ.asHom.hom.app M) :
          (a : (↑((AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGrpCat)).obj.obj M) : Type u)) →
            (↑((AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGrpCat)).obj.obj M) : Type u))
        x :
      (↑(Functor.obj
            (ObjectProperty.FullSubcategory.obj (P := additiveFunctor (ModuleCat R) AddCommGrpCat)
              (AdditiveFunctor.of
                (forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
                  ModuleCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                  (↑x1 : Type u) →+ (↑x2 : Type u)) (CD := AddCommGrpCat.carrier))))
            M) :
        Type u))

Tactic:
w.symm.trans (congr_arg (φ.hom.app M) (one_smul R x))

Premises used: CategoryTheory.ConcreteCategory.hom, one_smul, congr_arg, CategoryTheory.InducedCategory.Hom.hom, Eq.symm, DFunLike.coe, CategoryTheory.NatTrans.app, Eq.trans