[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
⊢ ∀ {U V : Opens ↑(ProjectiveSpectrum.top 𝒜)} (i : U ⟶ V) (f : (x : { x // x ∈ V }) → at ↑x),
    (fun {U} f => IsFraction f) f →
      (fun {U} f => IsFraction f) fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)
[PROOFSTEP]
rintro V U i f ⟨j, r, s, w⟩
[GOAL]
case intro.intro.intro
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
V U : Opens ↑(ProjectiveSpectrum.top 𝒜)
i : V ⟶ U
f : (x : { x // x ∈ U }) → at ↑x
j : ℕ
r s : { x // x ∈ 𝒜 j }
w : ∀ (x : { x // x ∈ U }), ∃ s_nin, f x = Quotient.mk'' { deg := j, num := r, den := s, den_mem := s_nin }
⊢ IsFraction fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)
[PROOFSTEP]
exact ⟨j, r, s, fun y => w (i y)⟩
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : { x // x ∈ U.unop }) → at ↑x
ha : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate a
hb : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate b
x : { x // x ∈ U.unop }
⊢ ∃ V x i,
    PrelocalPredicate.pred (isFractionPrelocal 𝒜) fun x =>
      (a + b) ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)
[PROOFSTEP]
rcases ha x with ⟨Va, ma, ia, ja, ⟨ra, ra_mem⟩, ⟨sa, sa_mem⟩, wa⟩
[GOAL]
case intro.intro.intro.intro.intro.mk.intro.mk
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : { x // x ∈ U.unop }) → at ↑x
ha : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate a
hb : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate b
x : { x // x ∈ U.unop }
Va : Opens ↑(ProjectiveSpectrum.top 𝒜)
ma : ↑x ∈ Va
ia : Va ⟶ U.unop
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
wa :
  ∀ (x : { x // x ∈ Va }),
    ∃ s_nin,
      (fun x => a ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem },
            den_mem := s_nin }
⊢ ∃ V x i,
    PrelocalPredicate.pred (isFractionPrelocal 𝒜) fun x =>
      (a + b) ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)
[PROOFSTEP]
rcases hb x with ⟨Vb, mb, ib, jb, ⟨rb, rb_mem⟩, ⟨sb, sb_mem⟩, wb⟩
[GOAL]
case intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : { x // x ∈ U.unop }) → at ↑x
ha : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate a
hb : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate b
x : { x // x ∈ U.unop }
Va : Opens ↑(ProjectiveSpectrum.top 𝒜)
ma : ↑x ∈ Va
ia : Va ⟶ U.unop
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
wa :
  ∀ (x : { x // x ∈ Va }),
    ∃ s_nin,
      (fun x => a ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem },
            den_mem := s_nin }
Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)
mb : ↑x ∈ Vb
ib : Vb ⟶ U.unop
jb : ℕ
rb : A
rb_mem : rb ∈ 𝒜 jb
sb : A
sb_mem : sb ∈ 𝒜 jb
wb :
  ∀ (x : { x // x ∈ Vb }),
    ∃ s_nin,
      (fun x => b ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := jb, num := { val := rb, property := rb_mem }, den := { val := sb, property := sb_mem },
            den_mem := s_nin }
⊢ ∃ V x i,
    PrelocalPredicate.pred (isFractionPrelocal 𝒜) fun x =>
      (a + b) ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)
[PROOFSTEP]
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 => ⟨fun h => _, _⟩⟩
[GOAL]
case intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.refine'_1
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : { x // x ∈ U.unop }) → at ↑x
ha : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate a
hb : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate b
x : { x // x ∈ U.unop }
Va : Opens ↑(ProjectiveSpectrum.top 𝒜)
ma : ↑x ∈ Va
ia : Va ⟶ U.unop
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
wa :
  ∀ (x : { x // x ∈ Va }),
    ∃ s_nin,
      (fun x => a ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem },
            den_mem := s_nin }
Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)
mb : ↑x ∈ Vb
ib : Vb ⟶ U.unop
jb : ℕ
rb : A
rb_mem : rb ∈ 𝒜 jb
sb : A
sb_mem : sb ∈ 𝒜 jb
wb :
  ∀ (x : { x // x ∈ Vb }),
    ∃ s_nin,
      (fun x => b ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := jb, num := { val := rb, property := rb_mem }, den := { val := sb, property := sb_mem },
            den_mem := s_nin }
y : { x // x ∈ Va ⊓ Vb }
h : ↑{ val := sa * sb, property := (_ : sa * sb ∈ 𝒜 (ja + jb)) } ∈ (↑y).asHomogeneousIdeal
⊢ False
[PROOFSTEP]
cases' (y : ProjectiveSpectrum.top 𝒜).isPrime.mem_or_mem h with h h
[GOAL]
case intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.refine'_1.inl
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : { x // x ∈ U.unop }) → at ↑x
ha : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate a
hb : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate b
x : { x // x ∈ U.unop }
Va : Opens ↑(ProjectiveSpectrum.top 𝒜)
ma : ↑x ∈ Va
ia : Va ⟶ U.unop
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
wa :
  ∀ (x : { x // x ∈ Va }),
    ∃ s_nin,
      (fun x => a ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem },
            den_mem := s_nin }
Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)
mb : ↑x ∈ Vb
ib : Vb ⟶ U.unop
jb : ℕ
rb : A
rb_mem : rb ∈ 𝒜 jb
sb : A
sb_mem : sb ∈ 𝒜 jb
wb :
  ∀ (x : { x // x ∈ Vb }),
    ∃ s_nin,
      (fun x => b ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := jb, num := { val := rb, property := rb_mem }, den := { val := sb, property := sb_mem },
            den_mem := s_nin }
y : { x // x ∈ Va ⊓ Vb }
h✝ : ↑{ val := sa * sb, property := (_ : sa * sb ∈ 𝒜 (ja + jb)) } ∈ (↑y).asHomogeneousIdeal
h : sa ∈ HomogeneousIdeal.toIdeal (↑y).asHomogeneousIdeal
⊢ False
[PROOFSTEP]
obtain ⟨nin, -⟩ := wa ⟨y, (Opens.infLELeft Va Vb y).2⟩
[GOAL]
case intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.refine'_1.inl.intro
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : { x // x ∈ U.unop }) → at ↑x
ha : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate a
hb : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate b
x : { x // x ∈ U.unop }
Va : Opens ↑(ProjectiveSpectrum.top 𝒜)
ma : ↑x ∈ Va
ia : Va ⟶ U.unop
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
wa :
  ∀ (x : { x // x ∈ Va }),
    ∃ s_nin,
      (fun x => a ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem },
            den_mem := s_nin }
Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)
mb : ↑x ∈ Vb
ib : Vb ⟶ U.unop
jb : ℕ
rb : A
rb_mem : rb ∈ 𝒜 jb
sb : A
sb_mem : sb ∈ 𝒜 jb
wb :
  ∀ (x : { x // x ∈ Vb }),
    ∃ s_nin,
      (fun x => b ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := jb, num := { val := rb, property := rb_mem }, den := { val := sb, property := sb_mem },
            den_mem := s_nin }
y : { x // x ∈ Va ⊓ Vb }
h✝ : ↑{ val := sa * sb, property := (_ : sa * sb ∈ 𝒜 (ja + jb)) } ∈ (↑y).asHomogeneousIdeal
h : sa ∈ HomogeneousIdeal.toIdeal (↑y).asHomogeneousIdeal
nin :
  ¬↑{ val := sa, property := sa_mem } ∈
      (↑{ val := ↑y,
            property := (_ : ↑((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑Va) }) y) ∈ Va) }).asHomogeneousIdeal
⊢ False
[PROOFSTEP]
exact nin h
[GOAL]
case intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.refine'_1.inr
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : { x // x ∈ U.unop }) → at ↑x
ha : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate a
hb : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate b
x : { x // x ∈ U.unop }
Va : Opens ↑(ProjectiveSpectrum.top 𝒜)
ma : ↑x ∈ Va
ia : Va ⟶ U.unop
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
wa :
  ∀ (x : { x // x ∈ Va }),
    ∃ s_nin,
      (fun x => a ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem },
            den_mem := s_nin }
Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)
mb : ↑x ∈ Vb
ib : Vb ⟶ U.unop
jb : ℕ
rb : A
rb_mem : rb ∈ 𝒜 jb
sb : A
sb_mem : sb ∈ 𝒜 jb
wb :
  ∀ (x : { x // x ∈ Vb }),
    ∃ s_nin,
      (fun x => b ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := jb, num := { val := rb, property := rb_mem }, den := { val := sb, property := sb_mem },
            den_mem := s_nin }
y : { x // x ∈ Va ⊓ Vb }
h✝ : ↑{ val := sa * sb, property := (_ : sa * sb ∈ 𝒜 (ja + jb)) } ∈ (↑y).asHomogeneousIdeal
h : sb ∈ HomogeneousIdeal.toIdeal (↑y).asHomogeneousIdeal
⊢ False
[PROOFSTEP]
obtain ⟨nin, -⟩ := wb ⟨y, (Opens.infLERight Va Vb y).2⟩
[GOAL]
case intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.refine'_1.inr.intro
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : { x // x ∈ U.unop }) → at ↑x
ha : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate a
hb : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate b
x : { x // x ∈ U.unop }
Va : Opens ↑(ProjectiveSpectrum.top 𝒜)
ma : ↑x ∈ Va
ia : Va ⟶ U.unop
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
wa :
  ∀ (x : { x // x ∈ Va }),
    ∃ s_nin,
      (fun x => a ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem },
            den_mem := s_nin }
Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)
mb : ↑x ∈ Vb
ib : Vb ⟶ U.unop
jb : ℕ
rb : A
rb_mem : rb ∈ 𝒜 jb
sb : A
sb_mem : sb ∈ 𝒜 jb
wb :
  ∀ (x : { x // x ∈ Vb }),
    ∃ s_nin,
      (fun x => b ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := jb, num := { val := rb, property := rb_mem }, den := { val := sb, property := sb_mem },
            den_mem := s_nin }
y : { x // x ∈ Va ⊓ Vb }
h✝ : ↑{ val := sa * sb, property := (_ : sa * sb ∈ 𝒜 (ja + jb)) } ∈ (↑y).asHomogeneousIdeal
h : sb ∈ HomogeneousIdeal.toIdeal (↑y).asHomogeneousIdeal
nin :
  ¬↑{ val := sb, property := sb_mem } ∈
      (↑{ val := ↑y,
            property := (_ : ↑((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑Vb) }) y) ∈ Vb) }).asHomogeneousIdeal
⊢ False
[PROOFSTEP]
exact nin h
[GOAL]
case intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.refine'_2
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : { x // x ∈ U.unop }) → at ↑x
ha : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate a
hb : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate b
x : { x // x ∈ U.unop }
Va : Opens ↑(ProjectiveSpectrum.top 𝒜)
ma : ↑x ∈ Va
ia : Va ⟶ U.unop
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
wa :
  ∀ (x : { x // x ∈ Va }),
    ∃ s_nin,
      (fun x => a ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem },
            den_mem := s_nin }
Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)
mb : ↑x ∈ Vb
ib : Vb ⟶ U.unop
jb : ℕ
rb : A
rb_mem : rb ∈ 𝒜 jb
sb : A
sb_mem : sb ∈ 𝒜 jb
wb :
  ∀ (x : { x // x ∈ Vb }),
    ∃ s_nin,
      (fun x => b ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := jb, num := { val := rb, property := rb_mem }, den := { val := sb, property := sb_mem },
            den_mem := s_nin }
y : { x // x ∈ Va ⊓ Vb }
⊢ (fun x => (a + b) ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) y =
    Quotient.mk''
      { deg := ja + jb, num := { val := sb * ra + sa * rb, property := (_ : sb * ra + sa * rb ∈ 𝒜 (ja + jb)) },
        den := { val := sa * sb, property := (_ : sa * sb ∈ 𝒜 (ja + jb)) },
        den_mem :=
          (_ : ↑{ val := sa * sb, property := (_ : sa * sb ∈ 𝒜 (ja + jb)) } ∈ (↑y).asHomogeneousIdeal → False) }
[PROOFSTEP]
simp only [add_mul, map_add, Pi.add_apply, RingHom.map_mul, ext_iff_val, add_val]
[GOAL]
case intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.refine'_2
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : { x // x ∈ U.unop }) → at ↑x
ha : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate a
hb : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate b
x : { x // x ∈ U.unop }
Va : Opens ↑(ProjectiveSpectrum.top 𝒜)
ma : ↑x ∈ Va
ia : Va ⟶ U.unop
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
wa :
  ∀ (x : { x // x ∈ Va }),
    ∃ s_nin,
      (fun x => a ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem },
            den_mem := s_nin }
Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)
mb : ↑x ∈ Vb
ib : Vb ⟶ U.unop
jb : ℕ
rb : A
rb_mem : rb ∈ 𝒜 jb
sb : A
sb_mem : sb ∈ 𝒜 jb
wb :
  ∀ (x : { x // x ∈ Vb }),
    ∃ s_nin,
      (fun x => b ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := jb, num := { val := rb, property := rb_mem }, den := { val := sb, property := sb_mem },
            den_mem := s_nin }
y : { x // x ∈ Va ⊓ Vb }
⊢ val (a { val := ↑y, property := (_ : ↑y ∈ ↑U.unop) }) + val (b { val := ↑y, property := (_ : ↑y ∈ ↑U.unop) }) =
    val
      (Quotient.mk''
        { deg := ja + jb, num := { val := sb * ra + sa * rb, property := (_ : sb * ra + sa * rb ∈ 𝒜 (ja + jb)) },
          den := { val := sa * sb, property := (_ : sa * sb ∈ 𝒜 (ja + jb)) },
          den_mem :=
            (_ : ↑{ val := sa * sb, property := (_ : sa * sb ∈ 𝒜 (ja + jb)) } ∈ (↑y).asHomogeneousIdeal → False) })
[PROOFSTEP]
obtain ⟨nin1, hy1⟩ := wa (Opens.infLELeft Va Vb y)
[GOAL]
case intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.refine'_2.intro
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : { x // x ∈ U.unop }) → at ↑x
ha : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate a
hb : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate b
x : { x // x ∈ U.unop }
Va : Opens ↑(ProjectiveSpectrum.top 𝒜)
ma : ↑x ∈ Va
ia : Va ⟶ U.unop
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
wa :
  ∀ (x : { x // x ∈ Va }),
    ∃ s_nin,
      (fun x => a ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem },
            den_mem := s_nin }
Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)
mb : ↑x ∈ Vb
ib : Vb ⟶ U.unop
jb : ℕ
rb : A
rb_mem : rb ∈ 𝒜 jb
sb : A
sb_mem : sb ∈ 𝒜 jb
wb :
  ∀ (x : { x // x ∈ Vb }),
    ∃ s_nin,
      (fun x => b ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := jb, num := { val := rb, property := rb_mem }, den := { val := sb, property := sb_mem },
            den_mem := s_nin }
y : { x // x ∈ Va ⊓ Vb }
nin1 :
  ¬↑{ val := sa, property := sa_mem } ∈ (↑((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑Va) }) y)).asHomogeneousIdeal
hy1 :
  (fun x => a ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x))
      ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑Va) }) y) =
    Quotient.mk''
      { deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem }, den_mem := nin1 }
⊢ val (a { val := ↑y, property := (_ : ↑y ∈ ↑U.unop) }) + val (b { val := ↑y, property := (_ : ↑y ∈ ↑U.unop) }) =
    val
      (Quotient.mk''
        { deg := ja + jb, num := { val := sb * ra + sa * rb, property := (_ : sb * ra + sa * rb ∈ 𝒜 (ja + jb)) },
          den := { val := sa * sb, property := (_ : sa * sb ∈ 𝒜 (ja + jb)) },
          den_mem :=
            (_ : ↑{ val := sa * sb, property := (_ : sa * sb ∈ 𝒜 (ja + jb)) } ∈ (↑y).asHomogeneousIdeal → False) })
[PROOFSTEP]
obtain ⟨nin2, hy2⟩ := wb (Opens.infLERight Va Vb y)
[GOAL]
case intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.refine'_2.intro.intro
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : { x // x ∈ U.unop }) → at ↑x
ha : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate a
hb : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate b
x : { x // x ∈ U.unop }
Va : Opens ↑(ProjectiveSpectrum.top 𝒜)
ma : ↑x ∈ Va
ia : Va ⟶ U.unop
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
wa :
  ∀ (x : { x // x ∈ Va }),
    ∃ s_nin,
      (fun x => a ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem },
            den_mem := s_nin }
Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)
mb : ↑x ∈ Vb
ib : Vb ⟶ U.unop
jb : ℕ
rb : A
rb_mem : rb ∈ 𝒜 jb
sb : A
sb_mem : sb ∈ 𝒜 jb
wb :
  ∀ (x : { x // x ∈ Vb }),
    ∃ s_nin,
      (fun x => b ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := jb, num := { val := rb, property := rb_mem }, den := { val := sb, property := sb_mem },
            den_mem := s_nin }
y : { x // x ∈ Va ⊓ Vb }
nin1 :
  ¬↑{ val := sa, property := sa_mem } ∈ (↑((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑Va) }) y)).asHomogeneousIdeal
hy1 :
  (fun x => a ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x))
      ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑Va) }) y) =
    Quotient.mk''
      { deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem }, den_mem := nin1 }
nin2 :
  ¬↑{ val := sb, property := sb_mem } ∈ (↑((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑Vb) }) y)).asHomogeneousIdeal
hy2 :
  (fun x => b ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x))
      ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑Vb) }) y) =
    Quotient.mk''
      { deg := jb, num := { val := rb, property := rb_mem }, den := { val := sb, property := sb_mem }, den_mem := nin2 }
⊢ val (a { val := ↑y, property := (_ : ↑y ∈ ↑U.unop) }) + val (b { val := ↑y, property := (_ : ↑y ∈ ↑U.unop) }) =
    val
      (Quotient.mk''
        { deg := ja + jb, num := { val := sb * ra + sa * rb, property := (_ : sb * ra + sa * rb ∈ 𝒜 (ja + jb)) },
          den := { val := sa * sb, property := (_ : sa * sb ∈ 𝒜 (ja + jb)) },
          den_mem :=
            (_ : ↑{ val := sa * sb, property := (_ : sa * sb ∈ 𝒜 (ja + jb)) } ∈ (↑y).asHomogeneousIdeal → False) })
[PROOFSTEP]
dsimp only at hy1 hy2
[GOAL]
case intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.refine'_2.intro.intro
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : { x // x ∈ U.unop }) → at ↑x
ha : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate a
hb : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate b
x : { x // x ∈ U.unop }
Va : Opens ↑(ProjectiveSpectrum.top 𝒜)
ma : ↑x ∈ Va
ia : Va ⟶ U.unop
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
wa :
  ∀ (x : { x // x ∈ Va }),
    ∃ s_nin,
      (fun x => a ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem },
            den_mem := s_nin }
Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)
mb : ↑x ∈ Vb
ib : Vb ⟶ U.unop
jb : ℕ
rb : A
rb_mem : rb ∈ 𝒜 jb
sb : A
sb_mem : sb ∈ 𝒜 jb
wb :
  ∀ (x : { x // x ∈ Vb }),
    ∃ s_nin,
      (fun x => b ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := jb, num := { val := rb, property := rb_mem }, den := { val := sb, property := sb_mem },
            den_mem := s_nin }
y : { x // x ∈ Va ⊓ Vb }
nin1 :
  ¬↑{ val := sa, property := sa_mem } ∈ (↑((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑Va) }) y)).asHomogeneousIdeal
hy1 :
  a { val := ↑y, property := (_ : ↑{ val := ↑y, property := (_ : ↑y ∈ ↑Va) } ∈ ↑U.unop) } =
    Quotient.mk''
      { deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem }, den_mem := nin1 }
nin2 :
  ¬↑{ val := sb, property := sb_mem } ∈ (↑((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑Vb) }) y)).asHomogeneousIdeal
hy2 :
  b { val := ↑y, property := (_ : ↑{ val := ↑y, property := (_ : ↑y ∈ ↑Vb) } ∈ ↑U.unop) } =
    Quotient.mk''
      { deg := jb, num := { val := rb, property := rb_mem }, den := { val := sb, property := sb_mem }, den_mem := nin2 }
⊢ val (a { val := ↑y, property := (_ : ↑y ∈ ↑U.unop) }) + val (b { val := ↑y, property := (_ : ↑y ∈ ↑U.unop) }) =
    val
      (Quotient.mk''
        { deg := ja + jb, num := { val := sb * ra + sa * rb, property := (_ : sb * ra + sa * rb ∈ 𝒜 (ja + jb)) },
          den := { val := sa * sb, property := (_ : sa * sb ∈ 𝒜 (ja + jb)) },
          den_mem :=
            (_ : ↑{ val := sa * sb, property := (_ : sa * sb ∈ 𝒜 (ja + jb)) } ∈ (↑y).asHomogeneousIdeal → False) })
[PROOFSTEP]
erw [hy1, hy2]
[GOAL]
case intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.refine'_2.intro.intro
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : { x // x ∈ U.unop }) → at ↑x
ha : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate a
hb : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate b
x : { x // x ∈ U.unop }
Va : Opens ↑(ProjectiveSpectrum.top 𝒜)
ma : ↑x ∈ Va
ia : Va ⟶ U.unop
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
wa :
  ∀ (x : { x // x ∈ Va }),
    ∃ s_nin,
      (fun x => a ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem },
            den_mem := s_nin }
Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)
mb : ↑x ∈ Vb
ib : Vb ⟶ U.unop
jb : ℕ
rb : A
rb_mem : rb ∈ 𝒜 jb
sb : A
sb_mem : sb ∈ 𝒜 jb
wb :
  ∀ (x : { x // x ∈ Vb }),
    ∃ s_nin,
      (fun x => b ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := jb, num := { val := rb, property := rb_mem }, den := { val := sb, property := sb_mem },
            den_mem := s_nin }
y : { x // x ∈ Va ⊓ Vb }
nin1 :
  ¬↑{ val := sa, property := sa_mem } ∈ (↑((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑Va) }) y)).asHomogeneousIdeal
hy1 :
  a { val := ↑y, property := (_ : ↑{ val := ↑y, property := (_ : ↑y ∈ ↑Va) } ∈ ↑U.unop) } =
    Quotient.mk''
      { deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem }, den_mem := nin1 }
nin2 :
  ¬↑{ val := sb, property := sb_mem } ∈ (↑((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑Vb) }) y)).asHomogeneousIdeal
hy2 :
  b { val := ↑y, property := (_ : ↑{ val := ↑y, property := (_ : ↑y ∈ ↑Vb) } ∈ ↑U.unop) } =
    Quotient.mk''
      { deg := jb, num := { val := rb, property := rb_mem }, den := { val := sb, property := sb_mem }, den_mem := nin2 }
⊢ val
        (Quotient.mk''
          { deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem },
            den_mem := nin1 }) +
      val
        (Quotient.mk''
          { deg := jb, num := { val := rb, property := rb_mem }, den := { val := sb, property := sb_mem },
            den_mem := nin2 }) =
    val
      (Quotient.mk''
        { deg := ja + jb, num := { val := sb * ra + sa * rb, property := (_ : sb * ra + sa * rb ∈ 𝒜 (ja + jb)) },
          den := { val := sa * sb, property := (_ : sa * sb ∈ 𝒜 (ja + jb)) },
          den_mem :=
            (_ : ↑{ val := sa * sb, property := (_ : sa * sb ∈ 𝒜 (ja + jb)) } ∈ (↑y).asHomogeneousIdeal → False) })
[PROOFSTEP]
simp only [val_mk'', add_mk, add_comm (sa * rb)]
[GOAL]
case intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.refine'_2.intro.intro
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : { x // x ∈ U.unop }) → at ↑x
ha : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate a
hb : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate b
x : { x // x ∈ U.unop }
Va : Opens ↑(ProjectiveSpectrum.top 𝒜)
ma : ↑x ∈ Va
ia : Va ⟶ U.unop
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
wa :
  ∀ (x : { x // x ∈ Va }),
    ∃ s_nin,
      (fun x => a ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem },
            den_mem := s_nin }
Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)
mb : ↑x ∈ Vb
ib : Vb ⟶ U.unop
jb : ℕ
rb : A
rb_mem : rb ∈ 𝒜 jb
sb : A
sb_mem : sb ∈ 𝒜 jb
wb :
  ∀ (x : { x // x ∈ Vb }),
    ∃ s_nin,
      (fun x => b ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := jb, num := { val := rb, property := rb_mem }, den := { val := sb, property := sb_mem },
            den_mem := s_nin }
y : { x // x ∈ Va ⊓ Vb }
nin1 :
  ¬↑{ val := sa, property := sa_mem } ∈ (↑((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑Va) }) y)).asHomogeneousIdeal
hy1 :
  a { val := ↑y, property := (_ : ↑{ val := ↑y, property := (_ : ↑y ∈ ↑Va) } ∈ ↑U.unop) } =
    Quotient.mk''
      { deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem }, den_mem := nin1 }
nin2 :
  ¬↑{ val := sb, property := sb_mem } ∈ (↑((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑Vb) }) y)).asHomogeneousIdeal
hy2 :
  b { val := ↑y, property := (_ : ↑{ val := ↑y, property := (_ : ↑y ∈ ↑Vb) } ∈ ↑U.unop) } =
    Quotient.mk''
      { deg := jb, num := { val := rb, property := rb_mem }, den := { val := sb, property := sb_mem }, den_mem := nin2 }
⊢ Localization.mk (sb * ra + sa * rb)
      ({ val := sa,
          property :=
            (_ :
              ↑{ deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem },
                      den_mem := nin1 }.den ∈
                Ideal.primeCompl (HomogeneousIdeal.toIdeal (↑y).asHomogeneousIdeal)) } *
        { val := sb,
          property :=
            (_ :
              ↑{ deg := jb, num := { val := rb, property := rb_mem }, den := { val := sb, property := sb_mem },
                      den_mem := nin2 }.den ∈
                Ideal.primeCompl (HomogeneousIdeal.toIdeal (↑y).asHomogeneousIdeal)) }) =
    Localization.mk (sb * ra + sa * rb)
      { val := sa * sb,
        property :=
          (_ :
            ↑{ deg := ja + jb, num := { val := sb * ra + sa * rb, property := (_ : sb * ra + sa * rb ∈ 𝒜 (ja + jb)) },
                    den := { val := sa * sb, property := (_ : sa * sb ∈ 𝒜 (ja + jb)) },
                    den_mem :=
                      (_ :
                        ↑{ val := sa * sb, property := (_ : sa * sb ∈ 𝒜 (ja + jb)) } ∈ (↑y).asHomogeneousIdeal →
                          False) }.den ∈
              Ideal.primeCompl (HomogeneousIdeal.toIdeal (↑y).asHomogeneousIdeal)) }
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a : (x : { x // x ∈ U.unop }) → at ↑x
ha : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate a
x : { x // x ∈ U.unop }
⊢ ∃ V x i,
    PrelocalPredicate.pred (isFractionPrelocal 𝒜) fun x =>
      (-a) ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)
[PROOFSTEP]
rcases ha x with ⟨V, m, i, j, ⟨r, r_mem⟩, ⟨s, s_mem⟩, w⟩
[GOAL]
case intro.intro.intro.intro.intro.mk.intro.mk
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a : (x : { x // x ∈ U.unop }) → at ↑x
ha : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate a
x : { x // x ∈ U.unop }
V : Opens ↑(ProjectiveSpectrum.top 𝒜)
m : ↑x ∈ V
i : V ⟶ U.unop
j : ℕ
r : A
r_mem : r ∈ 𝒜 j
s : A
s_mem : s ∈ 𝒜 j
w :
  ∀ (x : { x // x ∈ V }),
    ∃ s_nin,
      (fun x => a ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := j, num := { val := r, property := r_mem }, den := { val := s, property := s_mem }, den_mem := s_nin }
⊢ ∃ V x i,
    PrelocalPredicate.pred (isFractionPrelocal 𝒜) fun x =>
      (-a) ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)
[PROOFSTEP]
choose nin hy using w
[GOAL]
case intro.intro.intro.intro.intro.mk.intro.mk
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a : (x : { x // x ∈ U.unop }) → at ↑x
ha : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate a
x : { x // x ∈ U.unop }
V : Opens ↑(ProjectiveSpectrum.top 𝒜)
m : ↑x ∈ V
i : V ⟶ U.unop
j : ℕ
r : A
r_mem : r ∈ 𝒜 j
s : A
s_mem : s ∈ 𝒜 j
nin : ∀ (x : { x // x ∈ V }), ¬↑{ val := s, property := s_mem } ∈ (↑x).asHomogeneousIdeal
hy :
  ∀ (x : { x // x ∈ V }),
    (fun x => a ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
      Quotient.mk''
        { deg := j, num := { val := r, property := r_mem }, den := { val := s, property := s_mem },
          den_mem := (_ : ¬↑{ val := s, property := s_mem } ∈ (↑x).asHomogeneousIdeal) }
⊢ ∃ V x i,
    PrelocalPredicate.pred (isFractionPrelocal 𝒜) fun x =>
      (-a) ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)
[PROOFSTEP]
refine' ⟨V, m, i, j, ⟨-r, Submodule.neg_mem _ r_mem⟩, ⟨s, s_mem⟩, fun y => ⟨nin y, _⟩⟩
[GOAL]
case intro.intro.intro.intro.intro.mk.intro.mk
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a : (x : { x // x ∈ U.unop }) → at ↑x
ha : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate a
x : { x // x ∈ U.unop }
V : Opens ↑(ProjectiveSpectrum.top 𝒜)
m : ↑x ∈ V
i : V ⟶ U.unop
j : ℕ
r : A
r_mem : r ∈ 𝒜 j
s : A
s_mem : s ∈ 𝒜 j
nin : ∀ (x : { x // x ∈ V }), ¬↑{ val := s, property := s_mem } ∈ (↑x).asHomogeneousIdeal
hy :
  ∀ (x : { x // x ∈ V }),
    (fun x => a ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
      Quotient.mk''
        { deg := j, num := { val := r, property := r_mem }, den := { val := s, property := s_mem },
          den_mem := (_ : ¬↑{ val := s, property := s_mem } ∈ (↑x).asHomogeneousIdeal) }
y : { x // x ∈ V }
⊢ (fun x => (-a) ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) y =
    Quotient.mk''
      { deg := j, num := { val := -r, property := (_ : -r ∈ 𝒜 j) }, den := { val := s, property := s_mem },
        den_mem := (_ : ¬↑{ val := s, property := s_mem } ∈ (↑y).asHomogeneousIdeal) }
[PROOFSTEP]
simp only [ext_iff_val, val_mk''] at hy
[GOAL]
case intro.intro.intro.intro.intro.mk.intro.mk
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a : (x : { x // x ∈ U.unop }) → at ↑x
ha : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate a
x : { x // x ∈ U.unop }
V : Opens ↑(ProjectiveSpectrum.top 𝒜)
m : ↑x ∈ V
i : V ⟶ U.unop
j : ℕ
r : A
r_mem : r ∈ 𝒜 j
s : A
s_mem : s ∈ 𝒜 j
nin : ∀ (x : { x // x ∈ V }), ¬↑{ val := s, property := s_mem } ∈ (↑x).asHomogeneousIdeal
y : { x // x ∈ V }
hy :
  ∀ (x : { x // x ∈ V }),
    val (a { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) =
      Localization.mk r
        { val := s,
          property :=
            (_ :
              ↑{ deg := j, num := { val := r, property := r_mem }, den := { val := s, property := s_mem },
                      den_mem := (_ : ¬↑{ val := s, property := s_mem } ∈ (↑x).asHomogeneousIdeal) }.den ∈
                Ideal.primeCompl (HomogeneousIdeal.toIdeal (↑x).asHomogeneousIdeal)) }
⊢ (fun x => (-a) ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) y =
    Quotient.mk''
      { deg := j, num := { val := -r, property := (_ : -r ∈ 𝒜 j) }, den := { val := s, property := s_mem },
        den_mem := (_ : ¬↑{ val := s, property := s_mem } ∈ (↑y).asHomogeneousIdeal) }
[PROOFSTEP]
simp only [Pi.neg_apply, ext_iff_val, neg_val, hy, val_mk'', neg_mk]
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : { x // x ∈ U.unop }) → at ↑x
ha : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate a
hb : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate b
x : { x // x ∈ U.unop }
⊢ ∃ V x i,
    PrelocalPredicate.pred (isFractionPrelocal 𝒜) fun x =>
      (a * b) ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)
[PROOFSTEP]
rcases ha x with ⟨Va, ma, ia, ja, ⟨ra, ra_mem⟩, ⟨sa, sa_mem⟩, wa⟩
[GOAL]
case intro.intro.intro.intro.intro.mk.intro.mk
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : { x // x ∈ U.unop }) → at ↑x
ha : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate a
hb : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate b
x : { x // x ∈ U.unop }
Va : Opens ↑(ProjectiveSpectrum.top 𝒜)
ma : ↑x ∈ Va
ia : Va ⟶ U.unop
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
wa :
  ∀ (x : { x // x ∈ Va }),
    ∃ s_nin,
      (fun x => a ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem },
            den_mem := s_nin }
⊢ ∃ V x i,
    PrelocalPredicate.pred (isFractionPrelocal 𝒜) fun x =>
      (a * b) ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)
[PROOFSTEP]
rcases hb x with ⟨Vb, mb, ib, jb, ⟨rb, rb_mem⟩, ⟨sb, sb_mem⟩, wb⟩
[GOAL]
case intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : { x // x ∈ U.unop }) → at ↑x
ha : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate a
hb : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate b
x : { x // x ∈ U.unop }
Va : Opens ↑(ProjectiveSpectrum.top 𝒜)
ma : ↑x ∈ Va
ia : Va ⟶ U.unop
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
wa :
  ∀ (x : { x // x ∈ Va }),
    ∃ s_nin,
      (fun x => a ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem },
            den_mem := s_nin }
Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)
mb : ↑x ∈ Vb
ib : Vb ⟶ U.unop
jb : ℕ
rb : A
rb_mem : rb ∈ 𝒜 jb
sb : A
sb_mem : sb ∈ 𝒜 jb
wb :
  ∀ (x : { x // x ∈ Vb }),
    ∃ s_nin,
      (fun x => b ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := jb, num := { val := rb, property := rb_mem }, den := { val := sb, property := sb_mem },
            den_mem := s_nin }
⊢ ∃ V x i,
    PrelocalPredicate.pred (isFractionPrelocal 𝒜) fun x =>
      (a * b) ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)
[PROOFSTEP]
refine'
  ⟨Va ⊓ Vb, ⟨ma, mb⟩, Opens.infLELeft _ _ ≫ ia, ja + jb, ⟨ra * rb, SetLike.mul_mem_graded ra_mem rb_mem⟩,
    ⟨sa * sb, SetLike.mul_mem_graded sa_mem sb_mem⟩, fun y => ⟨fun h => _, _⟩⟩
[GOAL]
case intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.refine'_1
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : { x // x ∈ U.unop }) → at ↑x
ha : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate a
hb : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate b
x : { x // x ∈ U.unop }
Va : Opens ↑(ProjectiveSpectrum.top 𝒜)
ma : ↑x ∈ Va
ia : Va ⟶ U.unop
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
wa :
  ∀ (x : { x // x ∈ Va }),
    ∃ s_nin,
      (fun x => a ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem },
            den_mem := s_nin }
Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)
mb : ↑x ∈ Vb
ib : Vb ⟶ U.unop
jb : ℕ
rb : A
rb_mem : rb ∈ 𝒜 jb
sb : A
sb_mem : sb ∈ 𝒜 jb
wb :
  ∀ (x : { x // x ∈ Vb }),
    ∃ s_nin,
      (fun x => b ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := jb, num := { val := rb, property := rb_mem }, den := { val := sb, property := sb_mem },
            den_mem := s_nin }
y : { x // x ∈ Va ⊓ Vb }
h : ↑{ val := sa * sb, property := (_ : sa * sb ∈ 𝒜 (ja + jb)) } ∈ (↑y).asHomogeneousIdeal
⊢ False
[PROOFSTEP]
cases' (y : ProjectiveSpectrum.top 𝒜).isPrime.mem_or_mem h with h h
[GOAL]
case intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.refine'_1.inl
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : { x // x ∈ U.unop }) → at ↑x
ha : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate a
hb : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate b
x : { x // x ∈ U.unop }
Va : Opens ↑(ProjectiveSpectrum.top 𝒜)
ma : ↑x ∈ Va
ia : Va ⟶ U.unop
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
wa :
  ∀ (x : { x // x ∈ Va }),
    ∃ s_nin,
      (fun x => a ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem },
            den_mem := s_nin }
Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)
mb : ↑x ∈ Vb
ib : Vb ⟶ U.unop
jb : ℕ
rb : A
rb_mem : rb ∈ 𝒜 jb
sb : A
sb_mem : sb ∈ 𝒜 jb
wb :
  ∀ (x : { x // x ∈ Vb }),
    ∃ s_nin,
      (fun x => b ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := jb, num := { val := rb, property := rb_mem }, den := { val := sb, property := sb_mem },
            den_mem := s_nin }
y : { x // x ∈ Va ⊓ Vb }
h✝ : ↑{ val := sa * sb, property := (_ : sa * sb ∈ 𝒜 (ja + jb)) } ∈ (↑y).asHomogeneousIdeal
h : sa ∈ HomogeneousIdeal.toIdeal (↑y).asHomogeneousIdeal
⊢ False
[PROOFSTEP]
choose nin _ using wa ⟨y, (Opens.infLELeft Va Vb y).2⟩
[GOAL]
case intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.refine'_1.inl
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : { x // x ∈ U.unop }) → at ↑x
ha : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate a
hb : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate b
x : { x // x ∈ U.unop }
Va : Opens ↑(ProjectiveSpectrum.top 𝒜)
ma : ↑x ∈ Va
ia : Va ⟶ U.unop
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
wa :
  ∀ (x : { x // x ∈ Va }),
    ∃ s_nin,
      (fun x => a ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem },
            den_mem := s_nin }
Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)
mb : ↑x ∈ Vb
ib : Vb ⟶ U.unop
jb : ℕ
rb : A
rb_mem : rb ∈ 𝒜 jb
sb : A
sb_mem : sb ∈ 𝒜 jb
wb :
  ∀ (x : { x // x ∈ Vb }),
    ∃ s_nin,
      (fun x => b ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := jb, num := { val := rb, property := rb_mem }, den := { val := sb, property := sb_mem },
            den_mem := s_nin }
y : { x // x ∈ Va ⊓ Vb }
h✝ : ↑{ val := sa * sb, property := (_ : sa * sb ∈ 𝒜 (ja + jb)) } ∈ (↑y).asHomogeneousIdeal
h : sa ∈ HomogeneousIdeal.toIdeal (↑y).asHomogeneousIdeal
nin :
  ¬↑{ val := sa, property := sa_mem } ∈
      (↑{ val := ↑y,
            property := (_ : ↑((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑Va) }) y) ∈ Va) }).asHomogeneousIdeal
x✝ :
  (fun x => a ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x))
      { val := ↑y, property := (_ : ↑((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑Va) }) y) ∈ Va) } =
    Quotient.mk''
      { deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem }, den_mem := nin }
⊢ False
[PROOFSTEP]
exact nin h
[GOAL]
case intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.refine'_1.inr
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : { x // x ∈ U.unop }) → at ↑x
ha : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate a
hb : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate b
x : { x // x ∈ U.unop }
Va : Opens ↑(ProjectiveSpectrum.top 𝒜)
ma : ↑x ∈ Va
ia : Va ⟶ U.unop
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
wa :
  ∀ (x : { x // x ∈ Va }),
    ∃ s_nin,
      (fun x => a ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem },
            den_mem := s_nin }
Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)
mb : ↑x ∈ Vb
ib : Vb ⟶ U.unop
jb : ℕ
rb : A
rb_mem : rb ∈ 𝒜 jb
sb : A
sb_mem : sb ∈ 𝒜 jb
wb :
  ∀ (x : { x // x ∈ Vb }),
    ∃ s_nin,
      (fun x => b ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := jb, num := { val := rb, property := rb_mem }, den := { val := sb, property := sb_mem },
            den_mem := s_nin }
y : { x // x ∈ Va ⊓ Vb }
h✝ : ↑{ val := sa * sb, property := (_ : sa * sb ∈ 𝒜 (ja + jb)) } ∈ (↑y).asHomogeneousIdeal
h : sb ∈ HomogeneousIdeal.toIdeal (↑y).asHomogeneousIdeal
⊢ False
[PROOFSTEP]
choose nin _ using wb ⟨y, (Opens.infLERight Va Vb y).2⟩
[GOAL]
case intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.refine'_1.inr
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : { x // x ∈ U.unop }) → at ↑x
ha : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate a
hb : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate b
x : { x // x ∈ U.unop }
Va : Opens ↑(ProjectiveSpectrum.top 𝒜)
ma : ↑x ∈ Va
ia : Va ⟶ U.unop
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
wa :
  ∀ (x : { x // x ∈ Va }),
    ∃ s_nin,
      (fun x => a ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem },
            den_mem := s_nin }
Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)
mb : ↑x ∈ Vb
ib : Vb ⟶ U.unop
jb : ℕ
rb : A
rb_mem : rb ∈ 𝒜 jb
sb : A
sb_mem : sb ∈ 𝒜 jb
wb :
  ∀ (x : { x // x ∈ Vb }),
    ∃ s_nin,
      (fun x => b ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := jb, num := { val := rb, property := rb_mem }, den := { val := sb, property := sb_mem },
            den_mem := s_nin }
y : { x // x ∈ Va ⊓ Vb }
h✝ : ↑{ val := sa * sb, property := (_ : sa * sb ∈ 𝒜 (ja + jb)) } ∈ (↑y).asHomogeneousIdeal
h : sb ∈ HomogeneousIdeal.toIdeal (↑y).asHomogeneousIdeal
nin :
  ¬↑{ val := sb, property := sb_mem } ∈
      (↑{ val := ↑y,
            property := (_ : ↑((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑Vb) }) y) ∈ Vb) }).asHomogeneousIdeal
x✝ :
  (fun x => b ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x))
      { val := ↑y, property := (_ : ↑((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑Vb) }) y) ∈ Vb) } =
    Quotient.mk''
      { deg := jb, num := { val := rb, property := rb_mem }, den := { val := sb, property := sb_mem }, den_mem := nin }
⊢ False
[PROOFSTEP]
exact nin h
[GOAL]
case intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.refine'_2
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : { x // x ∈ U.unop }) → at ↑x
ha : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate a
hb : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate b
x : { x // x ∈ U.unop }
Va : Opens ↑(ProjectiveSpectrum.top 𝒜)
ma : ↑x ∈ Va
ia : Va ⟶ U.unop
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
wa :
  ∀ (x : { x // x ∈ Va }),
    ∃ s_nin,
      (fun x => a ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem },
            den_mem := s_nin }
Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)
mb : ↑x ∈ Vb
ib : Vb ⟶ U.unop
jb : ℕ
rb : A
rb_mem : rb ∈ 𝒜 jb
sb : A
sb_mem : sb ∈ 𝒜 jb
wb :
  ∀ (x : { x // x ∈ Vb }),
    ∃ s_nin,
      (fun x => b ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := jb, num := { val := rb, property := rb_mem }, den := { val := sb, property := sb_mem },
            den_mem := s_nin }
y : { x // x ∈ Va ⊓ Vb }
⊢ (fun x => (a * b) ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) y =
    Quotient.mk''
      { deg := ja + jb, num := { val := ra * rb, property := (_ : ra * rb ∈ 𝒜 (ja + jb)) },
        den := { val := sa * sb, property := (_ : sa * sb ∈ 𝒜 (ja + jb)) },
        den_mem :=
          (_ : ↑{ val := sa * sb, property := (_ : sa * sb ∈ 𝒜 (ja + jb)) } ∈ (↑y).asHomogeneousIdeal → False) }
[PROOFSTEP]
simp only [Pi.mul_apply, RingHom.map_mul]
[GOAL]
case intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.refine'_2
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : { x // x ∈ U.unop }) → at ↑x
ha : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate a
hb : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate b
x : { x // x ∈ U.unop }
Va : Opens ↑(ProjectiveSpectrum.top 𝒜)
ma : ↑x ∈ Va
ia : Va ⟶ U.unop
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
wa :
  ∀ (x : { x // x ∈ Va }),
    ∃ s_nin,
      (fun x => a ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem },
            den_mem := s_nin }
Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)
mb : ↑x ∈ Vb
ib : Vb ⟶ U.unop
jb : ℕ
rb : A
rb_mem : rb ∈ 𝒜 jb
sb : A
sb_mem : sb ∈ 𝒜 jb
wb :
  ∀ (x : { x // x ∈ Vb }),
    ∃ s_nin,
      (fun x => b ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := jb, num := { val := rb, property := rb_mem }, den := { val := sb, property := sb_mem },
            den_mem := s_nin }
y : { x // x ∈ Va ⊓ Vb }
⊢ a { val := ↑y, property := (_ : ↑y ∈ ↑U.unop) } * b { val := ↑y, property := (_ : ↑y ∈ ↑U.unop) } =
    Quotient.mk''
      { deg := ja + jb, num := { val := ra * rb, property := (_ : ra * rb ∈ 𝒜 (ja + jb)) },
        den := { val := sa * sb, property := (_ : sa * sb ∈ 𝒜 (ja + jb)) },
        den_mem :=
          (_ : ↑{ val := sa * sb, property := (_ : sa * sb ∈ 𝒜 (ja + jb)) } ∈ (↑y).asHomogeneousIdeal → False) }
[PROOFSTEP]
choose nin1 hy1 using wa (Opens.infLELeft Va Vb y)
[GOAL]
case intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.refine'_2
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : { x // x ∈ U.unop }) → at ↑x
ha : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate a
hb : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate b
x : { x // x ∈ U.unop }
Va : Opens ↑(ProjectiveSpectrum.top 𝒜)
ma : ↑x ∈ Va
ia : Va ⟶ U.unop
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
wa :
  ∀ (x : { x // x ∈ Va }),
    ∃ s_nin,
      (fun x => a ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem },
            den_mem := s_nin }
Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)
mb : ↑x ∈ Vb
ib : Vb ⟶ U.unop
jb : ℕ
rb : A
rb_mem : rb ∈ 𝒜 jb
sb : A
sb_mem : sb ∈ 𝒜 jb
wb :
  ∀ (x : { x // x ∈ Vb }),
    ∃ s_nin,
      (fun x => b ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := jb, num := { val := rb, property := rb_mem }, den := { val := sb, property := sb_mem },
            den_mem := s_nin }
y : { x // x ∈ Va ⊓ Vb }
nin1 :
  ¬↑{ val := sa, property := sa_mem } ∈ (↑((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑Va) }) y)).asHomogeneousIdeal
hy1 :
  (fun x => a ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x))
      ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑Va) }) y) =
    Quotient.mk''
      { deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem }, den_mem := nin1 }
⊢ a { val := ↑y, property := (_ : ↑y ∈ ↑U.unop) } * b { val := ↑y, property := (_ : ↑y ∈ ↑U.unop) } =
    Quotient.mk''
      { deg := ja + jb, num := { val := ra * rb, property := (_ : ra * rb ∈ 𝒜 (ja + jb)) },
        den := { val := sa * sb, property := (_ : sa * sb ∈ 𝒜 (ja + jb)) },
        den_mem :=
          (_ : ↑{ val := sa * sb, property := (_ : sa * sb ∈ 𝒜 (ja + jb)) } ∈ (↑y).asHomogeneousIdeal → False) }
[PROOFSTEP]
choose nin2 hy2 using wb (Opens.infLERight Va Vb y)
[GOAL]
case intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.refine'_2
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : { x // x ∈ U.unop }) → at ↑x
ha : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate a
hb : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate b
x : { x // x ∈ U.unop }
Va : Opens ↑(ProjectiveSpectrum.top 𝒜)
ma : ↑x ∈ Va
ia : Va ⟶ U.unop
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
wa :
  ∀ (x : { x // x ∈ Va }),
    ∃ s_nin,
      (fun x => a ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem },
            den_mem := s_nin }
Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)
mb : ↑x ∈ Vb
ib : Vb ⟶ U.unop
jb : ℕ
rb : A
rb_mem : rb ∈ 𝒜 jb
sb : A
sb_mem : sb ∈ 𝒜 jb
wb :
  ∀ (x : { x // x ∈ Vb }),
    ∃ s_nin,
      (fun x => b ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := jb, num := { val := rb, property := rb_mem }, den := { val := sb, property := sb_mem },
            den_mem := s_nin }
y : { x // x ∈ Va ⊓ Vb }
nin1 :
  ¬↑{ val := sa, property := sa_mem } ∈ (↑((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑Va) }) y)).asHomogeneousIdeal
hy1 :
  (fun x => a ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x))
      ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑Va) }) y) =
    Quotient.mk''
      { deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem }, den_mem := nin1 }
nin2 :
  ¬↑{ val := sb, property := sb_mem } ∈ (↑((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑Vb) }) y)).asHomogeneousIdeal
hy2 :
  (fun x => b ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x))
      ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑Vb) }) y) =
    Quotient.mk''
      { deg := jb, num := { val := rb, property := rb_mem }, den := { val := sb, property := sb_mem }, den_mem := nin2 }
⊢ a { val := ↑y, property := (_ : ↑y ∈ ↑U.unop) } * b { val := ↑y, property := (_ : ↑y ∈ ↑U.unop) } =
    Quotient.mk''
      { deg := ja + jb, num := { val := ra * rb, property := (_ : ra * rb ∈ 𝒜 (ja + jb)) },
        den := { val := sa * sb, property := (_ : sa * sb ∈ 𝒜 (ja + jb)) },
        den_mem :=
          (_ : ↑{ val := sa * sb, property := (_ : sa * sb ∈ 𝒜 (ja + jb)) } ∈ (↑y).asHomogeneousIdeal → False) }
[PROOFSTEP]
rw [ext_iff_val] at hy1 hy2 ⊢
[GOAL]
case intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.refine'_2
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : { x // x ∈ U.unop }) → at ↑x
ha : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate a
hb : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate b
x : { x // x ∈ U.unop }
Va : Opens ↑(ProjectiveSpectrum.top 𝒜)
ma : ↑x ∈ Va
ia : Va ⟶ U.unop
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
wa :
  ∀ (x : { x // x ∈ Va }),
    ∃ s_nin,
      (fun x => a ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem },
            den_mem := s_nin }
Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)
mb : ↑x ∈ Vb
ib : Vb ⟶ U.unop
jb : ℕ
rb : A
rb_mem : rb ∈ 𝒜 jb
sb : A
sb_mem : sb ∈ 𝒜 jb
wb :
  ∀ (x : { x // x ∈ Vb }),
    ∃ s_nin,
      (fun x => b ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := jb, num := { val := rb, property := rb_mem }, den := { val := sb, property := sb_mem },
            den_mem := s_nin }
y : { x // x ∈ Va ⊓ Vb }
nin1 :
  ¬↑{ val := sa, property := sa_mem } ∈ (↑((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑Va) }) y)).asHomogeneousIdeal
hy1 :
  val
      ((fun x => a ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x))
        ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑Va) }) y)) =
    val
      (Quotient.mk''
        { deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem },
          den_mem := nin1 })
nin2 :
  ¬↑{ val := sb, property := sb_mem } ∈ (↑((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑Vb) }) y)).asHomogeneousIdeal
hy2 :
  val
      ((fun x => b ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x))
        ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑Vb) }) y)) =
    val
      (Quotient.mk''
        { deg := jb, num := { val := rb, property := rb_mem }, den := { val := sb, property := sb_mem },
          den_mem := nin2 })
⊢ val (a { val := ↑y, property := (_ : ↑y ∈ ↑U.unop) } * b { val := ↑y, property := (_ : ↑y ∈ ↑U.unop) }) =
    val
      (Quotient.mk''
        { deg := ja + jb, num := { val := ra * rb, property := (_ : ra * rb ∈ 𝒜 (ja + jb)) },
          den := { val := sa * sb, property := (_ : sa * sb ∈ 𝒜 (ja + jb)) },
          den_mem :=
            (_ : ↑{ val := sa * sb, property := (_ : sa * sb ∈ 𝒜 (ja + jb)) } ∈ (↑y).asHomogeneousIdeal → False) })
[PROOFSTEP]
erw [mul_val, hy1, hy2]
[GOAL]
case intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.refine'_2
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : { x // x ∈ U.unop }) → at ↑x
ha : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate a
hb : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate b
x : { x // x ∈ U.unop }
Va : Opens ↑(ProjectiveSpectrum.top 𝒜)
ma : ↑x ∈ Va
ia : Va ⟶ U.unop
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
wa :
  ∀ (x : { x // x ∈ Va }),
    ∃ s_nin,
      (fun x => a ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem },
            den_mem := s_nin }
Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)
mb : ↑x ∈ Vb
ib : Vb ⟶ U.unop
jb : ℕ
rb : A
rb_mem : rb ∈ 𝒜 jb
sb : A
sb_mem : sb ∈ 𝒜 jb
wb :
  ∀ (x : { x // x ∈ Vb }),
    ∃ s_nin,
      (fun x => b ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := jb, num := { val := rb, property := rb_mem }, den := { val := sb, property := sb_mem },
            den_mem := s_nin }
y : { x // x ∈ Va ⊓ Vb }
nin1 :
  ¬↑{ val := sa, property := sa_mem } ∈ (↑((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑Va) }) y)).asHomogeneousIdeal
hy1 :
  val
      ((fun x => a ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x))
        ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑Va) }) y)) =
    val
      (Quotient.mk''
        { deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem },
          den_mem := nin1 })
nin2 :
  ¬↑{ val := sb, property := sb_mem } ∈ (↑((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑Vb) }) y)).asHomogeneousIdeal
hy2 :
  val
      ((fun x => b ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x))
        ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑Vb) }) y)) =
    val
      (Quotient.mk''
        { deg := jb, num := { val := rb, property := rb_mem }, den := { val := sb, property := sb_mem },
          den_mem := nin2 })
⊢ val
        (Quotient.mk''
          { deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem },
            den_mem := nin1 }) *
      val
        (Quotient.mk''
          { deg := jb, num := { val := rb, property := rb_mem }, den := { val := sb, property := sb_mem },
            den_mem := nin2 }) =
    val
      (Quotient.mk''
        { deg := ja + jb, num := { val := ra * rb, property := (_ : ra * rb ∈ 𝒜 (ja + jb)) },
          den := { val := sa * sb, property := (_ : sa * sb ∈ 𝒜 (ja + jb)) },
          den_mem :=
            (_ : ↑{ val := sa * sb, property := (_ : sa * sb ∈ 𝒜 (ja + jb)) } ∈ (↑y).asHomogeneousIdeal → False) })
[PROOFSTEP]
simp only [val_mk'', mk_mul]
[GOAL]
case intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.refine'_2
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : { x // x ∈ U.unop }) → at ↑x
ha : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate a
hb : PrelocalPredicate.pred (isLocallyFraction 𝒜).toPrelocalPredicate b
x : { x // x ∈ U.unop }
Va : Opens ↑(ProjectiveSpectrum.top 𝒜)
ma : ↑x ∈ Va
ia : Va ⟶ U.unop
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
wa :
  ∀ (x : { x // x ∈ Va }),
    ∃ s_nin,
      (fun x => a ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem },
            den_mem := s_nin }
Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)
mb : ↑x ∈ Vb
ib : Vb ⟶ U.unop
jb : ℕ
rb : A
rb_mem : rb ∈ 𝒜 jb
sb : A
sb_mem : sb ∈ 𝒜 jb
wb :
  ∀ (x : { x // x ∈ Vb }),
    ∃ s_nin,
      (fun x => b ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) x =
        Quotient.mk''
          { deg := jb, num := { val := rb, property := rb_mem }, den := { val := sb, property := sb_mem },
            den_mem := s_nin }
y : { x // x ∈ Va ⊓ Vb }
nin1 :
  ¬↑{ val := sa, property := sa_mem } ∈ (↑((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑Va) }) y)).asHomogeneousIdeal
hy1 :
  val
      ((fun x => a ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x))
        ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑Va) }) y)) =
    val
      (Quotient.mk''
        { deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem },
          den_mem := nin1 })
nin2 :
  ¬↑{ val := sb, property := sb_mem } ∈ (↑((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑Vb) }) y)).asHomogeneousIdeal
hy2 :
  val
      ((fun x => b ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x))
        ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑Vb) }) y)) =
    val
      (Quotient.mk''
        { deg := jb, num := { val := rb, property := rb_mem }, den := { val := sb, property := sb_mem },
          den_mem := nin2 })
⊢ Localization.mk (ra * rb)
      ({ val := sa,
          property :=
            (_ :
              ↑{ deg := ja, num := { val := ra, property := ra_mem }, den := { val := sa, property := sa_mem },
                      den_mem := nin1 }.den ∈
                Ideal.primeCompl (HomogeneousIdeal.toIdeal (↑y).asHomogeneousIdeal)) } *
        { val := sb,
          property :=
            (_ :
              ↑{ deg := jb, num := { val := rb, property := rb_mem }, den := { val := sb, property := sb_mem },
                      den_mem := nin2 }.den ∈
                Ideal.primeCompl (HomogeneousIdeal.toIdeal (↑y).asHomogeneousIdeal)) }) =
    Localization.mk (ra * rb)
      { val := sa * sb,
        property :=
          (_ :
            ↑{ deg := ja + jb, num := { val := ra * rb, property := (_ : ra * rb ∈ 𝒜 (ja + jb)) },
                    den := { val := sa * sb, property := (_ : sa * sb ∈ 𝒜 (ja + jb)) },
                    den_mem :=
                      (_ :
                        ↑{ val := sa * sb, property := (_ : sa * sb ∈ 𝒜 (ja + jb)) } ∈ (↑y).asHomogeneousIdeal →
                          False) }.den ∈
              Ideal.primeCompl (HomogeneousIdeal.toIdeal (↑y).asHomogeneousIdeal)) }
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
⊢ ∀ {X Y : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ} (f : X ⟶ Y),
    (structurePresheafInCommRing 𝒜 ⋙ forget CommRingCat).map f ≫
        ((fun U => Iso.refl ((structurePresheafInCommRing 𝒜 ⋙ forget CommRingCat).obj U)) Y).hom =
      ((fun U => Iso.refl ((structurePresheafInCommRing 𝒜 ⋙ forget CommRingCat).obj U)) X).hom ≫
        (structureSheafInType 𝒜).val.map f
[PROOFSTEP]
aesop_cat
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
f : at x
⊢ x ∈ ProjectiveSpectrum.basicOpen 𝒜 (HomogeneousLocalization.den f)
[PROOFSTEP]
rw [ProjectiveSpectrum.mem_basicOpen]
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
f : at x
⊢ ¬HomogeneousLocalization.den f ∈ x.asHomogeneousIdeal
[PROOFSTEP]
exact f.den_mem
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
z1 z2 : ↑(Presheaf.stalk (Sheaf.presheaf (Proj.structureSheaf 𝒜)) x)
eq1 : ↑(stalkToFiberRingHom 𝒜 x) z1 = ↑(stalkToFiberRingHom 𝒜 x) z2
⊢ z1 = z2
[PROOFSTEP]
obtain ⟨u1, memu1, s1, rfl⟩ := (Proj.structureSheaf 𝒜).presheaf.germ_exist x z1
[GOAL]
case intro.intro.intro
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
z2 : ↑(Presheaf.stalk (Sheaf.presheaf (Proj.structureSheaf 𝒜)) x)
u1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu1 : x ∈ u1
s1 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u1))
eq1 :
  ↑(stalkToFiberRingHom 𝒜 x)
      (↑(Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) { val := x, property := memu1 }) s1) =
    ↑(stalkToFiberRingHom 𝒜 x) z2
⊢ ↑(Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) { val := x, property := memu1 }) s1 = z2
[PROOFSTEP]
obtain ⟨u2, memu2, s2, rfl⟩ := (Proj.structureSheaf 𝒜).presheaf.germ_exist x z2
[GOAL]
case intro.intro.intro.intro.intro.intro
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
u1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu1 : x ∈ u1
s1 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u1))
u2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu2 : x ∈ u2
s2 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u2))
eq1 :
  ↑(stalkToFiberRingHom 𝒜 x)
      (↑(Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) { val := x, property := memu1 }) s1) =
    ↑(stalkToFiberRingHom 𝒜 x)
      (↑(Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) { val := x, property := memu2 }) s2)
⊢ ↑(Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) { val := x, property := memu1 }) s1 =
    ↑(Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) { val := x, property := memu2 }) s2
[PROOFSTEP]
obtain ⟨v1, memv1, i1, ⟨j1, ⟨a1, a1_mem⟩, ⟨b1, b1_mem⟩, hs1⟩⟩ := s1.2 ⟨x, memu1⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk.intro.mk
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
u1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu1 : x ∈ u1
s1 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u1))
u2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu2 : x ∈ u2
s2 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u2))
eq1 :
  ↑(stalkToFiberRingHom 𝒜 x)
      (↑(Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) { val := x, property := memu1 }) s1) =
    ↑(stalkToFiberRingHom 𝒜 x)
      (↑(Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) { val := x, property := memu2 }) s2)
v1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv1 : ↑{ val := x, property := memu1 } ∈ v1
i1 : v1 ⟶ (op u1).unop
j1 : ℕ
a1 : A
a1_mem : a1 ∈ 𝒜 j1
b1 : A
b1_mem : b1 ∈ 𝒜 j1
hs1 :
  ∀ (x : { x // x ∈ v1 }),
    ∃ s_nin,
      (fun x => ↑s1 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u1).unop) }) x)) x =
        Quotient.mk''
          { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
            den_mem := s_nin }
⊢ ↑(Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) { val := x, property := memu1 }) s1 =
    ↑(Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) { val := x, property := memu2 }) s2
[PROOFSTEP]
obtain ⟨v2, memv2, i2, ⟨j2, ⟨a2, a2_mem⟩, ⟨b2, b2_mem⟩, hs2⟩⟩ := s2.2 ⟨x, memu2⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
u1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu1 : x ∈ u1
s1 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u1))
u2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu2 : x ∈ u2
s2 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u2))
eq1 :
  ↑(stalkToFiberRingHom 𝒜 x)
      (↑(Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) { val := x, property := memu1 }) s1) =
    ↑(stalkToFiberRingHom 𝒜 x)
      (↑(Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) { val := x, property := memu2 }) s2)
v1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv1 : ↑{ val := x, property := memu1 } ∈ v1
i1 : v1 ⟶ (op u1).unop
j1 : ℕ
a1 : A
a1_mem : a1 ∈ 𝒜 j1
b1 : A
b1_mem : b1 ∈ 𝒜 j1
hs1 :
  ∀ (x : { x // x ∈ v1 }),
    ∃ s_nin,
      (fun x => ↑s1 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u1).unop) }) x)) x =
        Quotient.mk''
          { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
            den_mem := s_nin }
v2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv2 : ↑{ val := x, property := memu2 } ∈ v2
i2 : v2 ⟶ (op u2).unop
j2 : ℕ
a2 : A
a2_mem : a2 ∈ 𝒜 j2
b2 : A
b2_mem : b2 ∈ 𝒜 j2
hs2 :
  ∀ (x : { x // x ∈ v2 }),
    ∃ s_nin,
      (fun x => ↑s2 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u2).unop) }) x)) x =
        Quotient.mk''
          { deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
            den_mem := s_nin }
⊢ ↑(Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) { val := x, property := memu1 }) s1 =
    ↑(Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) { val := x, property := memu2 }) s2
[PROOFSTEP]
obtain ⟨b1_nin_x, eq2⟩ := hs1 ⟨x, memv1⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.intro
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
u1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu1 : x ∈ u1
s1 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u1))
u2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu2 : x ∈ u2
s2 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u2))
eq1 :
  ↑(stalkToFiberRingHom 𝒜 x)
      (↑(Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) { val := x, property := memu1 }) s1) =
    ↑(stalkToFiberRingHom 𝒜 x)
      (↑(Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) { val := x, property := memu2 }) s2)
v1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv1 : ↑{ val := x, property := memu1 } ∈ v1
i1 : v1 ⟶ (op u1).unop
j1 : ℕ
a1 : A
a1_mem : a1 ∈ 𝒜 j1
b1 : A
b1_mem : b1 ∈ 𝒜 j1
hs1 :
  ∀ (x : { x // x ∈ v1 }),
    ∃ s_nin,
      (fun x => ↑s1 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u1).unop) }) x)) x =
        Quotient.mk''
          { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
            den_mem := s_nin }
