-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf (goal)
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 := ⋯ })
⊢ ∃ (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)
have 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 := sorry })),
  ∃ (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⟩