-- 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
s t :
  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))
⊢ (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)))
      ((↑s : (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))) ⋯) +
        (↑t : (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))) ⋯)) =
    HAdd.hAdd (α := Localizations N (↑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)))
          ((↑s : (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)))
          ((↑t : (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 : HAdd.hAdd (α := Localizations N (↑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)))
        ((↑s : (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)))
    ((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)))
        ((↑t : (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))) =
  HAdd.hAdd (α := Localizations N (↑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)))
        ((↑s : (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)))
    ((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)))
        ((↑t : (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_add]