-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (hypothesis)
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 :
  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 :
    ((σ : (a : R) → S) b : S) ∉
      (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top S) : Type u)) ↦
              x ∈
                { carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ :
                    Opens (↑(PrimeSpectrum.Top S) : Type u) } ⊓
                  V)
              q ⋯) :
          (↑(PrimeSpectrum.Top S) : Type u)).asIdeal),
    Eq (α :=
      Localizations N
        (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top S) : Type u)) ↦
              x ∈
                { carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ :
                    Opens (↑(PrimeSpectrum.Top S) : Type u) } ⊓
                  V)
              q ⋯) :
          (↑(PrimeSpectrum.Top S) : Type u)))
      ((fun
              (x :
                ↥({ carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ :
                      Opens (↑(PrimeSpectrum.Top S) : Type u) } ⊓
                    V)) ↦
            (comapFun f U V hUV s
                (({ carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ :
                          Opens (↑(PrimeSpectrum.Top S) : Type u) }.infLERight
                      V :
                    (a : ↥({ carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ } ⊓ V)) → ↥V)
                  x) :
              Localizations (R := S) N
                (↑(({ carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ :
                              Opens (↑(PrimeSpectrum.Top S) : Type u) }.infLERight
                          V :
                        (a : ↥({ carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ } ⊓ V)) → ↥V)
                      x) :
                  (↑(PrimeSpectrum.Top S) : Type u))))
          (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top S) : Type u)) ↦
            x ∈
              { carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ :
                  Opens (↑(PrimeSpectrum.Top S) : Type u) } ⊓
                V)
            q ⋯) :
        Localizations (R := S) N
          (↑(({ carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ :
                        Opens (↑(PrimeSpectrum.Top S) : Type u) }.infLERight
                    V :
                  (a : ↥({ carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ } ⊓ V)) → ↥V)
                (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top S) : Type u)) ↦
                  x ∈
                    { carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ :
                        Opens (↑(PrimeSpectrum.Top S) : Type u) } ⊓
                      V)
                  q ⋯)) :
            (↑(PrimeSpectrum.Top S) : Type u)))
      (LocalizedModule.mk ((f : (a : M) → N) a)
          (Subtype.mk (p := fun (x : S) ↦
            x ∈
              (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top S) : Type u)) ↦
                        x ∈
                          { carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ :
                              Opens (↑(PrimeSpectrum.Top S) : Type u) } ⊓
                            V)
                        q ⋯) :
                    (↑(PrimeSpectrum.Top S) : Type u)).asIdeal.primeCompl)
            ((σ : (a : R) → S) b) hs) :
        LocalizedModule
          (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top S) : Type u)) ↦
                    x ∈
                      { carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ :
                          Opens (↑(PrimeSpectrum.Top S) : Type u) } ⊓
                        V)
                    q ⋯) :
                (↑(PrimeSpectrum.Top S) : Type u)).asIdeal.primeCompl
          N)
have hs₁ : b ∉
  (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ W) (PrimeSpectrum.comap σ q) hqW) :
      (↑(PrimeSpectrum.Top R) : Type u)).asIdeal
Tactic: obtain ⟨hs, H⟩ := h_frac ⟨PrimeSpectrum.comap σ q, hqW⟩