-- 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))
hsbx :
  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
hsb :
  Eq (α :=
    Localizations M
      (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ Vb) (↑x : (↑(PrimeSpectrum.Top R) : Type u))
            ⋯) :
        (↑(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))))
      (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ Vb) (↑x : (↑(PrimeSpectrum.Top R) : Type u))
        ⋯))
    (LocalizedModule.mk rb
      (Subtype.mk (p := fun (x_2 : R) ↦
        x_2 ∈
          (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ Vb)
                    (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ⋯) :
                (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl)
        sb hsbx))
⊢ ∃ (hs : sa * sb ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
    Eq (α := Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
      ((fun (x : ↥(Va ⊓ Vb)) ↦ (a + b) ((Va.infLELeft Vb ≫ ia : (a : ↥(Va ⊓ Vb)) → ↥U) x)) x)
      (LocalizedModule.mk (sb • ra + sa • rb)
        (Subtype.mk (p := fun (x_2 : R) ↦ x_2 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) (sa * sb)
          hs))

Tactic:
⟨x.1.asIdeal.primeCompl.mul_mem hsax hsbx,
      congr($hsa + $hsb).trans (LocalizedModule.mk_add_mk ..)⟩

Premises used: LocalizedModule.mk_add_mk, Submonoid.mul_mem, congrArg, id, HAdd.hAdd, congr, Exists.intro, Ideal.primeCompl, Subtype.val, PrimeSpectrum.asIdeal, Eq.trans