-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
Goal:
R M A : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : Algebra R A
S : Type u
inst_5 : CommRing S
N : Type u
inst_6 : AddCommGroup N
inst_7 : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
V : Opens (↑(PrimeSpectrum.Top S) : Type u)
hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier
r : R
m :
  Functor.obj
    (ObjectProperty.FullSubcategory.obj (P :=
      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
      (structureSheafInType R M))
    (op U)
x : ↥(unop (op V))
rw :
  HSMul.hSMul (α := S) (β := Localizations N (↑x : (↑(PrimeSpectrum.Top S) : Type u))) ((σ : (a : R) → S) r : S)
      ((Localizations.comapFun f (↑x : (↑(PrimeSpectrum.Top S) : Type u)) :
            (a : Localizations M (PrimeSpectrum.comap σ (↑x : (↑(PrimeSpectrum.Top S) : Type u)))) →
              Localizations N (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
          ((↑m : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
            (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ U)
              (PrimeSpectrum.comap σ (↑x : (↑(PrimeSpectrum.Top S) : Type u))) ⋯)) :
        Localizations N (↑x : (↑(PrimeSpectrum.Top S) : Type u))) =
    HSMul.hSMul (α := S) (β := Localizations N (↑x : (↑(PrimeSpectrum.Top S) : Type u))) ((σ : (a : R) → S) r : S)
      ((Localizations.comapFun f (↑x : (↑(PrimeSpectrum.Top S) : Type u)) :
            (a : Localizations M (PrimeSpectrum.comap σ (↑x : (↑(PrimeSpectrum.Top S) : Type u)))) →
              Localizations N (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
          ((↑m : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
            (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ U)
              (PrimeSpectrum.comap σ (↑x : (↑(PrimeSpectrum.Top S) : Type u))) ⋯)) :
        Localizations N (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
⊢ (Localizations.comapFun f (↑x : (↑(PrimeSpectrum.Top S) : Type u)) :
        (a : Localizations M (PrimeSpectrum.comap σ (↑x : (↑(PrimeSpectrum.Top S) : Type u)))) →
          Localizations N (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
      (r •
        (↑m : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
          (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ U)
            (PrimeSpectrum.comap σ (↑x : (↑(PrimeSpectrum.Top S) : Type u))) ⋯)) =
    HSMul.hSMul (α := S) (β := Localizations N (↑x : (↑(PrimeSpectrum.Top S) : Type u))) ((σ : (a : R) → S) r : S)
      ((Localizations.comapFun f (↑x : (↑(PrimeSpectrum.Top S) : Type u)) :
            (a : Localizations M (PrimeSpectrum.comap σ (↑x : (↑(PrimeSpectrum.Top S) : Type u)))) →
              Localizations N (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
          ((↑m : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
            (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ U)
              (PrimeSpectrum.comap σ (↑x : (↑(PrimeSpectrum.Top S) : Type u))) ⋯)) :
        Localizations N (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
have rw₁ : HSMul.hSMul (α := S) (β := Localizations N (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
    ((algebraMap S S : (a : S) → S) ((σ : (a : R) → S) r : S) : S)
    ((Localizations.comapFun f (↑x : (↑(PrimeSpectrum.Top S) : Type u)) :
          (a : Localizations M (PrimeSpectrum.comap σ (↑x : (↑(PrimeSpectrum.Top S) : Type u)))) →
            Localizations N (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
        ((↑m : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
          (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ U)
            (PrimeSpectrum.comap σ (↑x : (↑(PrimeSpectrum.Top S) : Type u))) sorry)) :
      Localizations N (↑x : (↑(PrimeSpectrum.Top S) : Type u))) =
  HSMul.hSMul (α := S) (β := Localizations N (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
    ((algebraMap S S : (a : S) → S) ((σ : (a : R) → S) r : S) : S)
    ((Localizations.comapFun f (↑x : (↑(PrimeSpectrum.Top S) : Type u)) :
          (a : Localizations M (PrimeSpectrum.comap σ (↑x : (↑(PrimeSpectrum.Top S) : Type u)))) →
            Localizations N (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
        ((↑m : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
          (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ U)
            (PrimeSpectrum.comap σ (↑x : (↑(PrimeSpectrum.Top S) : Type u))) sorry)) :
      Localizations N (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
Tactic: rw [map_smulₛₗ, ← IsScalarTower.algebraMap_smul S]