-- 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)
⊢ 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))

Tactic:
have w := CategoryTheory.congr_fun
      (φ.hom.naturality (ModuleCat.ofHom (LinearMap.toSpanSingleton R M x))) (1 : R)