-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
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))
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))) ⋯) +
        (↑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)))
⊢ (↑(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

Tactic:
dsimp [comapFun]

Premises used: AlgebraicGeometry.StructureSheaf.comapFun