-- 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 := ⋯ })
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)
have _ : ∀ (x : ↥(Va ⊓ Vb)),
  Eq (α := at (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
    ((fun (x : ↥(Va ⊓ Vb)) ↦ (a + b) ((Va.infLELeft Vb ≫ ia : (a : ↥(Va ⊓ Vb)) → ↥(unop U)) x)) x)
    (HomogeneousLocalization.mk
      { deg := ja + jb, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (ja + jb)) (sb * ra + sa * rb) sorry,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (ja + jb)) (sa * sb) sorry, den_mem := sorry })
Tactic: refine
    ⟨Va ⊓ Vb, ⟨ma, mb⟩, Opens.infLELeft _ _ ≫ ia, ja + jb,
      ⟨sb * ra + sa * rb,
        add_mem (add_comm jb ja ▸ mul_mem_graded sb_mem ra_mem : sb * ra ∈ 𝒜 (ja + jb))
          (mul_mem_graded sa_mem rb_mem)⟩,
      ⟨sa * sb, mul_mem_graded sa_mem sb_mem⟩, fun y ↦
        y.1.asHomogeneousIdeal.toIdeal.primeCompl.mul_mem (hwa ⟨y.1, y.2.1⟩) (hwb ⟨y.1, y.2.2⟩), ?_⟩