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

Tactic:
ext x