v2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv2 : ↑{ val := x, property := memu2 } ∈ v2
i2 : v2 ⟶ (op u2).unop
j2 : ℕ
a2 : A
a2_mem : a2 ∈ 𝒜 j2
b2 : A
b2_mem : b2 ∈ 𝒜 j2
hs2 :
  ∀ (x : { x // x ∈ v2 }),
    ∃ s_nin,
      (fun x => ↑s2 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u2).unop) }) x)) x =
        Quotient.mk''
          { deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
            den_mem := s_nin }
b1_nin_x : ¬↑{ val := b1, property := b1_mem } ∈ (↑{ val := x, property := memv1 }).asHomogeneousIdeal
eq2 :
  (fun x => ↑s1 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u1).unop) }) x)) { val := x, property := memv1 } =
    Quotient.mk''
      { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
        den_mem := b1_nin_x }
⊢ ↑(Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) { val := x, property := memu1 }) s1 =
    ↑(Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) { val := x, property := memu2 }) s2
[PROOFSTEP]
obtain ⟨b2_nin_x, eq3⟩ := hs2 ⟨x, memv2⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.intro.intro
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
u1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu1 : x ∈ u1
s1 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u1))
u2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu2 : x ∈ u2
s2 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u2))
eq1 :
  ↑(stalkToFiberRingHom 𝒜 x)
      (↑(Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) { val := x, property := memu1 }) s1) =
    ↑(stalkToFiberRingHom 𝒜 x)
      (↑(Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) { val := x, property := memu2 }) s2)
