-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Modules.Tilde (goal)
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
⊢ 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
have 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' := sorry :
                        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' := sorry :
                      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: ext x