-- 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
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
y : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)
hy : y ∈ Va ⊓ Vb
wa :
  ∀ (a_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) (b : a_1 ∈ Va),
    Eq (α := at a_1)
      (a (Subtype.mk (p := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ x ∈ unop U) a_1 ⋯) :
        at
          (↑(Subtype.mk (p := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ x ∈ unop U) a_1 ⋯) :
            (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
      (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 := ⋯ })
wb :
  ∀ (a : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) (b_1 : a ∈ Vb),
    Eq (α := at a)
      (b (Subtype.mk (p := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ x ∈ unop U) a ⋯) :
        at
          (↑(Subtype.mk (p := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ x ∈ unop U) a ⋯) :
            (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
      (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 := ⋯ })
⊢ Eq (α :=
    at
      (↑(Subtype.mk (p := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ x ∈ Va ⊓ Vb) y hy) :
        (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
    ((fun (x : ↥(Va ⊓ Vb)) ↦ (a * b) ((Va.infLELeft Vb ≫ ia : (a : ↥(Va ⊓ Vb)) → ↥(unop U)) x))
      (Subtype.mk (p := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ x ∈ Va ⊓ Vb) y hy))
    (HomogeneousLocalization.mk
      { deg := ja + jb, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (ja + jb)) (ra * rb) ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (ja + jb)) (sa * sb) ⋯, den_mem := ⋯ })

Tactic:
simp [wa y hy.1, wb y hy.2, ext_iff_val, Localization.mk_mul]

Premises used: HomogeneousLocalization.ext_iff_val, And.right, And.left, Localization.mk_mul