-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M_1 : ModuleCat (↑R : Type u)
M N : (Spec R).Modules
f : Functor.obj modulesSpecToSheaf M ⟶ Functor.obj modulesSpecToSheaf N
X Y : (Opens ↥(Spec R))ᵒᵖ
i : X ⟶ Y
x : (↑(M.val.obj X) : Type u)
⊢ Eq (α :=
    (↑(Functor.obj
          (ModuleCat.restrictScalars
            (RingCat.Hom.hom
              (CategoryTheory.Functor.map
                (ObjectProperty.FullSubcategory.obj (P :=
                  CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
                i)))
          (N.val.obj Y)) :
      Type u))
    ((ModuleCat.Hom.hom
            (M.val.map i ≫
              CategoryTheory.Functor.map
                (ModuleCat.restrictScalars
                  (RingCat.Hom.hom
                    (CategoryTheory.Functor.map
                      (ObjectProperty.FullSubcategory.obj (P :=
                        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
                      i)))
                ((fun (U : (Opens ↥(Spec R))ᵒᵖ) ↦
                    ModuleCat.ofHom
                      { toAddHom := (ModuleCat.Hom.hom (f.hom.app U)).toAddHom, map_smul' := ⋯ :
                        LinearMap (R :=
                          (↑(Functor.obj
                                (ObjectProperty.FullSubcategory.obj (P :=
                                  CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R)))
                                  (Spec R).ringCatSheaf)
                                U) :
                            Type u))
                          (RingHom.id
                            (↑(Functor.obj
                                  (ObjectProperty.FullSubcategory.obj (P :=
                                    CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R)))
                                    (Spec R).ringCatSheaf)
                                  U) :
                              Type u))
                          (↑(M.val.1 U) : Type u) (↑(N.val.1 U) : Type u) })
                  Y)) :
          (a : (↑(M.val.obj X) : Type u)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom ((Spec R).ringCatSheaf.obj.map i))).obj (N.val.obj Y)) :
              Type u))
        x :
      (↑(Functor.obj
            (ModuleCat.restrictScalars
              (RingCat.Hom.hom
                (CategoryTheory.Functor.map
                  (ObjectProperty.FullSubcategory.obj (P :=
                    CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
                  i)))
            (N.val.obj Y)) :
        Type u))
    ((ModuleCat.Hom.hom
            ((fun (U : (Opens ↥(Spec R))ᵒᵖ) ↦
                  ModuleCat.ofHom
                    { toAddHom := (ModuleCat.Hom.hom (f.hom.app U)).toAddHom, map_smul' := ⋯ :
                      LinearMap (R :=
                        (↑(Functor.obj
                              (ObjectProperty.FullSubcategory.obj (P :=
                                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R)))
                                (Spec R).ringCatSheaf)
                              U) :
                          Type u))
                        (RingHom.id
                          (↑(Functor.obj
                                (ObjectProperty.FullSubcategory.obj (P :=
                                  CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R)))
                                  (Spec R).ringCatSheaf)
                                U) :
                            Type u))
                        (↑(M.val.1 U) : Type u) (↑(N.val.1 U) : Type u) })
                X ≫
              N.val.map i) :
          (a : (↑(M.val.obj X) : Type u)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom ((Spec R).ringCatSheaf.obj.map i))).obj (N.val.obj Y)) :
              Type u))
        x :
      (↑(Functor.obj
            (ModuleCat.restrictScalars
              (RingCat.Hom.hom
                (CategoryTheory.Functor.map
                  (ObjectProperty.FullSubcategory.obj (P :=
                    CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
                  i)))
            (N.val.obj Y)) :
        Type u))

Tactic:
congr($(f.1.naturality i).hom x)

Premises used: congrArg, id, CategoryTheory.NatTrans.naturality, CategoryTheory.InducedCategory.Hom.hom, ModuleCat.Hom.hom, DFunLike.coe