-- 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))
⊢ (↑(Subtype.mk (p := fun (f : (x : ↥(unop (op V))) → Localizations N (↑x : (↑(PrimeSpectrum.Top S) : Type u))) ↦
            PrelocalPredicate.pred (T := Localizations N)
              (LocalPredicate.toPrelocalPredicate (T := Localizations N) (isLocallyFraction S N)) f)
            (comapFun f U V hUV
              (↑(s + t) : (x : ↥(unop (op U))) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))))
            ⋯) :
        (x : ↥(unop (op V))) → Localizations N (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
      x =
    (↑(Subtype.mk (p := fun (f : (x : ↥(unop (op V))) → Localizations N (↑x : (↑(PrimeSpectrum.Top S) : Type u))) ↦
              PrelocalPredicate.pred (T := Localizations N)
                (LocalPredicate.toPrelocalPredicate (T := Localizations N) (isLocallyFraction S N)) f)
              (comapFun f U V hUV
                (↑s : (x : ↥(unop (op U))) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))))
              ⋯ +
            Subtype.mk (p := fun (f : (x : ↥(unop (op V))) → Localizations N (↑x : (↑(PrimeSpectrum.Top S) : Type u))) ↦
              PrelocalPredicate.pred (T := Localizations N)
                (LocalPredicate.toPrelocalPredicate (T := Localizations N) (isLocallyFraction S N)) f)
              (comapFun f U V hUV
                (↑t : (x : ↥(unop (op U))) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))))
              ⋯) :
        (x : ↥(unop (op V))) → Localizations N (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
      x
have dsimp : (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) +
      (↑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)) =
  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: dsimp [comapFun]