-- 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
U : (Opens ↥(Spec R))ᵒᵖ
t :
  (↑(Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
        U) :
    Type u)
m : (↑(M.val.1 U) : Type u)
x : ↥(Spec R)
hxU : x ∈ unop U
r : (↑R : Type u)
hxr : x ∈ (↑(basicOpen r) : Set (PrimeSpectrum (↑R : Type u)))
hrU : basicOpen r ≤ unop U
⊢ Eq (α :=
    (↑((Functor.obj modulesSpecToSheaf N).obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))).obj
          (op (basicOpen r))) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑R : Type u)) ↦
            LinearMap (R := (↑R : Type u)) (RingHom.id (↑R : Type u)) (↑x1 : Type u) (↑x2 : Type u)) (CC :=
            ModuleCat.carrier)
            ((Functor.obj modulesSpecToSheaf N).obj (P :=
                  CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))).map
              (homOfLE hrU).op) :
          (a : (↑((modulesSpecToSheaf.obj N).obj.obj (op (unop U))) : Type u)) →
            (↑((modulesSpecToSheaf.obj N).obj.obj (op (basicOpen r))) : Type u))
        ((ModuleCat.Hom.hom (f.hom.app U)).toFun (t • m)) :
      (↑((Functor.obj modulesSpecToSheaf N).obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))).obj
            (op (basicOpen r))) :
        Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑R : Type u)) ↦
            LinearMap (R := (↑R : Type u)) (RingHom.id (↑R : Type u)) (↑x1 : Type u) (↑x2 : Type u)) (CC :=
            ModuleCat.carrier)
            ((Functor.obj modulesSpecToSheaf N).obj (P :=
                  CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))).map
              (homOfLE hrU).op) :
          (a : (↑((modulesSpecToSheaf.obj N).obj.obj (op (unop U))) : Type u)) →
            (↑((modulesSpecToSheaf.obj N).obj.obj (op (basicOpen r))) : Type u))
        (HSMul.hSMul (α :=
          (↑(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) :
                (a : (↑((Spec R).ringCatSheaf.obj.obj U) : Type u)) → (↑((Spec R).ringCatSheaf.obj.obj U) : Type u))
              t :
            (↑(Functor.obj
                  (ObjectProperty.FullSubcategory.obj (P :=
                    CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
                  U) :
              Type u))
          ((ModuleCat.Hom.hom (f.hom.app U)).toFun m)) :
      (↑((Functor.obj modulesSpecToSheaf N).obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))).obj
            (op (basicOpen r))) :
        Type u))
have refine : (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑R : Type u)) ↦
        LinearMap (R := (↑R : Type u)) (RingHom.id (↑R : Type u)) (↑x1 : Type u) (↑x2 : Type u)) (CC :=
        ModuleCat.carrier)
        ((Functor.obj modulesSpecToSheaf N).obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))).map
          (homOfLE hrU).op) :
      (a : (↑((modulesSpecToSheaf.obj N).obj.obj (op (unop U))) : Type u)) →
        (↑((modulesSpecToSheaf.obj N).obj.obj (op (basicOpen r))) : Type u))
    ((ModuleCat.Hom.hom (f.hom.app U)).toFun (t • m)) =
  HSMul.hSMul (α :=
    (↑(Functor.obj (C := (Opens ↥(Spec R))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
          (op (basicOpen r))) :
      Type u))
    (β :=
    (↑(Functor.obj (C :=
          ModuleCat
            (↑(Functor.obj (C := (Opens ↥(Spec R))ᵒᵖ)
                  (ObjectProperty.FullSubcategory.obj (P :=
                    CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
                  (op (basicOpen r))) :
              Type u))
          (ModuleCat.restrictScalars
            (RingCat.Hom.hom
              (CategoryTheory.Functor.map
                (ObjectProperty.FullSubcategory.obj (P :=
                  CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
                (homOfLE hrU).op)))
          (N.val.obj (op (basicOpen r)))) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
            (X :=
            Functor.obj
              (ObjectProperty.FullSubcategory.obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
              (op (unop U)))
            (Y :=
            Functor.obj (C := (Opens ↥(Spec R))ᵒᵖ)
              (ObjectProperty.FullSubcategory.obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
              (op (basicOpen r)))
            (CategoryTheory.Functor.map
              (ObjectProperty.FullSubcategory.obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
              (homOfLE hrU).op) :
          (a : (↑((Spec R).ringCatSheaf.obj.obj (op (unop U))) : Type u)) →
            (↑((Spec R).ringCatSheaf.obj.obj (op (basicOpen r))) : Type u))
        t :
      (↑(Functor.obj (C := (Opens ↥(Spec R))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
            (op (basicOpen r))) :
        Type u))
    ((ConcreteCategory.hom (FC :=
            fun
              (x1 x2 :
                ModuleCat
                  (↑(Functor.obj
                        (ObjectProperty.FullSubcategory.obj (P :=
                          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
                        (op (unop U))) :
                    Type u)) ↦
            LinearMap (R :=
              (↑(Functor.obj
                    (ObjectProperty.FullSubcategory.obj (P :=
                      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
                    (op (unop U))) :
                Type u))
              (RingHom.id
                (↑(Functor.obj
                      (ObjectProperty.FullSubcategory.obj (P :=
                        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
                      (op (unop U))) :
                  Type u))
              (↑x1 : Type u) (↑x2 : Type u))
            (CC := ModuleCat.carrier) (N.val.map (homOfLE hrU).op) :
          (a : (↑(N.val.obj (op (unop U))) : Type u)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom ((Spec R).ringCatSheaf.obj.map (homOfLE hrU).op))).obj
                  (N.val.obj (op (basicOpen r)))) :
              Type u))
        ((ModuleCat.Hom.hom (f.hom.app U)).toFun m) :
      (↑(Functor.obj (C :=
            ModuleCat
              (↑(Functor.obj (C := (Opens ↥(Spec R))ᵒᵖ)
                    (ObjectProperty.FullSubcategory.obj (P :=
                      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
                    (op (basicOpen r))) :
                Type u))
            (ModuleCat.restrictScalars
              (RingCat.Hom.hom
                (CategoryTheory.Functor.map
                  (ObjectProperty.FullSubcategory.obj (P :=
                    CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
                  (homOfLE hrU).op)))
            (N.val.obj (op (basicOpen r)))) :
        Type u))
Tactic: refine Eq.trans ?_ (N.val.map_smul (homOfLE hrU).op t _).symm