v1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv1 : ↑{ val := x, property := memu1 } ∈ v1
i1 : v1 ⟶ (op u1).unop
j1 : ℕ
a1 : A
a1_mem : a1 ∈ 𝒜 j1
b1 : A
b1_mem : b1 ∈ 𝒜 j1
hs1 :
  ∀ (x : { x // x ∈ v1 }),
    ∃ s_nin,
      (fun x => ↑s1 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u1).unop) }) x)) x =
        Quotient.mk''
          { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
            den_mem := s_nin }
v2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv2 : ↑{ val := x, property := memu2 } ∈ v2
i2 : v2 ⟶ (op u2).unop
j2 : ℕ
a2 : A
a2_mem : a2 ∈ 𝒜 j2
b2 : A
b2_mem : b2 ∈ 𝒜 j2
hs2 :
  ∀ (x : { x // x ∈ v2 }),
    ∃ s_nin,
      (fun x => ↑s2 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u2).unop) }) x)) x =
        Quotient.mk''
          { deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
            den_mem := s_nin }
b1_nin_x : ¬↑{ val := b1, property := b1_mem } ∈ (↑{ val := x, property := memv1 }).asHomogeneousIdeal
eq2 :
  (fun x => ↑s1 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u1).unop) }) x)) { val := x, property := memv1 } =
    Quotient.mk''
      { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
        den_mem := b1_nin_x }
