-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
U : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ
a b : (x : ↥(unop U)) → at (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))
ha :
  PrelocalPredicate.pred (X := ProjectiveSpectrum.top 𝒜) (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
    at x)
    (LocalPredicate.toPrelocalPredicate (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
        (isLocallyFraction 𝒜) :
      PrelocalPredicate (X := ProjectiveSpectrum.top 𝒜) fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
    a
hb :
  PrelocalPredicate.pred (X := ProjectiveSpectrum.top 𝒜) (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
    at x)
    (LocalPredicate.toPrelocalPredicate (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
        (isLocallyFraction 𝒜) :
      PrelocalPredicate (X := ProjectiveSpectrum.top 𝒜) fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
    b
x : ↥(unop U)
Va : Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)
ma : (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ∈ Va
ia : Va ⟶ unop U
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
hwa :
  ∀ (x : ↥Va),
    (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 ja) sa sa_mem) : A) ∉
      (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal
wa :
  ∀ (x : ↥Va),
    Eq (α := at (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
      ((fun (x : ↥Va) ↦
          (a ((ia : (a : ↥Va) → ↥(unop U)) x) :
            at (↑((ia : (a : ↥Va) → ↥(unop U)) x) : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))))
        x)
      (HomogeneousLocalization.mk
        { deg := ja, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 ja) ra ra_mem,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 ja) sa sa_mem, den_mem := ⋯ })
rcases :
  ∀ (Vb : Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) (mb : (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ∈ Vb)
    (ib : Vb ⟶ unop U) (jb : ℕ) (rb : A) (rb_mem : rb ∈ 𝒜 jb) (sb : A) (sb_mem : sb ∈ 𝒜 jb)
    (hwb :
      ∀ (x : ↥Vb),
        (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 jb) sb sb_mem) : A) ∉
          (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal)
    (wb :
      ∀ (x : ↥Vb),
        Eq (α := at (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
          ((fun (x : ↥Vb) ↦
              (b ((ib : (a : ↥Vb) → ↥(unop U)) x) :
                at (↑((ib : (a : ↥Vb) → ↥(unop U)) x) : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))))
            x)
          (HomogeneousLocalization.mk
            { deg := jb, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 jb) rb rb_mem,
              den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 jb) sb sb_mem, den_mem := ⋯ })),
    ∃ (V : Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) (_ : (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ∈ V) (i
      : V ⟶ unop U),
      PrelocalPredicate.pred (X := ProjectiveSpectrum.top 𝒜) (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
        at x)
        (isFractionPrelocal 𝒜 :
          PrelocalPredicate (X := ProjectiveSpectrum.top 𝒜) fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
        (U := V) fun (x : ↥V) ↦ (a + b) ((i : (a : ↥V) → ↥(unop U)) x)
⊢ ∃ (V : Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) (_ : (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ∈ V) (i :
    V ⟶ unop U),
    PrelocalPredicate.pred (X := ProjectiveSpectrum.top 𝒜) (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
      at x)
      (isFractionPrelocal 𝒜 :
        PrelocalPredicate (X := ProjectiveSpectrum.top 𝒜) fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
      (U := V) fun (x : ↥V) ↦ (a + b) ((i : (a : ↥V) → ↥(unop U)) x)

Tactic:
rcases hb x with ⟨Vb, mb, ib, jb, ⟨rb, rb_mem⟩, ⟨sb, sb_mem⟩, hwb, wb⟩