-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Tannaka (hypothesis)
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))))
          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))
have 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))
Tactic: have w := CategoryTheory.congr_fun
      (φ.hom.naturality (ModuleCat.ofHom (LinearMap.toSpanSingleton R M x))) (1 : R)