b2_nin_x : ¬↑{ val := b2, property := b2_mem } ∈ (↑{ val := x, property := memv2 }).asHomogeneousIdeal
eq3 :
  (fun x => ↑s2 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u2).unop) }) x)) { val := x, property := memv2 } =
    Quotient.mk''
      { deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
        den_mem := b2_nin_x }
⊢ ↑(Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) { val := x, property := memu1 }) s1 =
    ↑(Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) { val := x, property := memu2 }) s2
[PROOFSTEP]
dsimp only at eq1 eq2 eq3
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.intro.intro
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
u1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu1 : x ∈ u1
s1 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u1))
u2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu2 : x ∈ u2
s2 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u2))
eq1 :
  ↑(stalkToFiberRingHom 𝒜 x)
      (↑(Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) { val := x, property := memu1 }) s1) =
    ↑(stalkToFiberRingHom 𝒜 x)
      (↑(Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) { val := x, property := memu2 }) s2)
v1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv1 : ↑{ val := x, property := memu1 } ∈ v1
i1 : v1 ⟶ (op u1).unop
j1 : ℕ
a1 : A
a1_mem : a1 ∈ 𝒜 j1
b1 : A
b1_mem : b1 ∈ 𝒜 j1
hs1 :
  ∀ (x : { x // x ∈ v1 }),
    ∃ s_nin,
      (fun x => ↑s1 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u1).unop) }) x)) x =
        Quotient.mk''
          { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
            den_mem := s_nin }
v2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv2 : ↑{ val := x, property := memu2 } ∈ v2
i2 : v2 ⟶ (op u2).unop
j2 : ℕ
a2 : A
a2_mem : a2 ∈ 𝒜 j2
b2 : A
b2_mem : b2 ∈ 𝒜 j2
hs2 :
  ∀ (x : { x // x ∈ v2 }),
    ∃ s_nin,
      (fun x => ↑s2 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u2).unop) }) x)) x =
        Quotient.mk''
          { deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
            den_mem := s_nin }
b1_nin_x : ¬↑{ val := b1, property := b1_mem } ∈ (↑{ val := x, property := memv1 }).asHomogeneousIdeal
eq2 :
  ↑s1 { val := x, property := (_ : ↑{ val := x, property := memv1 } ∈ ↑(op u1).unop) } =
    Quotient.mk''
      { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
        den_mem := b1_nin_x }
b2_nin_x : ¬↑{ val := b2, property := b2_mem } ∈ (↑{ val := x, property := memv2 }).asHomogeneousIdeal
eq3 :
  ↑s2 { val := x, property := (_ : ↑{ val := x, property := memv2 } ∈ ↑(op u2).unop) } =
    Quotient.mk''
      { deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
        den_mem := b2_nin_x }
⊢ ↑(Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) { val := x, property := memu1 }) s1 =
    ↑(Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) { val := x, property := memu2 }) s2
[PROOFSTEP]
erw [stalkToFiberRingHom_germ 𝒜 u1 ⟨x, memu1⟩ s1, stalkToFiberRingHom_germ 𝒜 u2 ⟨x, memu2⟩ s2] at eq1
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.intro.intro
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
u1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu1 : x ∈ u1
s1 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u1))
u2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu2 : x ∈ u2
s2 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u2))
eq1 : ↑s1 { val := x, property := memu1 } = ↑s2 { val := x, property := memu2 }
v1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv1 : ↑{ val := x, property := memu1 } ∈ v1
i1 : v1 ⟶ (op u1).unop
j1 : ℕ
a1 : A
a1_mem : a1 ∈ 𝒜 j1
b1 : A
b1_mem : b1 ∈ 𝒜 j1
hs1 :
  ∀ (x : { x // x ∈ v1 }),
    ∃ s_nin,
      (fun x => ↑s1 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u1).unop) }) x)) x =
        Quotient.mk''
          { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
            den_mem := s_nin }
v2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv2 : ↑{ val := x, property := memu2 } ∈ v2
i2 : v2 ⟶ (op u2).unop
j2 : ℕ
a2 : A
a2_mem : a2 ∈ 𝒜 j2
b2 : A
b2_mem : b2 ∈ 𝒜 j2
hs2 :
  ∀ (x : { x // x ∈ v2 }),
    ∃ s_nin,
      (fun x => ↑s2 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u2).unop) }) x)) x =
        Quotient.mk''
          { deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
            den_mem := s_nin }
b1_nin_x : ¬↑{ val := b1, property := b1_mem } ∈ (↑{ val := x, property := memv1 }).asHomogeneousIdeal
eq2 :
  ↑s1 { val := x, property := (_ : ↑{ val := x, property := memv1 } ∈ ↑(op u1).unop) } =
    Quotient.mk''
      { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
        den_mem := b1_nin_x }
b2_nin_x : ¬↑{ val := b2, property := b2_mem } ∈ (↑{ val := x, property := memv2 }).asHomogeneousIdeal
eq3 :
  ↑s2 { val := x, property := (_ : ↑{ val := x, property := memv2 } ∈ ↑(op u2).unop) } =
    Quotient.mk''
      { deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
        den_mem := b2_nin_x }
⊢ ↑(Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) { val := x, property := memu1 }) s1 =
    ↑(Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) { val := x, property := memu2 }) s2
[PROOFSTEP]
erw [eq1] at eq2
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.intro.intro
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
u1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu1 : x ∈ u1
s1 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u1))
u2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu2 : x ∈ u2
s2 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u2))
eq1 : ↑s1 { val := x, property := memu1 } = ↑s2 { val := x, property := memu2 }
v1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv1 : ↑{ val := x, property := memu1 } ∈ v1
i1 : v1 ⟶ (op u1).unop
j1 : ℕ
a1 : A
a1_mem : a1 ∈ 𝒜 j1
b1 : A
b1_mem : b1 ∈ 𝒜 j1
hs1 :
  ∀ (x : { x // x ∈ v1 }),
    ∃ s_nin,
      (fun x => ↑s1 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u1).unop) }) x)) x =
        Quotient.mk''
          { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
            den_mem := s_nin }
v2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv2 : ↑{ val := x, property := memu2 } ∈ v2
i2 : v2 ⟶ (op u2).unop
j2 : ℕ
a2 : A
a2_mem : a2 ∈ 𝒜 j2
b2 : A
b2_mem : b2 ∈ 𝒜 j2
hs2 :
  ∀ (x : { x // x ∈ v2 }),
    ∃ s_nin,
      (fun x => ↑s2 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u2).unop) }) x)) x =
        Quotient.mk''
          { deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
            den_mem := s_nin }
b1_nin_x : ¬↑{ val := b1, property := b1_mem } ∈ (↑{ val := x, property := memv1 }).asHomogeneousIdeal
eq2 :
  ↑s2 { val := x, property := memu2 } =
    Quotient.mk''
      { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
        den_mem := b1_nin_x }
b2_nin_x : ¬↑{ val := b2, property := b2_mem } ∈ (↑{ val := x, property := memv2 }).asHomogeneousIdeal
eq3 :
  ↑s2 { val := x, property := (_ : ↑{ val := x, property := memv2 } ∈ ↑(op u2).unop) } =
    Quotient.mk''
      { deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
        den_mem := b2_nin_x }
⊢ ↑(Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) { val := x, property := memu1 }) s1 =
    ↑(Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) { val := x, property := memu2 }) s2
[PROOFSTEP]
erw [eq2, Quotient.eq''] at eq3
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.intro.intro
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
u1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu1 : x ∈ u1
s1 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u1))
u2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu2 : x ∈ u2
s2 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u2))
eq1 : ↑s1 { val := x, property := memu1 } = ↑s2 { val := x, property := memu2 }
v1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv1 : ↑{ val := x, property := memu1 } ∈ v1
i1 : v1 ⟶ (op u1).unop
j1 : ℕ
a1 : A
a1_mem : a1 ∈ 𝒜 j1
b1 : A
b1_mem : b1 ∈ 𝒜 j1
hs1 :
  ∀ (x : { x // x ∈ v1 }),
    ∃ s_nin,
      (fun x => ↑s1 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u1).unop) }) x)) x =
        Quotient.mk''
          { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
            den_mem := s_nin }
v2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv2 : ↑{ val := x, property := memu2 } ∈ v2
i2 : v2 ⟶ (op u2).unop
j2 : ℕ
a2 : A
a2_mem : a2 ∈ 𝒜 j2
b2 : A
b2_mem : b2 ∈ 𝒜 j2
hs2 :
  ∀ (x : { x // x ∈ v2 }),
    ∃ s_nin,
      (fun x => ↑s2 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u2).unop) }) x)) x =
        Quotient.mk''
          { deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
            den_mem := s_nin }
