-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u
inst_3 : CommRing S
N : Type u
inst_4 : AddCommGroup N
inst_5 : 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 : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))
hs_1 :
  PrelocalPredicate.pred (T := Localizations M)
    (LocalPredicate.toPrelocalPredicate (T := Localizations M) (isLocallyFraction R M)) s
this_1 : Module R N := Module.compHom N σ
this_2 : Algebra R S := σ.toAlgebra
this : IsScalarTower R S N
p : (↑(PrimeSpectrum.Top S) : Type u)
hpV : p ∈ V
W : Opens (↑(PrimeSpectrum.Top R) : Type u)
m :
  (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ U) (PrimeSpectrum.comap σ p) ⋯) :
      (↑(PrimeSpectrum.Top R) : Type u)) ∈
    W
iWU : W ⟶ U
a : M
b : R
h_frac :
  ∀ (x : ↥W),
    ∃ (hs : b ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥W) ↦
            (s ((iWU : (a : ↥W) → ↥U) x) :
              Localizations (R := R) M (↑((iWU : (a : ↥W) → ↥U) x) : (↑(PrimeSpectrum.Top R) : Type u))))
          x)
        (LocalizedModule.mk a
          (Subtype.mk (p := fun (x_1 : R) ↦ x_1 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) b hs))
q : (↑(PrimeSpectrum.Top S) : Type u)
hqW :
  q ∈
    (↑{ carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ : Opens (↑(PrimeSpectrum.Top S) : Type u) } :
      Set (↑(PrimeSpectrum.Top S) : Type u))
hqV : q ∈ (↑V : Set (↑(PrimeSpectrum.Top S) : Type u))
hs :
  b ∉
    (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ W) (PrimeSpectrum.comap σ q) hqW) :
        (↑(PrimeSpectrum.Top R) : Type u)).asIdeal
H :
  Eq (α := Localizations M (PrimeSpectrum.comap σ q))
    (s (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ U) (PrimeSpectrum.comap σ q) ⋯) :
      Localizations M
        (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ U) (PrimeSpectrum.comap σ q) ⋯) :
          (↑(PrimeSpectrum.Top R) : Type u)))
    (LocalizedModule.mk a
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Ideal.primeCompl (Ideal.comap σ q.asIdeal)) x)
        b hs))
rw :
  Eq (α := Localizations N q)
    ((Localizations.comapFun f q : (a : Localizations M (PrimeSpectrum.comap σ q)) → Localizations N q)
        (LocalizedModule.mk a
          (Subtype.mk (p := fun (x : R) ↦
            Membership.mem (γ := Submonoid R) (Ideal.primeCompl (Ideal.comap σ q.asIdeal)) x) b hs)) :
      Localizations N q)
    (LocalizedModule.mk ((f : (a : M) → N) a)
        (Subtype.mk (p := fun (x : S) ↦ x ∈ q.asIdeal.primeCompl) ((σ : (a : R) → S) b) hs) :
      LocalizedModule q.asIdeal.primeCompl N)
⊢ Eq (α := Localizations N q)
    ((Localizations.comapFun f q : (a : Localizations M (PrimeSpectrum.comap σ q)) → Localizations N q)
        (s (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ U) (PrimeSpectrum.comap σ q) ⋯)) :
      Localizations N q)
    (LocalizedModule.mk ((f : (a : M) → N) a)
        (Subtype.mk (p := fun (x : S) ↦ x ∈ q.asIdeal.primeCompl) ((σ : (a : R) → S) b) hs) :
      LocalizedModule q.asIdeal.primeCompl N)

Tactic:
rw [H]