-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)
U : Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)
hxU : x ∈ U
s :
  ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier)
    (Functor.obj (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜)) (op U))
V : Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)
hxV :
  (↑(Subtype.mk (p := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ x ∈ unop (op U)) x hxU) :
      (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ∈
    V
i : V ⟶ unop (op U)
n : ℕ
a b : ↥(𝒜 n)
h : ∀ (x : ↥V), (↑b : A) ∉ (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal
e :
  ∀ (a_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) (b_1 : a_1 ∈ V),
    (↑s : (x : ↥U) → at (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
        (Subtype.mk (p := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ x ∈ U) a_1 ⋯) =
      HomogeneousLocalization.mk { deg := n, num := a, den := b, den_mem := ⋯ }
a₁ :
  ∀ (t : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) (ht : t ∈ unop (op V)),
    Eq (α :=
      Localization (M := A)
        (↑(Subtype.mk (p := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ x ∈ unop (op V)) t ht) :
                (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
      (HomogeneousLocalization.val.{0, u_1, u_2} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
        ((↑(((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                      CommRingCat.carrier) (X :=
                      Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                        (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                        (op
                            (ProjectiveSpectrum.basicOpen 𝒜
                              (↑(HomogeneousLocalization.NumDenSameDeg.den
                                    { deg := n, num := a, den := b, den_mem := ⋯ }) :
                                A)) :
                          (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ))
                      (Y :=
                      Functor.obj
                        (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                        (op V))
                      (CategoryTheory.Functor.map (Sheaf.presheaf (Proj.structureSheaf 𝒜)) (Quiver.Hom.op (homOfLE ⋯)) :
                        Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                            (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                            (op
                                (ProjectiveSpectrum.basicOpen 𝒜
                                  (↑(HomogeneousLocalization.NumDenSameDeg.den
                                        { deg := n, num := a, den := b, den_mem := ⋯ :
                                          HomogeneousLocalization.NumDenSameDeg 𝒜
                                            x.asHomogeneousIdeal.toIdeal.primeCompl }) :
                                    A)) :
                              (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ) ⟶
                          Functor.obj
                            (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                            (op V)) :
                    (↑(Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                            (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                            (op
                                (ProjectiveSpectrum.basicOpen 𝒜
                                  (↑(HomogeneousLocalization.NumDenSameDeg.den
                                        { deg := n, num := a, den := b, den_mem := ⋯ }) :
                                    A)) :
                              (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)) :
                        Type u_1) →+*
                      (↑(Functor.obj
                            (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                            (op V)) :
                        Type u_1)) :
                  (a :
                      (↑((Proj.structureSheaf 𝒜).presheaf.obj
                            (op
                              (ProjectiveSpectrum.basicOpen 𝒜
                                (↑{ deg := n, num := a, den := b, den_mem := ⋯ }.den : A)))) :
                        Type u_1)) →
                    (↑((Proj.structureSheaf 𝒜).presheaf.obj (op V)) : Type u_1))
                (sectionInBasicOpen 𝒜 x { deg := n, num := a, den := b, den_mem := ⋯ })) :
            (x : ↥(unop (op V))) →
              (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
                (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
          (Subtype.mk (p := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ x ∈ unop (op V)) t ht)))
      (HomogeneousLocalization.val.{0, u_1, u_2} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
        ((↑(((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                      CommRingCat.carrier) (X :=
                      Functor.obj
                        (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                        (op (unop (op U))))
                      (Y :=
                      Functor.obj
                        (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                        (op V))
                      (CategoryTheory.Functor.map (Sheaf.presheaf (Proj.structureSheaf 𝒜)) i.op :
                        Functor.obj
                            (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                            (op (unop (op U))) ⟶
                          Functor.obj
                            (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                            (op V)) :
                    (↑(Functor.obj
                            (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                            (op (unop (op U)))) :
                        Type u_1) →+*
                      (↑(Functor.obj
                            (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                            (op V)) :
                        Type u_1)) :
                  (a : (↑((Proj.structureSheaf 𝒜).presheaf.obj (op (unop (op U)))) : Type u_1)) →
                    (↑((Proj.structureSheaf 𝒜).presheaf.obj (op V)) : Type u_1))
                s) :
            (x : ↥(unop (op V))) →
              (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
                (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
          (Subtype.mk (p := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ x ∈ unop (op V)) t ht)))
⊢ Eq.{u_1 + 1} (α :=
    (x : ↥(unop (op V))) →
      (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x) (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
    (↑(((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (X :=
                Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                  (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                  (op
                      (ProjectiveSpectrum.basicOpen 𝒜
                        (↑(HomogeneousLocalization.NumDenSameDeg.den { deg := n, num := a, den := b, den_mem := ⋯ }) :
                          A)) :
                    (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ))
                (Y :=
                Functor.obj (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                  (op V))
                (CategoryTheory.Functor.map (Sheaf.presheaf (Proj.structureSheaf 𝒜)) (Quiver.Hom.op (homOfLE ⋯)) :
                  Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                      (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                      (op
                          (ProjectiveSpectrum.basicOpen 𝒜
                            (↑(HomogeneousLocalization.NumDenSameDeg.den
                                  { deg := n, num := a, den := b, den_mem := ⋯ :
                                    HomogeneousLocalization.NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl }) :
                              A)) :
                        (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ) ⟶
                    Functor.obj
                      (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                      (op V)) :
              (↑(Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                      (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                      (op
                          (ProjectiveSpectrum.basicOpen 𝒜
                            (↑(HomogeneousLocalization.NumDenSameDeg.den
                                  { deg := n, num := a, den := b, den_mem := ⋯ }) :
                              A)) :
                        (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)) :
                  Type u_1) →+*
                (↑(Functor.obj
                      (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                      (op V)) :
                  Type u_1)) :
            (a :
                (↑((Proj.structureSheaf 𝒜).presheaf.obj
                      (op (ProjectiveSpectrum.basicOpen 𝒜 (↑{ deg := n, num := a, den := b, den_mem := ⋯ }.den : A)))) :
                  Type u_1)) →
              (↑((Proj.structureSheaf 𝒜).presheaf.obj (op V)) : Type u_1))
          (sectionInBasicOpen 𝒜 x { deg := n, num := a, den := b, den_mem := ⋯ })) :
      (x : ↥(unop (op V))) →
        (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x) (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
    (↑(((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (X :=
                Functor.obj (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                  (op (unop (op U))))
                (Y :=
                Functor.obj (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                  (op V))
                (CategoryTheory.Functor.map (Sheaf.presheaf (Proj.structureSheaf 𝒜)) i.op :
                  Functor.obj (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                      (op (unop (op U))) ⟶
                    Functor.obj
                      (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                      (op V)) :
              (↑(Functor.obj (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                      (op (unop (op U)))) :
                  Type u_1) →+*
                (↑(Functor.obj
                      (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                      (op V)) :
                  Type u_1)) :
            (a : (↑((Proj.structureSheaf 𝒜).presheaf.obj (op (unop (op U)))) : Type u_1)) →
              (↑((Proj.structureSheaf 𝒜).presheaf.obj (op V)) : Type u_1))
          s) :
      (x : ↥(unop (op V))) →
        (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x) (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))

Tactic:
ext ⟨t, ht⟩