b1_nin_x : ¬↑{ val := b1, property := b1_mem } ∈ (↑{ val := x, property := memv1 }).asHomogeneousIdeal
eq2 :
  ↑s2 { val := x, property := memu2 } =
    Quotient.mk''
      { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
        den_mem := b1_nin_x }
b2_nin_x : ¬↑{ val := b2, property := b2_mem } ∈ (↑{ val := x, property := memv2 }).asHomogeneousIdeal
eq3 :
  Setoid.r
    { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
      den_mem := b1_nin_x }
    { deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
      den_mem := b2_nin_x }
⊢ ↑(Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) { val := x, property := memu1 }) s1 =
    ↑(Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) { val := x, property := memu2 }) s2
[PROOFSTEP]
change Localization.mk _ _ = Localization.mk _ _ at eq3
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.intro.intro
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
u1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu1 : x ∈ u1
s1 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u1))
u2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu2 : x ∈ u2
s2 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u2))
eq1 : ↑s1 { val := x, property := memu1 } = ↑s2 { val := x, property := memu2 }
v1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv1 : ↑{ val := x, property := memu1 } ∈ v1
i1 : v1 ⟶ (op u1).unop
j1 : ℕ
a1 : A
a1_mem : a1 ∈ 𝒜 j1
b1 : A
b1_mem : b1 ∈ 𝒜 j1
hs1 :
  ∀ (x : { x // x ∈ v1 }),
    ∃ s_nin,
      (fun x => ↑s1 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u1).unop) }) x)) x =
        Quotient.mk''
          { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
            den_mem := s_nin }
v2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv2 : ↑{ val := x, property := memu2 } ∈ v2
i2 : v2 ⟶ (op u2).unop
j2 : ℕ
a2 : A
a2_mem : a2 ∈ 𝒜 j2
b2 : A
b2_mem : b2 ∈ 𝒜 j2
hs2 :
  ∀ (x : { x // x ∈ v2 }),
    ∃ s_nin,
      (fun x => ↑s2 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u2).unop) }) x)) x =
        Quotient.mk''
          { deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
            den_mem := s_nin }
b1_nin_x : ¬↑{ val := b1, property := b1_mem } ∈ (↑{ val := x, property := memv1 }).asHomogeneousIdeal
eq2 :
  ↑s2 { val := x, property := memu2 } =
    Quotient.mk''
      { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
        den_mem := b1_nin_x }
b2_nin_x : ¬↑{ val := b2, property := b2_mem } ∈ (↑{ val := x, property := memv2 }).asHomogeneousIdeal
eq3 :
  Localization.mk
      ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
            den_mem := b1_nin_x }.num
      {
        val :=
          ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                den_mem := b1_nin_x }.den,
        property :=
          (_ :
            ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                    den_mem := b1_nin_x }.den ∈
              Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } =
    Localization.mk
      ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
            den_mem := b2_nin_x }.num
      {
        val :=
          ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                den_mem := b2_nin_x }.den,
        property :=
          (_ :
            ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                    den_mem := b2_nin_x }.den ∈
              Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) }
⊢ ↑(Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) { val := x, property := memu1 }) s1 =
    ↑(Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) { val := x, property := memu2 }) s2
[PROOFSTEP]
rw [Localization.mk_eq_mk', IsLocalization.eq] at eq3
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.intro.intro
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
u1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu1 : x ∈ u1
s1 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u1))
u2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu2 : x ∈ u2
s2 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u2))
eq1 : ↑s1 { val := x, property := memu1 } = ↑s2 { val := x, property := memu2 }
v1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv1 : ↑{ val := x, property := memu1 } ∈ v1
i1 : v1 ⟶ (op u1).unop
j1 : ℕ
a1 : A
a1_mem : a1 ∈ 𝒜 j1
b1 : A
b1_mem : b1 ∈ 𝒜 j1
hs1 :
  ∀ (x : { x // x ∈ v1 }),
    ∃ s_nin,
      (fun x => ↑s1 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u1).unop) }) x)) x =
        Quotient.mk''
          { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
            den_mem := s_nin }
v2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv2 : ↑{ val := x, property := memu2 } ∈ v2
i2 : v2 ⟶ (op u2).unop
j2 : ℕ
a2 : A
a2_mem : a2 ∈ 𝒜 j2
b2 : A
b2_mem : b2 ∈ 𝒜 j2
hs2 :
  ∀ (x : { x // x ∈ v2 }),
    ∃ s_nin,
      (fun x => ↑s2 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u2).unop) }) x)) x =
        Quotient.mk''
          { deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
            den_mem := s_nin }
b1_nin_x : ¬↑{ val := b1, property := b1_mem } ∈ (↑{ val := x, property := memv1 }).asHomogeneousIdeal
eq2 :
  ↑s2 { val := x, property := memu2 } =
    Quotient.mk''
      { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
        den_mem := b1_nin_x }
b2_nin_x : ¬↑{ val := b2, property := b2_mem } ∈ (↑{ val := x, property := memv2 }).asHomogeneousIdeal
eq3 :
  ∃ c,
    ↑c *
        (↑{
              val :=
                ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                      den_mem := b2_nin_x }.den,
              property :=
                (_ :
                  ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                          den_mem := b2_nin_x }.den ∈
                    Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
          ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                den_mem := b1_nin_x }.num) =
      ↑c *
        (↑{
              val :=
                ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                      den_mem := b1_nin_x }.den,
              property :=
                (_ :
                  ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                          den_mem := b1_nin_x }.den ∈
                    Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
          ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                den_mem := b2_nin_x }.num)
⊢ ↑(Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) { val := x, property := memu1 }) s1 =
    ↑(Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) { val := x, property := memu2 }) s2
[PROOFSTEP]
obtain ⟨⟨c, hc⟩, eq3⟩ := eq3
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.mk
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
u1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu1 : x ∈ u1
s1 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u1))
u2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu2 : x ∈ u2
s2 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u2))
eq1 : ↑s1 { val := x, property := memu1 } = ↑s2 { val := x, property := memu2 }
v1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv1 : ↑{ val := x, property := memu1 } ∈ v1
i1 : v1 ⟶ (op u1).unop
j1 : ℕ
a1 : A
a1_mem : a1 ∈ 𝒜 j1
b1 : A
b1_mem : b1 ∈ 𝒜 j1
hs1 :
  ∀ (x : { x // x ∈ v1 }),
    ∃ s_nin,
      (fun x => ↑s1 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u1).unop) }) x)) x =
        Quotient.mk''
          { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
            den_mem := s_nin }
v2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv2 : ↑{ val := x, property := memu2 } ∈ v2
i2 : v2 ⟶ (op u2).unop
j2 : ℕ
a2 : A
a2_mem : a2 ∈ 𝒜 j2
b2 : A
b2_mem : b2 ∈ 𝒜 j2
hs2 :
  ∀ (x : { x // x ∈ v2 }),
    ∃ s_nin,
      (fun x => ↑s2 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u2).unop) }) x)) x =
        Quotient.mk''
          { deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
            den_mem := s_nin }
b1_nin_x : ¬↑{ val := b1, property := b1_mem } ∈ (↑{ val := x, property := memv1 }).asHomogeneousIdeal
eq2 :
  ↑s2 { val := x, property := memu2 } =
    Quotient.mk''
      { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
        den_mem := b1_nin_x }
b2_nin_x : ¬↑{ val := b2, property := b2_mem } ∈ (↑{ val := x, property := memv2 }).asHomogeneousIdeal
c : A
hc : c ∈ Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)
eq3 :
  ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                    den_mem := b2_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                        den_mem := b2_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
              den_mem := b1_nin_x }.num) =
    ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                    den_mem := b1_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                        den_mem := b1_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
              den_mem := b2_nin_x }.num)
⊢ ↑(Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) { val := x, property := memu1 }) s1 =
    ↑(Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) { val := x, property := memu2 }) s2
[PROOFSTEP]
have eq3' :
  ∀ (y : ProjectiveSpectrum.top 𝒜)
    (hy : y ∈ ProjectiveSpectrum.basicOpen 𝒜 b1 ⊓ ProjectiveSpectrum.basicOpen 𝒜 b2 ⊓ ProjectiveSpectrum.basicOpen 𝒜 c),
    (Localization.mk a1
          ⟨b1,
            show b1 ∉ y.asHomogeneousIdeal by
              rw [← ProjectiveSpectrum.mem_basicOpen]
              exact leOfHom (Opens.infLELeft _ _ ≫ Opens.infLELeft _ _) hy⟩ :
        Localization.AtPrime y.1.toIdeal) =
      Localization.mk a2
        ⟨b2, by
          change b2 ∉ y.asHomogeneousIdeal
          rw [← ProjectiveSpectrum.mem_basicOpen]
          exact leOfHom (Opens.infLELeft _ _ ≫ Opens.infLERight _ _) hy⟩ :=
  by
  intro y hy
  rw [Localization.mk_eq_mk', IsLocalization.eq]
  exact
    ⟨⟨c,
        show c ∉ y.asHomogeneousIdeal by
          rw [← ProjectiveSpectrum.mem_basicOpen]
          exact leOfHom (Opens.infLERight _ _) hy⟩,
      eq3⟩
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
u1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu1 : x ∈ u1
s1 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u1))
u2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu2 : x ∈ u2
s2 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u2))
eq1 : ↑s1 { val := x, property := memu1 } = ↑s2 { val := x, property := memu2 }
v1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv1 : ↑{ val := x, property := memu1 } ∈ v1
i1 : v1 ⟶ (op u1).unop
j1 : ℕ
a1 : A
a1_mem : a1 ∈ 𝒜 j1
b1 : A
b1_mem : b1 ∈ 𝒜 j1
hs1 :
  ∀ (x : { x // x ∈ v1 }),
    ∃ s_nin,
      (fun x => ↑s1 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u1).unop) }) x)) x =
        Quotient.mk''
          { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
            den_mem := s_nin }
v2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv2 : ↑{ val := x, property := memu2 } ∈ v2
i2 : v2 ⟶ (op u2).unop
j2 : ℕ
a2 : A
a2_mem : a2 ∈ 𝒜 j2
b2 : A
b2_mem : b2 ∈ 𝒜 j2
hs2 :
  ∀ (x : { x // x ∈ v2 }),
    ∃ s_nin,
      (fun x => ↑s2 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u2).unop) }) x)) x =
        Quotient.mk''
          { deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
            den_mem := s_nin }
b1_nin_x : ¬↑{ val := b1, property := b1_mem } ∈ (↑{ val := x, property := memv1 }).asHomogeneousIdeal
eq2 :
  ↑s2 { val := x, property := memu2 } =
    Quotient.mk''
      { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
        den_mem := b1_nin_x }
b2_nin_x : ¬↑{ val := b2, property := b2_mem } ∈ (↑{ val := x, property := memv2 }).asHomogeneousIdeal
c : A
hc : c ∈ Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)
eq3 :
  ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                    den_mem := b2_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                        den_mem := b2_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
              den_mem := b1_nin_x }.num) =
    ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                    den_mem := b1_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                        den_mem := b1_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
              den_mem := b2_nin_x }.num)
y : ↑(ProjectiveSpectrum.top 𝒜)
hy : y ∈ ProjectiveSpectrum.basicOpen 𝒜 b1 ⊓ ProjectiveSpectrum.basicOpen 𝒜 b2 ⊓ ProjectiveSpectrum.basicOpen 𝒜 c
⊢ ¬b1 ∈ y.asHomogeneousIdeal
[PROOFSTEP]
rw [← ProjectiveSpectrum.mem_basicOpen]
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
u1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu1 : x ∈ u1
s1 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u1))
u2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu2 : x ∈ u2
s2 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u2))
eq1 : ↑s1 { val := x, property := memu1 } = ↑s2 { val := x, property := memu2 }
v1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv1 : ↑{ val := x, property := memu1 } ∈ v1
i1 : v1 ⟶ (op u1).unop
j1 : ℕ
a1 : A
a1_mem : a1 ∈ 𝒜 j1
b1 : A
b1_mem : b1 ∈ 𝒜 j1
hs1 :
  ∀ (x : { x // x ∈ v1 }),
    ∃ s_nin,
      (fun x => ↑s1 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u1).unop) }) x)) x =
        Quotient.mk''
          { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
            den_mem := s_nin }
v2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv2 : ↑{ val := x, property := memu2 } ∈ v2
i2 : v2 ⟶ (op u2).unop
j2 : ℕ
a2 : A
a2_mem : a2 ∈ 𝒜 j2
b2 : A
b2_mem : b2 ∈ 𝒜 j2
hs2 :
  ∀ (x : { x // x ∈ v2 }),
    ∃ s_nin,
      (fun x => ↑s2 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u2).unop) }) x)) x =
        Quotient.mk''
          { deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
            den_mem := s_nin }
b1_nin_x : ¬↑{ val := b1, property := b1_mem } ∈ (↑{ val := x, property := memv1 }).asHomogeneousIdeal
eq2 :
  ↑s2 { val := x, property := memu2 } =
    Quotient.mk''
      { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
        den_mem := b1_nin_x }
b2_nin_x : ¬↑{ val := b2, property := b2_mem } ∈ (↑{ val := x, property := memv2 }).asHomogeneousIdeal
c : A
hc : c ∈ Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)
eq3 :
  ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                    den_mem := b2_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                        den_mem := b2_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
              den_mem := b1_nin_x }.num) =
    ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                    den_mem := b1_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                        den_mem := b1_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
              den_mem := b2_nin_x }.num)
y : ↑(ProjectiveSpectrum.top 𝒜)
hy : y ∈ ProjectiveSpectrum.basicOpen 𝒜 b1 ⊓ ProjectiveSpectrum.basicOpen 𝒜 b2 ⊓ ProjectiveSpectrum.basicOpen 𝒜 c
⊢ y ∈ ProjectiveSpectrum.basicOpen 𝒜 b1
[PROOFSTEP]
exact leOfHom (Opens.infLELeft _ _ ≫ Opens.infLELeft _ _) hy
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
u1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu1 : x ∈ u1
s1 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u1))
u2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu2 : x ∈ u2
s2 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u2))
eq1 : ↑s1 { val := x, property := memu1 } = ↑s2 { val := x, property := memu2 }
v1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv1 : ↑{ val := x, property := memu1 } ∈ v1
i1 : v1 ⟶ (op u1).unop
j1 : ℕ
a1 : A
a1_mem : a1 ∈ 𝒜 j1
b1 : A
b1_mem : b1 ∈ 𝒜 j1
hs1 :
  ∀ (x : { x // x ∈ v1 }),
    ∃ s_nin,
      (fun x => ↑s1 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u1).unop) }) x)) x =
        Quotient.mk''
          { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
            den_mem := s_nin }
v2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv2 : ↑{ val := x, property := memu2 } ∈ v2
i2 : v2 ⟶ (op u2).unop
j2 : ℕ
a2 : A
a2_mem : a2 ∈ 𝒜 j2
b2 : A
b2_mem : b2 ∈ 𝒜 j2
hs2 :
  ∀ (x : { x // x ∈ v2 }),
    ∃ s_nin,
      (fun x => ↑s2 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u2).unop) }) x)) x =
        Quotient.mk''
          { deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
            den_mem := s_nin }
b1_nin_x : ¬↑{ val := b1, property := b1_mem } ∈ (↑{ val := x, property := memv1 }).asHomogeneousIdeal
eq2 :
  ↑s2 { val := x, property := memu2 } =
    Quotient.mk''
      { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
        den_mem := b1_nin_x }
b2_nin_x : ¬↑{ val := b2, property := b2_mem } ∈ (↑{ val := x, property := memv2 }).asHomogeneousIdeal
c : A
hc : c ∈ Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)
eq3 :
  ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                    den_mem := b2_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                        den_mem := b2_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
              den_mem := b1_nin_x }.num) =
    ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                    den_mem := b1_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                        den_mem := b1_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
              den_mem := b2_nin_x }.num)
y : ↑(ProjectiveSpectrum.top 𝒜)
hy : y ∈ ProjectiveSpectrum.basicOpen 𝒜 b1 ⊓ ProjectiveSpectrum.basicOpen 𝒜 b2 ⊓ ProjectiveSpectrum.basicOpen 𝒜 c
⊢ b2 ∈ Ideal.primeCompl (HomogeneousIdeal.toIdeal y.asHomogeneousIdeal)
[PROOFSTEP]
change b2 ∉ y.asHomogeneousIdeal
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
u1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu1 : x ∈ u1
s1 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u1))
u2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu2 : x ∈ u2
s2 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u2))
eq1 : ↑s1 { val := x, property := memu1 } = ↑s2 { val := x, property := memu2 }
v1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv1 : ↑{ val := x, property := memu1 } ∈ v1
i1 : v1 ⟶ (op u1).unop
j1 : ℕ
a1 : A
a1_mem : a1 ∈ 𝒜 j1
b1 : A
b1_mem : b1 ∈ 𝒜 j1
hs1 :
  ∀ (x : { x // x ∈ v1 }),
    ∃ s_nin,
      (fun x => ↑s1 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u1).unop) }) x)) x =
        Quotient.mk''
          { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
            den_mem := s_nin }
v2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv2 : ↑{ val := x, property := memu2 } ∈ v2
i2 : v2 ⟶ (op u2).unop
j2 : ℕ
a2 : A
a2_mem : a2 ∈ 𝒜 j2
b2 : A
b2_mem : b2 ∈ 𝒜 j2
hs2 :
  ∀ (x : { x // x ∈ v2 }),
    ∃ s_nin,
      (fun x => ↑s2 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u2).unop) }) x)) x =
        Quotient.mk''
          { deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
            den_mem := s_nin }
b1_nin_x : ¬↑{ val := b1, property := b1_mem } ∈ (↑{ val := x, property := memv1 }).asHomogeneousIdeal
eq2 :
  ↑s2 { val := x, property := memu2 } =
    Quotient.mk''
      { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
        den_mem := b1_nin_x }
b2_nin_x : ¬↑{ val := b2, property := b2_mem } ∈ (↑{ val := x, property := memv2 }).asHomogeneousIdeal
c : A
hc : c ∈ Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)
eq3 :
  ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                    den_mem := b2_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                        den_mem := b2_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
              den_mem := b1_nin_x }.num) =
    ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                    den_mem := b1_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                        den_mem := b1_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
              den_mem := b2_nin_x }.num)
y : ↑(ProjectiveSpectrum.top 𝒜)
hy : y ∈ ProjectiveSpectrum.basicOpen 𝒜 b1 ⊓ ProjectiveSpectrum.basicOpen 𝒜 b2 ⊓ ProjectiveSpectrum.basicOpen 𝒜 c
⊢ ¬b2 ∈ y.asHomogeneousIdeal
[PROOFSTEP]
rw [← ProjectiveSpectrum.mem_basicOpen]
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
u1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu1 : x ∈ u1
s1 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u1))
u2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu2 : x ∈ u2
s2 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u2))
eq1 : ↑s1 { val := x, property := memu1 } = ↑s2 { val := x, property := memu2 }
v1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv1 : ↑{ val := x, property := memu1 } ∈ v1
i1 : v1 ⟶ (op u1).unop
j1 : ℕ
a1 : A
a1_mem : a1 ∈ 𝒜 j1
b1 : A
b1_mem : b1 ∈ 𝒜 j1
hs1 :
  ∀ (x : { x // x ∈ v1 }),
    ∃ s_nin,
      (fun x => ↑s1 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u1).unop) }) x)) x =
        Quotient.mk''
          { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
            den_mem := s_nin }
