-- 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
P : (↑(PrimeSpectrum.Top R) : Type u)
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
a b : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))
ha :
  Membership.mem (γ := Set ((x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))))
    {f : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)) |
      PrelocalPredicate.pred (T := Localizations M)
        (LocalPredicate.toPrelocalPredicate (T := Localizations M) (isLocallyFraction R M)) f}
    a
hb :
  Membership.mem (γ := Set ((x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))))
    {f : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)) |
      PrelocalPredicate.pred (T := Localizations M)
        (LocalPredicate.toPrelocalPredicate (T := Localizations M) (isLocallyFraction R M)) f}
    b
x_1 : ↥U
Va : Opens (↑(PrimeSpectrum.Top R) : Type u)
ma : (↑x_1 : (↑(PrimeSpectrum.Top R) : Type u)) ∈ Va
ia : Va ⟶ U
ra : M
sa : R
wa :
  ∀ (x : ↥Va),
    ∃ (hs : sa ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥Va) ↦
            (a ((ia : (a : ↥Va) → ↥U) x) :
              Localizations (R := R) M (↑((ia : (a : ↥Va) → ↥U) x) : (↑(PrimeSpectrum.Top R) : Type u))))
          x)
        (LocalizedModule.mk ra
          (Subtype.mk (p := fun (x_2 : R) ↦ x_2 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) sa hs))
Vb : Opens (↑(PrimeSpectrum.Top R) : Type u)
mb : (↑x_1 : (↑(PrimeSpectrum.Top R) : Type u)) ∈ Vb
ib : Vb ⟶ U
rb : M
sb : R
wb :
  ∀ (x : ↥Vb),
    ∃ (hs : sb ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥Vb) ↦
            (b ((ib : (a : ↥Vb) → ↥U) x) :
              Localizations (R := R) M (↑((ib : (a : ↥Vb) → ↥U) x) : (↑(PrimeSpectrum.Top R) : Type u))))
          x)
        (LocalizedModule.mk rb
          (Subtype.mk (p := fun (x_2 : R) ↦ x_2 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) sb hs))
x : ↥(Va ⊓ Vb)
hsax :
  sa ∉
    (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ Va) (↑x : (↑(PrimeSpectrum.Top R) : Type u))
            ⋯) :
        (↑(PrimeSpectrum.Top R) : Type u)).asIdeal
hsa :
  Eq (α :=
    Localizations M
      (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ Va) (↑x : (↑(PrimeSpectrum.Top R) : Type u))
            ⋯) :
        (↑(PrimeSpectrum.Top R) : Type u)))
    ((fun (x : ↥Va) ↦
        (a ((ia : (a : ↥Va) → ↥U) x) :
          Localizations (R := R) M (↑((ia : (a : ↥Va) → ↥U) x) : (↑(PrimeSpectrum.Top R) : Type u))))
      (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ Va) (↑x : (↑(PrimeSpectrum.Top R) : Type u))
        ⋯))
    (LocalizedModule.mk ra
      (Subtype.mk (p := fun (x_2 : R) ↦
        x_2 ∈
          (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ Va)
                    (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ⋯) :
                (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl)
        sa hsax))
⊢ sb ∉
    (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ Vb) (↑x : (↑(PrimeSpectrum.Top R) : Type u))
            ⋯) :
        (↑(PrimeSpectrum.Top R) : Type u)).asIdeal

Tactic:
obtain ⟨hsbx, hsb⟩ := wb ⟨x.1, x.2.2⟩

Premises used: Subtype.mk, And.right, Subtype.val, Subtype.property