-- 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)))
h :
  ∀ (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))))
            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))
⊢ (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)))
        φ) =
    φ

Tactic:
ext M (x : M)