v2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv2 : ↑{ val := x, property := memu2 } ∈ v2
i2 : v2 ⟶ (op u2).unop
j2 : ℕ
a2 : A
a2_mem : a2 ∈ 𝒜 j2
b2 : A
b2_mem : b2 ∈ 𝒜 j2
hs2 :
  ∀ (x : { x // x ∈ v2 }),
    ∃ s_nin,
      (fun x => ↑s2 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u2).unop) }) x)) x =
        Quotient.mk''
          { deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
            den_mem := s_nin }
b1_nin_x : ¬↑{ val := b1, property := b1_mem } ∈ (↑{ val := x, property := memv1 }).asHomogeneousIdeal
eq2 :
  ↑s2 { val := x, property := memu2 } =
    Quotient.mk''
      { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
        den_mem := b1_nin_x }
b2_nin_x : ¬↑{ val := b2, property := b2_mem } ∈ (↑{ val := x, property := memv2 }).asHomogeneousIdeal
c : A
hc : c ∈ Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)
eq3 :
  ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                    den_mem := b2_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                        den_mem := b2_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
              den_mem := b1_nin_x }.num) =
    ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                    den_mem := b1_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                        den_mem := b1_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
              den_mem := b2_nin_x }.num)
y : ↑(ProjectiveSpectrum.top 𝒜)
hy : y ∈ ProjectiveSpectrum.basicOpen 𝒜 b1 ⊓ ProjectiveSpectrum.basicOpen 𝒜 b2 ⊓ ProjectiveSpectrum.basicOpen 𝒜 c
⊢ y ∈ ProjectiveSpectrum.basicOpen 𝒜 b2
[PROOFSTEP]
exact leOfHom (Opens.infLELeft _ _ ≫ Opens.infLERight _ _) hy
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
u1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu1 : x ∈ u1
s1 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u1))
u2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu2 : x ∈ u2
s2 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u2))
eq1 : ↑s1 { val := x, property := memu1 } = ↑s2 { val := x, property := memu2 }
v1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv1 : ↑{ val := x, property := memu1 } ∈ v1
i1 : v1 ⟶ (op u1).unop
j1 : ℕ
a1 : A
a1_mem : a1 ∈ 𝒜 j1
b1 : A
b1_mem : b1 ∈ 𝒜 j1
hs1 :
  ∀ (x : { x // x ∈ v1 }),
    ∃ s_nin,
      (fun x => ↑s1 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u1).unop) }) x)) x =
        Quotient.mk''
          { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
            den_mem := s_nin }
v2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv2 : ↑{ val := x, property := memu2 } ∈ v2
i2 : v2 ⟶ (op u2).unop
j2 : ℕ
a2 : A
a2_mem : a2 ∈ 𝒜 j2
b2 : A
b2_mem : b2 ∈ 𝒜 j2
hs2 :
  ∀ (x : { x // x ∈ v2 }),
    ∃ s_nin,
      (fun x => ↑s2 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u2).unop) }) x)) x =
        Quotient.mk''
          { deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
            den_mem := s_nin }
b1_nin_x : ¬↑{ val := b1, property := b1_mem } ∈ (↑{ val := x, property := memv1 }).asHomogeneousIdeal
eq2 :
  ↑s2 { val := x, property := memu2 } =
    Quotient.mk''
      { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
        den_mem := b1_nin_x }
b2_nin_x : ¬↑{ val := b2, property := b2_mem } ∈ (↑{ val := x, property := memv2 }).asHomogeneousIdeal
c : A
hc : c ∈ Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)
eq3 :
  ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                    den_mem := b2_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                        den_mem := b2_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
              den_mem := b1_nin_x }.num) =
    ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                    den_mem := b1_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                        den_mem := b1_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
              den_mem := b2_nin_x }.num)
⊢ ∀ (y : ↑(ProjectiveSpectrum.top 𝒜))
    (hy : y ∈ ProjectiveSpectrum.basicOpen 𝒜 b1 ⊓ ProjectiveSpectrum.basicOpen 𝒜 b2 ⊓ ProjectiveSpectrum.basicOpen 𝒜 c),
    Localization.mk a1 { val := b1, property := (_ : ¬b1 ∈ y.asHomogeneousIdeal) } =
      Localization.mk a2 { val := b2, property := (_ : ¬b2 ∈ y.asHomogeneousIdeal) }
[PROOFSTEP]
intro y hy
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
u1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu1 : x ∈ u1
s1 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u1))
u2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu2 : x ∈ u2
s2 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u2))
eq1 : ↑s1 { val := x, property := memu1 } = ↑s2 { val := x, property := memu2 }
v1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv1 : ↑{ val := x, property := memu1 } ∈ v1
i1 : v1 ⟶ (op u1).unop
j1 : ℕ
a1 : A
a1_mem : a1 ∈ 𝒜 j1
b1 : A
b1_mem : b1 ∈ 𝒜 j1
hs1 :
  ∀ (x : { x // x ∈ v1 }),
    ∃ s_nin,
      (fun x => ↑s1 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u1).unop) }) x)) x =
        Quotient.mk''
          { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
            den_mem := s_nin }
v2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv2 : ↑{ val := x, property := memu2 } ∈ v2
i2 : v2 ⟶ (op u2).unop
j2 : ℕ
a2 : A
a2_mem : a2 ∈ 𝒜 j2
b2 : A
b2_mem : b2 ∈ 𝒜 j2
hs2 :
  ∀ (x : { x // x ∈ v2 }),
    ∃ s_nin,
      (fun x => ↑s2 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u2).unop) }) x)) x =
        Quotient.mk''
          { deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
            den_mem := s_nin }
b1_nin_x : ¬↑{ val := b1, property := b1_mem } ∈ (↑{ val := x, property := memv1 }).asHomogeneousIdeal
eq2 :
  ↑s2 { val := x, property := memu2 } =
    Quotient.mk''
      { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
        den_mem := b1_nin_x }
b2_nin_x : ¬↑{ val := b2, property := b2_mem } ∈ (↑{ val := x, property := memv2 }).asHomogeneousIdeal
c : A
hc : c ∈ Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)
eq3 :
  ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                    den_mem := b2_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                        den_mem := b2_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
              den_mem := b1_nin_x }.num) =
    ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                    den_mem := b1_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                        den_mem := b1_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
              den_mem := b2_nin_x }.num)
y : ↑(ProjectiveSpectrum.top 𝒜)
hy : y ∈ ProjectiveSpectrum.basicOpen 𝒜 b1 ⊓ ProjectiveSpectrum.basicOpen 𝒜 b2 ⊓ ProjectiveSpectrum.basicOpen 𝒜 c
⊢ Localization.mk a1 { val := b1, property := (_ : ¬b1 ∈ y.asHomogeneousIdeal) } =
    Localization.mk a2 { val := b2, property := (_ : ¬b2 ∈ y.asHomogeneousIdeal) }
[PROOFSTEP]
rw [Localization.mk_eq_mk', IsLocalization.eq]
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
u1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu1 : x ∈ u1
s1 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u1))
u2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu2 : x ∈ u2
s2 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u2))
eq1 : ↑s1 { val := x, property := memu1 } = ↑s2 { val := x, property := memu2 }
v1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv1 : ↑{ val := x, property := memu1 } ∈ v1
i1 : v1 ⟶ (op u1).unop
j1 : ℕ
a1 : A
a1_mem : a1 ∈ 𝒜 j1
b1 : A
b1_mem : b1 ∈ 𝒜 j1
hs1 :
  ∀ (x : { x // x ∈ v1 }),
    ∃ s_nin,
      (fun x => ↑s1 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u1).unop) }) x)) x =
        Quotient.mk''
          { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
            den_mem := s_nin }
v2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv2 : ↑{ val := x, property := memu2 } ∈ v2
i2 : v2 ⟶ (op u2).unop
j2 : ℕ
a2 : A
a2_mem : a2 ∈ 𝒜 j2
b2 : A
b2_mem : b2 ∈ 𝒜 j2
hs2 :
  ∀ (x : { x // x ∈ v2 }),
    ∃ s_nin,
      (fun x => ↑s2 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u2).unop) }) x)) x =
        Quotient.mk''
          { deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
            den_mem := s_nin }
b1_nin_x : ¬↑{ val := b1, property := b1_mem } ∈ (↑{ val := x, property := memv1 }).asHomogeneousIdeal
eq2 :
  ↑s2 { val := x, property := memu2 } =
    Quotient.mk''
      { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
        den_mem := b1_nin_x }
b2_nin_x : ¬↑{ val := b2, property := b2_mem } ∈ (↑{ val := x, property := memv2 }).asHomogeneousIdeal
c : A
hc : c ∈ Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)
eq3 :
  ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                    den_mem := b2_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                        den_mem := b2_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
              den_mem := b1_nin_x }.num) =
    ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                    den_mem := b1_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                        den_mem := b1_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
              den_mem := b2_nin_x }.num)
y : ↑(ProjectiveSpectrum.top 𝒜)
hy : y ∈ ProjectiveSpectrum.basicOpen 𝒜 b1 ⊓ ProjectiveSpectrum.basicOpen 𝒜 b2 ⊓ ProjectiveSpectrum.basicOpen 𝒜 c
⊢ ∃ c_1,
    ↑c_1 * (↑{ val := b2, property := (_ : ¬b2 ∈ y.asHomogeneousIdeal) } * a1) =
      ↑c_1 * (↑{ val := b1, property := (_ : ¬b1 ∈ y.asHomogeneousIdeal) } * a2)
[PROOFSTEP]
exact
  ⟨⟨c,
      show c ∉ y.asHomogeneousIdeal by
        rw [← ProjectiveSpectrum.mem_basicOpen]
        exact leOfHom (Opens.infLERight _ _) hy⟩,
    eq3⟩
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
u1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu1 : x ∈ u1
s1 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u1))
u2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu2 : x ∈ u2
s2 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u2))
eq1 : ↑s1 { val := x, property := memu1 } = ↑s2 { val := x, property := memu2 }
v1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv1 : ↑{ val := x, property := memu1 } ∈ v1
i1 : v1 ⟶ (op u1).unop
j1 : ℕ
a1 : A
a1_mem : a1 ∈ 𝒜 j1
b1 : A
b1_mem : b1 ∈ 𝒜 j1
hs1 :
  ∀ (x : { x // x ∈ v1 }),
    ∃ s_nin,
      (fun x => ↑s1 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u1).unop) }) x)) x =
        Quotient.mk''
          { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
            den_mem := s_nin }
v2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv2 : ↑{ val := x, property := memu2 } ∈ v2
i2 : v2 ⟶ (op u2).unop
j2 : ℕ
a2 : A
a2_mem : a2 ∈ 𝒜 j2
b2 : A
b2_mem : b2 ∈ 𝒜 j2
hs2 :
  ∀ (x : { x // x ∈ v2 }),
    ∃ s_nin,
      (fun x => ↑s2 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u2).unop) }) x)) x =
        Quotient.mk''
          { deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
            den_mem := s_nin }
b1_nin_x : ¬↑{ val := b1, property := b1_mem } ∈ (↑{ val := x, property := memv1 }).asHomogeneousIdeal
eq2 :
  ↑s2 { val := x, property := memu2 } =
    Quotient.mk''
      { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
        den_mem := b1_nin_x }
b2_nin_x : ¬↑{ val := b2, property := b2_mem } ∈ (↑{ val := x, property := memv2 }).asHomogeneousIdeal
c : A
hc : c ∈ Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)
eq3 :
  ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                    den_mem := b2_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                        den_mem := b2_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
              den_mem := b1_nin_x }.num) =
    ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                    den_mem := b1_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                        den_mem := b1_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
              den_mem := b2_nin_x }.num)
y : ↑(ProjectiveSpectrum.top 𝒜)
hy : y ∈ ProjectiveSpectrum.basicOpen 𝒜 b1 ⊓ ProjectiveSpectrum.basicOpen 𝒜 b2 ⊓ ProjectiveSpectrum.basicOpen 𝒜 c
⊢ ¬c ∈ y.asHomogeneousIdeal
[PROOFSTEP]
rw [← ProjectiveSpectrum.mem_basicOpen]
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
u1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu1 : x ∈ u1
s1 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u1))
u2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu2 : x ∈ u2
s2 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u2))
eq1 : ↑s1 { val := x, property := memu1 } = ↑s2 { val := x, property := memu2 }
v1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv1 : ↑{ val := x, property := memu1 } ∈ v1
i1 : v1 ⟶ (op u1).unop
j1 : ℕ
a1 : A
a1_mem : a1 ∈ 𝒜 j1
b1 : A
b1_mem : b1 ∈ 𝒜 j1
hs1 :
  ∀ (x : { x // x ∈ v1 }),
    ∃ s_nin,
      (fun x => ↑s1 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u1).unop) }) x)) x =
        Quotient.mk''
          { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
            den_mem := s_nin }
v2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv2 : ↑{ val := x, property := memu2 } ∈ v2
i2 : v2 ⟶ (op u2).unop
j2 : ℕ
a2 : A
a2_mem : a2 ∈ 𝒜 j2
b2 : A
b2_mem : b2 ∈ 𝒜 j2
hs2 :
  ∀ (x : { x // x ∈ v2 }),
    ∃ s_nin,
      (fun x => ↑s2 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u2).unop) }) x)) x =
        Quotient.mk''
          { deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
            den_mem := s_nin }
b1_nin_x : ¬↑{ val := b1, property := b1_mem } ∈ (↑{ val := x, property := memv1 }).asHomogeneousIdeal
eq2 :
  ↑s2 { val := x, property := memu2 } =
    Quotient.mk''
      { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
        den_mem := b1_nin_x }
b2_nin_x : ¬↑{ val := b2, property := b2_mem } ∈ (↑{ val := x, property := memv2 }).asHomogeneousIdeal
c : A
hc : c ∈ Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)
eq3 :
  ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                    den_mem := b2_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                        den_mem := b2_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
              den_mem := b1_nin_x }.num) =
    ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                    den_mem := b1_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                        den_mem := b1_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
              den_mem := b2_nin_x }.num)
y : ↑(ProjectiveSpectrum.top 𝒜)
hy : y ∈ ProjectiveSpectrum.basicOpen 𝒜 b1 ⊓ ProjectiveSpectrum.basicOpen 𝒜 b2 ⊓ ProjectiveSpectrum.basicOpen 𝒜 c
⊢ y ∈ ProjectiveSpectrum.basicOpen 𝒜 c
[PROOFSTEP]
exact leOfHom (Opens.infLERight _ _) hy
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.mk
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
u1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu1 : x ∈ u1
s1 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u1))
u2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu2 : x ∈ u2
s2 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u2))
eq1 : ↑s1 { val := x, property := memu1 } = ↑s2 { val := x, property := memu2 }
v1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv1 : ↑{ val := x, property := memu1 } ∈ v1
i1 : v1 ⟶ (op u1).unop
j1 : ℕ
a1 : A
a1_mem : a1 ∈ 𝒜 j1
b1 : A
b1_mem : b1 ∈ 𝒜 j1
hs1 :
  ∀ (x : { x // x ∈ v1 }),
    ∃ s_nin,
      (fun x => ↑s1 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u1).unop) }) x)) x =
        Quotient.mk''
          { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
            den_mem := s_nin }
v2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv2 : ↑{ val := x, property := memu2 } ∈ v2
i2 : v2 ⟶ (op u2).unop
j2 : ℕ
a2 : A
a2_mem : a2 ∈ 𝒜 j2
b2 : A
b2_mem : b2 ∈ 𝒜 j2
hs2 :
  ∀ (x : { x // x ∈ v2 }),
    ∃ s_nin,
      (fun x => ↑s2 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u2).unop) }) x)) x =
        Quotient.mk''
          { deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
            den_mem := s_nin }
b1_nin_x : ¬↑{ val := b1, property := b1_mem } ∈ (↑{ val := x, property := memv1 }).asHomogeneousIdeal
eq2 :
  ↑s2 { val := x, property := memu2 } =
    Quotient.mk''
      { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
        den_mem := b1_nin_x }
b2_nin_x : ¬↑{ val := b2, property := b2_mem } ∈ (↑{ val := x, property := memv2 }).asHomogeneousIdeal
c : A
hc : c ∈ Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)
eq3 :
  ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                    den_mem := b2_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                        den_mem := b2_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
              den_mem := b1_nin_x }.num) =
    ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                    den_mem := b1_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                        den_mem := b1_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
              den_mem := b2_nin_x }.num)
eq3' :
  ∀ (y : ↑(ProjectiveSpectrum.top 𝒜))
    (hy : y ∈ ProjectiveSpectrum.basicOpen 𝒜 b1 ⊓ ProjectiveSpectrum.basicOpen 𝒜 b2 ⊓ ProjectiveSpectrum.basicOpen 𝒜 c),
    Localization.mk a1 { val := b1, property := (_ : ¬b1 ∈ y.asHomogeneousIdeal) } =
      Localization.mk a2 { val := b2, property := (_ : ¬b2 ∈ y.asHomogeneousIdeal) }
⊢ ↑(Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) { val := x, property := memu1 }) s1 =
    ↑(Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) { val := x, property := memu2 }) s2
[PROOFSTEP]
refine'
  Presheaf.germ_ext (Proj.structureSheaf 𝒜).1
    (ProjectiveSpectrum.basicOpen _ b1 ⊓ ProjectiveSpectrum.basicOpen _ b2 ⊓ ProjectiveSpectrum.basicOpen _ c ⊓ v1 ⊓ v2)
    ⟨⟨⟨⟨b1_nin_x, b2_nin_x⟩, hc⟩, memv1⟩, memv2⟩ (Opens.infLELeft _ _ ≫ Opens.infLERight _ _ ≫ i1)
    (Opens.infLERight _ _ ≫ i2) _
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.mk
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
u1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu1 : x ∈ u1
s1 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u1))
u2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu2 : x ∈ u2
s2 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u2))
eq1 : ↑s1 { val := x, property := memu1 } = ↑s2 { val := x, property := memu2 }
v1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv1 : ↑{ val := x, property := memu1 } ∈ v1
i1 : v1 ⟶ (op u1).unop
j1 : ℕ
a1 : A
a1_mem : a1 ∈ 𝒜 j1
b1 : A
b1_mem : b1 ∈ 𝒜 j1
hs1 :
  ∀ (x : { x // x ∈ v1 }),
    ∃ s_nin,
      (fun x => ↑s1 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u1).unop) }) x)) x =
        Quotient.mk''
          { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
            den_mem := s_nin }
v2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv2 : ↑{ val := x, property := memu2 } ∈ v2
i2 : v2 ⟶ (op u2).unop
j2 : ℕ
a2 : A
a2_mem : a2 ∈ 𝒜 j2
b2 : A
b2_mem : b2 ∈ 𝒜 j2
hs2 :
  ∀ (x : { x // x ∈ v2 }),
    ∃ s_nin,
      (fun x => ↑s2 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u2).unop) }) x)) x =
        Quotient.mk''
          { deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
            den_mem := s_nin }
b1_nin_x : ¬↑{ val := b1, property := b1_mem } ∈ (↑{ val := x, property := memv1 }).asHomogeneousIdeal
eq2 :
  ↑s2 { val := x, property := memu2 } =
    Quotient.mk''
      { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
        den_mem := b1_nin_x }
b2_nin_x : ¬↑{ val := b2, property := b2_mem } ∈ (↑{ val := x, property := memv2 }).asHomogeneousIdeal
c : A
hc : c ∈ Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)
eq3 :
  ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                    den_mem := b2_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                        den_mem := b2_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
              den_mem := b1_nin_x }.num) =
    ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                    den_mem := b1_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                        den_mem := b1_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
              den_mem := b2_nin_x }.num)
eq3' :
  ∀ (y : ↑(ProjectiveSpectrum.top 𝒜))
    (hy : y ∈ ProjectiveSpectrum.basicOpen 𝒜 b1 ⊓ ProjectiveSpectrum.basicOpen 𝒜 b2 ⊓ ProjectiveSpectrum.basicOpen 𝒜 c),
    Localization.mk a1 { val := b1, property := (_ : ¬b1 ∈ y.asHomogeneousIdeal) } =
      Localization.mk a2 { val := b2, property := (_ : ¬b2 ∈ y.asHomogeneousIdeal) }
⊢ ↑((Proj.structureSheaf 𝒜).val.map
          (infLELeft
                (ProjectiveSpectrum.basicOpen 𝒜 b1 ⊓ ProjectiveSpectrum.basicOpen 𝒜 b2 ⊓
                    ProjectiveSpectrum.basicOpen 𝒜 c ⊓
                  v1)
                v2 ≫
              infLERight
                  (ProjectiveSpectrum.basicOpen 𝒜 b1 ⊓ ProjectiveSpectrum.basicOpen 𝒜 b2 ⊓
                    ProjectiveSpectrum.basicOpen 𝒜 c)
                  v1 ≫
                i1).op)
      s1 =
    ↑((Proj.structureSheaf 𝒜).val.map
          (infLERight
                (ProjectiveSpectrum.basicOpen 𝒜 b1 ⊓ ProjectiveSpectrum.basicOpen 𝒜 b2 ⊓
                    ProjectiveSpectrum.basicOpen 𝒜 c ⊓
                  v1)
                v2 ≫
              i2).op)
      s2
[PROOFSTEP]
rw [Subtype.ext_iff_val]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.mk
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
u1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu1 : x ∈ u1
s1 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u1))
u2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu2 : x ∈ u2
s2 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u2))
eq1 : ↑s1 { val := x, property := memu1 } = ↑s2 { val := x, property := memu2 }
v1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv1 : ↑{ val := x, property := memu1 } ∈ v1
i1 : v1 ⟶ (op u1).unop
j1 : ℕ
a1 : A
a1_mem : a1 ∈ 𝒜 j1
b1 : A
b1_mem : b1 ∈ 𝒜 j1
hs1 :
  ∀ (x : { x // x ∈ v1 }),
    ∃ s_nin,
      (fun x => ↑s1 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u1).unop) }) x)) x =
        Quotient.mk''
          { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
            den_mem := s_nin }
v2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv2 : ↑{ val := x, property := memu2 } ∈ v2
i2 : v2 ⟶ (op u2).unop
j2 : ℕ
a2 : A
a2_mem : a2 ∈ 𝒜 j2
b2 : A
b2_mem : b2 ∈ 𝒜 j2
hs2 :
  ∀ (x : { x // x ∈ v2 }),
    ∃ s_nin,
      (fun x => ↑s2 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u2).unop) }) x)) x =
        Quotient.mk''
          { deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
            den_mem := s_nin }
b1_nin_x : ¬↑{ val := b1, property := b1_mem } ∈ (↑{ val := x, property := memv1 }).asHomogeneousIdeal
eq2 :
  ↑s2 { val := x, property := memu2 } =
    Quotient.mk''
      { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
        den_mem := b1_nin_x }
b2_nin_x : ¬↑{ val := b2, property := b2_mem } ∈ (↑{ val := x, property := memv2 }).asHomogeneousIdeal
c : A
hc : c ∈ Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)
eq3 :
  ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                    den_mem := b2_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                        den_mem := b2_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
              den_mem := b1_nin_x }.num) =
    ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                    den_mem := b1_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                        den_mem := b1_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
              den_mem := b2_nin_x }.num)
eq3' :
  ∀ (y : ↑(ProjectiveSpectrum.top 𝒜))
    (hy : y ∈ ProjectiveSpectrum.basicOpen 𝒜 b1 ⊓ ProjectiveSpectrum.basicOpen 𝒜 b2 ⊓ ProjectiveSpectrum.basicOpen 𝒜 c),
    Localization.mk a1 { val := b1, property := (_ : ¬b1 ∈ y.asHomogeneousIdeal) } =
      Localization.mk a2 { val := b2, property := (_ : ¬b2 ∈ y.asHomogeneousIdeal) }
⊢ ↑(↑((Proj.structureSheaf 𝒜).val.map
            (infLELeft
                  (ProjectiveSpectrum.basicOpen 𝒜 b1 ⊓ ProjectiveSpectrum.basicOpen 𝒜 b2 ⊓
                      ProjectiveSpectrum.basicOpen 𝒜 c ⊓
                    v1)
                  v2 ≫
                infLERight
                    (ProjectiveSpectrum.basicOpen 𝒜 b1 ⊓ ProjectiveSpectrum.basicOpen 𝒜 b2 ⊓
                      ProjectiveSpectrum.basicOpen 𝒜 c)
                    v1 ≫
                  i1).op)
        s1) =
    ↑(↑((Proj.structureSheaf 𝒜).val.map
            (infLERight
                  (ProjectiveSpectrum.basicOpen 𝒜 b1 ⊓ ProjectiveSpectrum.basicOpen 𝒜 b2 ⊓
                      ProjectiveSpectrum.basicOpen 𝒜 c ⊓
                    v1)
                  v2 ≫
                i2).op)
        s2)
[PROOFSTEP]
ext1 y
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.mk.h
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
u1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu1 : x ∈ u1
s1 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u1))
u2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu2 : x ∈ u2
s2 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u2))
eq1 : ↑s1 { val := x, property := memu1 } = ↑s2 { val := x, property := memu2 }
v1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv1 : ↑{ val := x, property := memu1 } ∈ v1
i1 : v1 ⟶ (op u1).unop
j1 : ℕ
a1 : A
a1_mem : a1 ∈ 𝒜 j1
b1 : A
b1_mem : b1 ∈ 𝒜 j1
hs1 :
  ∀ (x : { x // x ∈ v1 }),
    ∃ s_nin,
      (fun x => ↑s1 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u1).unop) }) x)) x =
        Quotient.mk''
          { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
            den_mem := s_nin }
v2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv2 : ↑{ val := x, property := memu2 } ∈ v2
i2 : v2 ⟶ (op u2).unop
j2 : ℕ
a2 : A
a2_mem : a2 ∈ 𝒜 j2
b2 : A
b2_mem : b2 ∈ 𝒜 j2
hs2 :
  ∀ (x : { x // x ∈ v2 }),
    ∃ s_nin,
      (fun x => ↑s2 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u2).unop) }) x)) x =
        Quotient.mk''
          { deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
            den_mem := s_nin }
b1_nin_x : ¬↑{ val := b1, property := b1_mem } ∈ (↑{ val := x, property := memv1 }).asHomogeneousIdeal
eq2 :
  ↑s2 { val := x, property := memu2 } =
    Quotient.mk''
      { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
        den_mem := b1_nin_x }
b2_nin_x : ¬↑{ val := b2, property := b2_mem } ∈ (↑{ val := x, property := memv2 }).asHomogeneousIdeal
c : A
hc : c ∈ Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)
eq3 :
  ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                    den_mem := b2_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                        den_mem := b2_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
              den_mem := b1_nin_x }.num) =
    ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                    den_mem := b1_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                        den_mem := b1_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
              den_mem := b2_nin_x }.num)
eq3' :
  ∀ (y : ↑(ProjectiveSpectrum.top 𝒜))
    (hy : y ∈ ProjectiveSpectrum.basicOpen 𝒜 b1 ⊓ ProjectiveSpectrum.basicOpen 𝒜 b2 ⊓ ProjectiveSpectrum.basicOpen 𝒜 c),
    Localization.mk a1 { val := b1, property := (_ : ¬b1 ∈ y.asHomogeneousIdeal) } =
      Localization.mk a2 { val := b2, property := (_ : ¬b2 ∈ y.asHomogeneousIdeal) }
y :
  { x //
    x ∈
      (op
          (ProjectiveSpectrum.basicOpen 𝒜 b1 ⊓ ProjectiveSpectrum.basicOpen 𝒜 b2 ⊓ ProjectiveSpectrum.basicOpen 𝒜 c ⊓
              v1 ⊓
            v2)).unop }
⊢ ↑(↑((Proj.structureSheaf 𝒜).val.map
              (infLELeft
                    (ProjectiveSpectrum.basicOpen 𝒜 b1 ⊓ ProjectiveSpectrum.basicOpen 𝒜 b2 ⊓
                        ProjectiveSpectrum.basicOpen 𝒜 c ⊓
                      v1)
                    v2 ≫
                  infLERight
                      (ProjectiveSpectrum.basicOpen 𝒜 b1 ⊓ ProjectiveSpectrum.basicOpen 𝒜 b2 ⊓
                        ProjectiveSpectrum.basicOpen 𝒜 c)
                      v1 ≫
                    i1).op)
          s1)
      y =
    ↑(↑((Proj.structureSheaf 𝒜).val.map
              (infLERight
                    (ProjectiveSpectrum.basicOpen 𝒜 b1 ⊓ ProjectiveSpectrum.basicOpen 𝒜 b2 ⊓
                        ProjectiveSpectrum.basicOpen 𝒜 c ⊓
                      v1)
                    v2 ≫
                  i2).op)
          s2)
      y
[PROOFSTEP]
simp only [res_apply]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.mk.h
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
u1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu1 : x ∈ u1
s1 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u1))
u2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu2 : x ∈ u2
s2 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u2))
eq1 : ↑s1 { val := x, property := memu1 } = ↑s2 { val := x, property := memu2 }
v1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv1 : ↑{ val := x, property := memu1 } ∈ v1
i1 : v1 ⟶ (op u1).unop
j1 : ℕ
a1 : A
a1_mem : a1 ∈ 𝒜 j1
b1 : A
b1_mem : b1 ∈ 𝒜 j1
hs1 :
  ∀ (x : { x // x ∈ v1 }),
    ∃ s_nin,
      (fun x => ↑s1 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u1).unop) }) x)) x =
        Quotient.mk''
          { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
            den_mem := s_nin }
v2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv2 : ↑{ val := x, property := memu2 } ∈ v2
i2 : v2 ⟶ (op u2).unop
j2 : ℕ
a2 : A
a2_mem : a2 ∈ 𝒜 j2
b2 : A
b2_mem : b2 ∈ 𝒜 j2
hs2 :
  ∀ (x : { x // x ∈ v2 }),
    ∃ s_nin,
      (fun x => ↑s2 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u2).unop) }) x)) x =
        Quotient.mk''
          { deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
            den_mem := s_nin }
b1_nin_x : ¬↑{ val := b1, property := b1_mem } ∈ (↑{ val := x, property := memv1 }).asHomogeneousIdeal
eq2 :
  ↑s2 { val := x, property := memu2 } =
    Quotient.mk''
      { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
        den_mem := b1_nin_x }
b2_nin_x : ¬↑{ val := b2, property := b2_mem } ∈ (↑{ val := x, property := memv2 }).asHomogeneousIdeal
c : A
hc : c ∈ Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)
eq3 :
  ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                    den_mem := b2_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                        den_mem := b2_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
              den_mem := b1_nin_x }.num) =
    ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                    den_mem := b1_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                        den_mem := b1_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
              den_mem := b2_nin_x }.num)
eq3' :
  ∀ (y : ↑(ProjectiveSpectrum.top 𝒜))
    (hy : y ∈ ProjectiveSpectrum.basicOpen 𝒜 b1 ⊓ ProjectiveSpectrum.basicOpen 𝒜 b2 ⊓ ProjectiveSpectrum.basicOpen 𝒜 c),
    Localization.mk a1 { val := b1, property := (_ : ¬b1 ∈ y.asHomogeneousIdeal) } =
      Localization.mk a2 { val := b2, property := (_ : ¬b2 ∈ y.asHomogeneousIdeal) }
y :
  { x //
    x ∈
      (op
          (ProjectiveSpectrum.basicOpen 𝒜 b1 ⊓ ProjectiveSpectrum.basicOpen 𝒜 b2 ⊓ ProjectiveSpectrum.basicOpen 𝒜 c ⊓
              v1 ⊓
            v2)).unop }
⊢ ↑s1 { val := ↑y, property := (_ : ↑y ∈ ↑(op u1).unop) } = ↑s2 { val := ↑y, property := (_ : ↑y ∈ ↑(op u2).unop) }
[PROOFSTEP]
obtain ⟨b1_nin_y, eq6⟩ := hs1 ⟨_, leOfHom (Opens.infLELeft _ _ ≫ Opens.infLERight _ _) y.2⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.mk.h.intro
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
u1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu1 : x ∈ u1
s1 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u1))
u2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu2 : x ∈ u2
s2 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u2))
eq1 : ↑s1 { val := x, property := memu1 } = ↑s2 { val := x, property := memu2 }
v1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv1 : ↑{ val := x, property := memu1 } ∈ v1
i1 : v1 ⟶ (op u1).unop
j1 : ℕ
a1 : A
a1_mem : a1 ∈ 𝒜 j1
b1 : A
b1_mem : b1 ∈ 𝒜 j1
hs1 :
  ∀ (x : { x // x ∈ v1 }),
    ∃ s_nin,
      (fun x => ↑s1 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u1).unop) }) x)) x =
        Quotient.mk''
          { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
            den_mem := s_nin }
v2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv2 : ↑{ val := x, property := memu2 } ∈ v2
i2 : v2 ⟶ (op u2).unop
j2 : ℕ
a2 : A
a2_mem : a2 ∈ 𝒜 j2
b2 : A
b2_mem : b2 ∈ 𝒜 j2
hs2 :
  ∀ (x : { x // x ∈ v2 }),
    ∃ s_nin,
      (fun x => ↑s2 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u2).unop) }) x)) x =
        Quotient.mk''
          { deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
            den_mem := s_nin }
b1_nin_x : ¬↑{ val := b1, property := b1_mem } ∈ (↑{ val := x, property := memv1 }).asHomogeneousIdeal
eq2 :
  ↑s2 { val := x, property := memu2 } =
    Quotient.mk''
      { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
        den_mem := b1_nin_x }
b2_nin_x : ¬↑{ val := b2, property := b2_mem } ∈ (↑{ val := x, property := memv2 }).asHomogeneousIdeal
c : A
hc : c ∈ Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)
eq3 :
  ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                    den_mem := b2_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                        den_mem := b2_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
              den_mem := b1_nin_x }.num) =
    ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                    den_mem := b1_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                        den_mem := b1_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
              den_mem := b2_nin_x }.num)
eq3' :
  ∀ (y : ↑(ProjectiveSpectrum.top 𝒜))
    (hy : y ∈ ProjectiveSpectrum.basicOpen 𝒜 b1 ⊓ ProjectiveSpectrum.basicOpen 𝒜 b2 ⊓ ProjectiveSpectrum.basicOpen 𝒜 c),
    Localization.mk a1 { val := b1, property := (_ : ¬b1 ∈ y.asHomogeneousIdeal) } =
      Localization.mk a2 { val := b2, property := (_ : ¬b2 ∈ y.asHomogeneousIdeal) }
y :
  { x //
    x ∈
      (op
          (ProjectiveSpectrum.basicOpen 𝒜 b1 ⊓ ProjectiveSpectrum.basicOpen 𝒜 b2 ⊓ ProjectiveSpectrum.basicOpen 𝒜 c ⊓
              v1 ⊓
            v2)).unop }
b1_nin_y : ¬↑{ val := b1, property := b1_mem } ∈ (↑{ val := ↑y, property := (_ : ↑y ∈ ↑v1) }).asHomogeneousIdeal
eq6 :
  (fun x => ↑s1 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u1).unop) }) x))
      { val := ↑y, property := (_ : ↑y ∈ ↑v1) } =
    Quotient.mk''
      { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
        den_mem := b1_nin_y }
⊢ ↑s1 { val := ↑y, property := (_ : ↑y ∈ ↑(op u1).unop) } = ↑s2 { val := ↑y, property := (_ : ↑y ∈ ↑(op u2).unop) }
[PROOFSTEP]
obtain ⟨b2_nin_y, eq7⟩ := hs2 ⟨_, leOfHom (Opens.infLERight _ _) y.2⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.mk.h.intro.intro
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
u1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu1 : x ∈ u1
s1 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u1))
u2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu2 : x ∈ u2
s2 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u2))
eq1 : ↑s1 { val := x, property := memu1 } = ↑s2 { val := x, property := memu2 }
v1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv1 : ↑{ val := x, property := memu1 } ∈ v1
i1 : v1 ⟶ (op u1).unop
j1 : ℕ
a1 : A
a1_mem : a1 ∈ 𝒜 j1
b1 : A
b1_mem : b1 ∈ 𝒜 j1
hs1 :
  ∀ (x : { x // x ∈ v1 }),
    ∃ s_nin,
      (fun x => ↑s1 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u1).unop) }) x)) x =
        Quotient.mk''
          { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
            den_mem := s_nin }
v2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv2 : ↑{ val := x, property := memu2 } ∈ v2
i2 : v2 ⟶ (op u2).unop
j2 : ℕ
a2 : A
a2_mem : a2 ∈ 𝒜 j2
b2 : A
b2_mem : b2 ∈ 𝒜 j2
hs2 :
  ∀ (x : { x // x ∈ v2 }),
    ∃ s_nin,
      (fun x => ↑s2 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u2).unop) }) x)) x =
        Quotient.mk''
          { deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
            den_mem := s_nin }
b1_nin_x : ¬↑{ val := b1, property := b1_mem } ∈ (↑{ val := x, property := memv1 }).asHomogeneousIdeal
eq2 :
  ↑s2 { val := x, property := memu2 } =
    Quotient.mk''
      { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
        den_mem := b1_nin_x }
b2_nin_x : ¬↑{ val := b2, property := b2_mem } ∈ (↑{ val := x, property := memv2 }).asHomogeneousIdeal
c : A
hc : c ∈ Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)
eq3 :
  ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                    den_mem := b2_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                        den_mem := b2_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
              den_mem := b1_nin_x }.num) =
    ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                    den_mem := b1_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                        den_mem := b1_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
              den_mem := b2_nin_x }.num)
eq3' :
  ∀ (y : ↑(ProjectiveSpectrum.top 𝒜))
    (hy : y ∈ ProjectiveSpectrum.basicOpen 𝒜 b1 ⊓ ProjectiveSpectrum.basicOpen 𝒜 b2 ⊓ ProjectiveSpectrum.basicOpen 𝒜 c),
    Localization.mk a1 { val := b1, property := (_ : ¬b1 ∈ y.asHomogeneousIdeal) } =
      Localization.mk a2 { val := b2, property := (_ : ¬b2 ∈ y.asHomogeneousIdeal) }
y :
  { x //
    x ∈
      (op
          (ProjectiveSpectrum.basicOpen 𝒜 b1 ⊓ ProjectiveSpectrum.basicOpen 𝒜 b2 ⊓ ProjectiveSpectrum.basicOpen 𝒜 c ⊓
              v1 ⊓
            v2)).unop }
b1_nin_y : ¬↑{ val := b1, property := b1_mem } ∈ (↑{ val := ↑y, property := (_ : ↑y ∈ ↑v1) }).asHomogeneousIdeal
eq6 :
  (fun x => ↑s1 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u1).unop) }) x))
      { val := ↑y, property := (_ : ↑y ∈ ↑v1) } =
    Quotient.mk''
      { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
        den_mem := b1_nin_y }
b2_nin_y : ¬↑{ val := b2, property := b2_mem } ∈ (↑{ val := ↑y, property := (_ : ↑y ∈ ↑v2) }).asHomogeneousIdeal
eq7 :
  (fun x => ↑s2 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u2).unop) }) x))
      { val := ↑y, property := (_ : ↑y ∈ ↑v2) } =
    Quotient.mk''
      { deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
        den_mem := b2_nin_y }
⊢ ↑s1 { val := ↑y, property := (_ : ↑y ∈ ↑(op u1).unop) } = ↑s2 { val := ↑y, property := (_ : ↑y ∈ ↑(op u2).unop) }
[PROOFSTEP]
simp only at eq6 eq7
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.mk.h.intro.intro
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
u1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu1 : x ∈ u1
s1 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u1))
u2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu2 : x ∈ u2
s2 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u2))
eq1 : ↑s1 { val := x, property := memu1 } = ↑s2 { val := x, property := memu2 }
v1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv1 : ↑{ val := x, property := memu1 } ∈ v1
i1 : v1 ⟶ (op u1).unop
j1 : ℕ
a1 : A
a1_mem : a1 ∈ 𝒜 j1
b1 : A
b1_mem : b1 ∈ 𝒜 j1
hs1 :
  ∀ (x : { x // x ∈ v1 }),
    ∃ s_nin,
      (fun x => ↑s1 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u1).unop) }) x)) x =
        Quotient.mk''
          { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
            den_mem := s_nin }
v2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv2 : ↑{ val := x, property := memu2 } ∈ v2
i2 : v2 ⟶ (op u2).unop
j2 : ℕ
a2 : A
a2_mem : a2 ∈ 𝒜 j2
b2 : A
b2_mem : b2 ∈ 𝒜 j2
hs2 :
  ∀ (x : { x // x ∈ v2 }),
    ∃ s_nin,
      (fun x => ↑s2 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u2).unop) }) x)) x =
        Quotient.mk''
          { deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
            den_mem := s_nin }
b1_nin_x : ¬↑{ val := b1, property := b1_mem } ∈ (↑{ val := x, property := memv1 }).asHomogeneousIdeal
eq2 :
  ↑s2 { val := x, property := memu2 } =
    Quotient.mk''
      { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
        den_mem := b1_nin_x }
b2_nin_x : ¬↑{ val := b2, property := b2_mem } ∈ (↑{ val := x, property := memv2 }).asHomogeneousIdeal
c : A
hc : c ∈ Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)
eq3 :
  ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                    den_mem := b2_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                        den_mem := b2_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
              den_mem := b1_nin_x }.num) =
    ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                    den_mem := b1_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                        den_mem := b1_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
              den_mem := b2_nin_x }.num)
eq3' :
  ∀ (y : ↑(ProjectiveSpectrum.top 𝒜))
    (hy : y ∈ ProjectiveSpectrum.basicOpen 𝒜 b1 ⊓ ProjectiveSpectrum.basicOpen 𝒜 b2 ⊓ ProjectiveSpectrum.basicOpen 𝒜 c),
    Localization.mk a1 { val := b1, property := (_ : ¬b1 ∈ y.asHomogeneousIdeal) } =
      Localization.mk a2 { val := b2, property := (_ : ¬b2 ∈ y.asHomogeneousIdeal) }
y :
  { x //
    x ∈
      (op
          (ProjectiveSpectrum.basicOpen 𝒜 b1 ⊓ ProjectiveSpectrum.basicOpen 𝒜 b2 ⊓ ProjectiveSpectrum.basicOpen 𝒜 c ⊓
              v1 ⊓
            v2)).unop }
b1_nin_y : ¬↑{ val := b1, property := b1_mem } ∈ (↑{ val := ↑y, property := (_ : ↑y ∈ ↑v1) }).asHomogeneousIdeal
eq6 :
  ↑s1 { val := ↑y, property := (_ : ↑{ val := ↑y, property := (_ : ↑y ∈ ↑v1) } ∈ ↑(op u1).unop) } =
    Quotient.mk''
      { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
        den_mem := b1_nin_y }
b2_nin_y : ¬↑{ val := b2, property := b2_mem } ∈ (↑{ val := ↑y, property := (_ : ↑y ∈ ↑v2) }).asHomogeneousIdeal
eq7 :
  ↑s2 { val := ↑y, property := (_ : ↑{ val := ↑y, property := (_ : ↑y ∈ ↑v2) } ∈ ↑(op u2).unop) } =
    Quotient.mk''
      { deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
        den_mem := b2_nin_y }
⊢ ↑s1 { val := ↑y, property := (_ : ↑y ∈ ↑(op u1).unop) } = ↑s2 { val := ↑y, property := (_ : ↑y ∈ ↑(op u2).unop) }
[PROOFSTEP]
erw [eq6, eq7, Quotient.eq'']
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.mk.h.intro.intro
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
u1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu1 : x ∈ u1
s1 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u1))
u2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu2 : x ∈ u2
s2 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u2))
eq1 : ↑s1 { val := x, property := memu1 } = ↑s2 { val := x, property := memu2 }
v1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv1 : ↑{ val := x, property := memu1 } ∈ v1
i1 : v1 ⟶ (op u1).unop
j1 : ℕ
a1 : A
a1_mem : a1 ∈ 𝒜 j1
b1 : A
b1_mem : b1 ∈ 𝒜 j1
hs1 :
  ∀ (x : { x // x ∈ v1 }),
    ∃ s_nin,
      (fun x => ↑s1 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u1).unop) }) x)) x =
        Quotient.mk''
          { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
            den_mem := s_nin }
v2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv2 : ↑{ val := x, property := memu2 } ∈ v2
i2 : v2 ⟶ (op u2).unop
j2 : ℕ
a2 : A
a2_mem : a2 ∈ 𝒜 j2
b2 : A
b2_mem : b2 ∈ 𝒜 j2
hs2 :
  ∀ (x : { x // x ∈ v2 }),
    ∃ s_nin,
      (fun x => ↑s2 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u2).unop) }) x)) x =
        Quotient.mk''
          { deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
            den_mem := s_nin }
b1_nin_x : ¬↑{ val := b1, property := b1_mem } ∈ (↑{ val := x, property := memv1 }).asHomogeneousIdeal
eq2 :
  ↑s2 { val := x, property := memu2 } =
    Quotient.mk''
      { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
        den_mem := b1_nin_x }
b2_nin_x : ¬↑{ val := b2, property := b2_mem } ∈ (↑{ val := x, property := memv2 }).asHomogeneousIdeal
c : A
hc : c ∈ Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)
eq3 :
  ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                    den_mem := b2_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                        den_mem := b2_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
              den_mem := b1_nin_x }.num) =
    ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                    den_mem := b1_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                        den_mem := b1_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
              den_mem := b2_nin_x }.num)
eq3' :
  ∀ (y : ↑(ProjectiveSpectrum.top 𝒜))
    (hy : y ∈ ProjectiveSpectrum.basicOpen 𝒜 b1 ⊓ ProjectiveSpectrum.basicOpen 𝒜 b2 ⊓ ProjectiveSpectrum.basicOpen 𝒜 c),
    Localization.mk a1 { val := b1, property := (_ : ¬b1 ∈ y.asHomogeneousIdeal) } =
      Localization.mk a2 { val := b2, property := (_ : ¬b2 ∈ y.asHomogeneousIdeal) }
y :
  { x //
    x ∈
      (op
          (ProjectiveSpectrum.basicOpen 𝒜 b1 ⊓ ProjectiveSpectrum.basicOpen 𝒜 b2 ⊓ ProjectiveSpectrum.basicOpen 𝒜 c ⊓
              v1 ⊓
            v2)).unop }
b1_nin_y : ¬↑{ val := b1, property := b1_mem } ∈ (↑{ val := ↑y, property := (_ : ↑y ∈ ↑v1) }).asHomogeneousIdeal
eq6 :
  ↑s1 { val := ↑y, property := (_ : ↑{ val := ↑y, property := (_ : ↑y ∈ ↑v1) } ∈ ↑(op u1).unop) } =
    Quotient.mk''
      { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
        den_mem := b1_nin_y }
b2_nin_y : ¬↑{ val := b2, property := b2_mem } ∈ (↑{ val := ↑y, property := (_ : ↑y ∈ ↑v2) }).asHomogeneousIdeal
eq7 :
  ↑s2 { val := ↑y, property := (_ : ↑{ val := ↑y, property := (_ : ↑y ∈ ↑v2) } ∈ ↑(op u2).unop) } =
    Quotient.mk''
      { deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
        den_mem := b2_nin_y }
⊢ Setoid.r
    { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
      den_mem := b1_nin_y }
    { deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
      den_mem := b2_nin_y }
[PROOFSTEP]
change Localization.mk _ _ = Localization.mk _ _
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.mk.h.intro.intro
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
u1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu1 : x ∈ u1
s1 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u1))
u2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memu2 : x ∈ u2
s2 : (forget CommRingCat).obj ((Sheaf.presheaf (Proj.structureSheaf 𝒜)).obj (op u2))
eq1 : ↑s1 { val := x, property := memu1 } = ↑s2 { val := x, property := memu2 }
v1 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv1 : ↑{ val := x, property := memu1 } ∈ v1
i1 : v1 ⟶ (op u1).unop
j1 : ℕ
a1 : A
a1_mem : a1 ∈ 𝒜 j1
b1 : A
b1_mem : b1 ∈ 𝒜 j1
hs1 :
  ∀ (x : { x // x ∈ v1 }),
    ∃ s_nin,
      (fun x => ↑s1 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u1).unop) }) x)) x =
        Quotient.mk''
          { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
            den_mem := s_nin }
v2 : Opens ↑(ProjectiveSpectrum.top 𝒜)
memv2 : ↑{ val := x, property := memu2 } ∈ v2
i2 : v2 ⟶ (op u2).unop
j2 : ℕ
a2 : A
a2_mem : a2 ∈ 𝒜 j2
b2 : A
b2_mem : b2 ∈ 𝒜 j2
hs2 :
  ∀ (x : { x // x ∈ v2 }),
    ∃ s_nin,
      (fun x => ↑s2 ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op u2).unop) }) x)) x =
        Quotient.mk''
          { deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
            den_mem := s_nin }
b1_nin_x : ¬↑{ val := b1, property := b1_mem } ∈ (↑{ val := x, property := memv1 }).asHomogeneousIdeal
eq2 :
  ↑s2 { val := x, property := memu2 } =
    Quotient.mk''
      { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
        den_mem := b1_nin_x }
b2_nin_x : ¬↑{ val := b2, property := b2_mem } ∈ (↑{ val := x, property := memv2 }).asHomogeneousIdeal
c : A
hc : c ∈ Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)
eq3 :
  ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                    den_mem := b2_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                        den_mem := b2_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
              den_mem := b1_nin_x }.num) =
    ↑{ val := c, property := hc } *
      (↑{
            val :=
              ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                    den_mem := b1_nin_x }.den,
            property :=
              (_ :
                ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                        den_mem := b1_nin_x }.den ∈
                  Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) } *
        ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
              den_mem := b2_nin_x }.num)
eq3' :
  ∀ (y : ↑(ProjectiveSpectrum.top 𝒜))
    (hy : y ∈ ProjectiveSpectrum.basicOpen 𝒜 b1 ⊓ ProjectiveSpectrum.basicOpen 𝒜 b2 ⊓ ProjectiveSpectrum.basicOpen 𝒜 c),
    Localization.mk a1 { val := b1, property := (_ : ¬b1 ∈ y.asHomogeneousIdeal) } =
      Localization.mk a2 { val := b2, property := (_ : ¬b2 ∈ y.asHomogeneousIdeal) }
y :
  { x //
    x ∈
      (op
          (ProjectiveSpectrum.basicOpen 𝒜 b1 ⊓ ProjectiveSpectrum.basicOpen 𝒜 b2 ⊓ ProjectiveSpectrum.basicOpen 𝒜 c ⊓
              v1 ⊓
            v2)).unop }
b1_nin_y : ¬↑{ val := b1, property := b1_mem } ∈ (↑{ val := ↑y, property := (_ : ↑y ∈ ↑v1) }).asHomogeneousIdeal
eq6 :
  ↑s1 { val := ↑y, property := (_ : ↑{ val := ↑y, property := (_ : ↑y ∈ ↑v1) } ∈ ↑(op u1).unop) } =
    Quotient.mk''
      { deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
        den_mem := b1_nin_y }
b2_nin_y : ¬↑{ val := b2, property := b2_mem } ∈ (↑{ val := ↑y, property := (_ : ↑y ∈ ↑v2) }).asHomogeneousIdeal
eq7 :
  ↑s2 { val := ↑y, property := (_ : ↑{ val := ↑y, property := (_ : ↑y ∈ ↑v2) } ∈ ↑(op u2).unop) } =
    Quotient.mk''
      { deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
        den_mem := b2_nin_y }
⊢ Localization.mk
      ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
            den_mem := b1_nin_y }.num
      {
        val :=
          ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                den_mem := b1_nin_y }.den,
        property :=
          (_ :
            ↑{ deg := j1, num := { val := a1, property := a1_mem }, den := { val := b1, property := b1_mem },
                    den_mem := b1_nin_y }.den ∈
              Ideal.primeCompl (HomogeneousIdeal.toIdeal (↑y).asHomogeneousIdeal)) } =
    Localization.mk
      ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
            den_mem := b2_nin_y }.num
      {
        val :=
          ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                den_mem := b2_nin_y }.den,
        property :=
          (_ :
            ↑{ deg := j2, num := { val := a2, property := a2_mem }, den := { val := b2, property := b2_mem },
                    den_mem := b2_nin_y }.den ∈
              Ideal.primeCompl (HomogeneousIdeal.toIdeal (↑y).asHomogeneousIdeal)) }
[PROOFSTEP]
exact
  eq3' _
    ⟨⟨leOfHom (Opens.infLELeft _ _ ≫ Opens.infLELeft _ _ ≫ Opens.infLELeft _ _ ≫ Opens.infLELeft _ _) y.2,
        leOfHom (Opens.infLELeft _ _ ≫ Opens.infLELeft _ _ ≫ Opens.infLELeft _ _ ≫ Opens.infLERight _ _) y.2⟩,
      leOfHom (Opens.infLELeft _ _ ≫ Opens.infLELeft _ _ ≫ Opens.infLERight _ _) y.2⟩
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
f : ↑(CommRingCat.of (at x))
⊢ ↑(stalkToFiberRingHom 𝒜 x) (homogeneousLocalizationToStalk 𝒜 x f) = f
[PROOFSTEP]
rw [homogeneousLocalizationToStalk]
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
f : ↑(CommRingCat.of (at x))
⊢ ↑(stalkToFiberRingHom 𝒜 x)
      (↑(Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜))
            { val := x, property := (_ : x ∈ ProjectiveSpectrum.basicOpen 𝒜 (HomogeneousLocalization.den f)) })
        (sectionInBasicOpen 𝒜 x f)) =
    f
[PROOFSTEP]
erw [stalkToFiberRingHom_germ 𝒜 (ProjectiveSpectrum.basicOpen 𝒜 f.den) ⟨x, _⟩ (sectionInBasicOpen _ x f)]
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
f : ↑(CommRingCat.of (at x))
⊢ ↑(sectionInBasicOpen 𝒜 x f)
      { val := x, property := (_ : x ∈ ProjectiveSpectrum.basicOpen 𝒜 (HomogeneousLocalization.den f)) } =
    f
[PROOFSTEP]
rw [sectionInBasicOpen, HomogeneousLocalization.ext_iff_val, f.eq_num_div_den]
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
f : ↑(CommRingCat.of (at x))
⊢ HomogeneousLocalization.val
      (↑{
            val := fun y =>
              Quotient.mk''
                { deg := HomogeneousLocalization.deg f,
                  num :=
                    { val := HomogeneousLocalization.num f,
                      property := (_ : HomogeneousLocalization.num f ∈ 𝒜 (HomogeneousLocalization.deg f)) },
                  den :=
                    { val := HomogeneousLocalization.den f,
                      property := (_ : HomogeneousLocalization.den f ∈ 𝒜 (HomogeneousLocalization.deg f)) },
                  den_mem := (_ : ↑y ∈ (op (ProjectiveSpectrum.basicOpen 𝒜 (HomogeneousLocalization.den f))).unop) },
            property :=
              (_ :
                ∀ (y : { x_1 // x_1 ∈ (op (ProjectiveSpectrum.basicOpen 𝒜 (HomogeneousLocalization.den f))).unop }),
                  ∃ V x_1 i,
                    PrelocalPredicate.pred (isFractionPrelocal 𝒜) fun x_2 =>
                      (fun y =>
                          Quotient.mk''
                            { deg := HomogeneousLocalization.deg f,
                              num :=
                                { val := HomogeneousLocalization.num f,
                                  property := (_ : HomogeneousLocalization.num f ∈ 𝒜 (HomogeneousLocalization.deg f)) },
                              den :=
                                { val := HomogeneousLocalization.den f,
                                  property := (_ : HomogeneousLocalization.den f ∈ 𝒜 (HomogeneousLocalization.deg f)) },
                              den_mem :=
                                (_ : ↑y ∈ (op (ProjectiveSpectrum.basicOpen 𝒜 (HomogeneousLocalization.den f))).unop) })
                        ((fun x_3 =>
                            { val := ↑x_3,
                              property :=
                                (_ :
                                  ↑x_3 ∈ ↑(op (ProjectiveSpectrum.basicOpen 𝒜 (HomogeneousLocalization.den f))).unop) })
                          x_2)) }
        { val := x, property := (_ : x ∈ ProjectiveSpectrum.basicOpen 𝒜 (HomogeneousLocalization.den f)) }) =
    Localization.mk (HomogeneousLocalization.num f)
      { val := HomogeneousLocalization.den f,
        property :=
          (_ : HomogeneousLocalization.den f ∈ Ideal.primeCompl (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) }
[PROOFSTEP]
simp only [unop_op, HomogeneousLocalization.val_mk'', mk_eq_monoidOf_mk']