-- 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)
y : at x
f g : NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl
c : A
hc : c ∈ x.asHomogeneousIdeal.toIdeal.primeCompl
hc' :
  (↑(Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x.asHomogeneousIdeal.toIdeal.primeCompl) c hc) : A) *
      ((↑g.den : A) * (↑f.num : A)) =
    (↑(Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x.asHomogeneousIdeal.toIdeal.primeCompl) c hc) : A) *
      ((↑f.den : A) * (↑g.num : A))
a :
  ∀ (t : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))
    (ht' : t ∈ (↑(ProjectiveSpectrum.basicOpen 𝒜 c) : Set (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
    (htf : t ∈ (↑(ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A)) : Set (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
    (htg : t ∈ (↑(ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A)) : Set (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))),
    Eq (α :=
      Localization (M := A)
        (↑(Subtype.mk (p := fun (x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
                    Membership.mem (γ := Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))
                      (unop
                        (op
                          (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                            ProjectiveSpectrum.basicOpen 𝒜 c)))
                      x_1)
                    t ⋯) :
                (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
      (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 𝒜 (↑f.den : A)) :
                          (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ))
                      (Y :=
                      Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                        (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                        (op
                            (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                              ProjectiveSpectrum.basicOpen 𝒜 c) :
                          (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ))
                      (CategoryTheory.Functor.map (Sheaf.presheaf (Proj.structureSheaf 𝒜))
                          (Quiver.Hom.op (homOfLE ⋯ ≫ homOfLE ⋯)) :
                        Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                            (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                            (op (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A)) :
                              (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ) ⟶
                          Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                            (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                            (op
                                (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓
                                    ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                                  ProjectiveSpectrum.basicOpen 𝒜 c) :
                              (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)) :
                    (↑(Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                            (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                            (op (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A)) :
                              (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)) :
                        Type u_1) →+*
                      (↑(Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                            (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                            (op
                                (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓
                                    ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                                  ProjectiveSpectrum.basicOpen 𝒜 c) :
                              (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)) :
                        Type u_1)) :
                  (a :
                      (↑((Proj.structureSheaf 𝒜).presheaf.obj (op (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A)))) :
                        Type u_1)) →
                    (↑((Proj.structureSheaf 𝒜).presheaf.obj
                          (op
                            (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                              ProjectiveSpectrum.basicOpen 𝒜 c))) :
                      Type u_1))
                (sectionInBasicOpen 𝒜 x f)) :
            (x_1 :
                ↥(unop
                    (op
                      (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                        ProjectiveSpectrum.basicOpen 𝒜 c)))) →
              (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
                (↑x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
          (Subtype.mk (p := fun (x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
            Membership.mem (γ := Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))
              (unop
                (op
                  (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                    ProjectiveSpectrum.basicOpen 𝒜 c)))
              x_1)
            t ⋯)))
      (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 𝒜 (↑g.den : A)) :
                          (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ))
                      (Y :=
                      Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                        (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                        (op
                            (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                              ProjectiveSpectrum.basicOpen 𝒜 c) :
                          (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ))
                      (CategoryTheory.Functor.map (Sheaf.presheaf (Proj.structureSheaf 𝒜))
                          (Quiver.Hom.op (homOfLE ⋯ ≫ homOfLE ⋯)) :
                        Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                            (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                            (op (ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A)) :
                              (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ) ⟶
                          Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                            (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                            (op
                                (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓
                                    ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                                  ProjectiveSpectrum.basicOpen 𝒜 c) :
                              (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)) :
                    (↑(Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                            (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                            (op (ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A)) :
                              (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)) :
                        Type u_1) →+*
                      (↑(Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                            (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                            (op
                                (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓
                                    ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                                  ProjectiveSpectrum.basicOpen 𝒜 c) :
                              (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)) :
                        Type u_1)) :
                  (a :
                      (↑((Proj.structureSheaf 𝒜).presheaf.obj (op (ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A)))) :
                        Type u_1)) →
                    (↑((Proj.structureSheaf 𝒜).presheaf.obj
                          (op
                            (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                              ProjectiveSpectrum.basicOpen 𝒜 c))) :
                      Type u_1))
                (sectionInBasicOpen 𝒜 x g)) :
            (x_1 :
                ↥(unop
                    (op
                      (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                        ProjectiveSpectrum.basicOpen 𝒜 c)))) →
              (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
                (↑x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
          (Subtype.mk (p := fun (x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
            Membership.mem (γ := Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))
              (unop
                (op
                  (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                    ProjectiveSpectrum.basicOpen 𝒜 c)))
              x_1)
            t ⋯)))
⊢ Eq.{u_1 + 1} (α :=
    (x_1 :
        ↥(unop
            (op
              (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                ProjectiveSpectrum.basicOpen 𝒜 c)))) →
      (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x) (↑x_1 : (↑(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 𝒜 (↑f.den : A)) :
                    (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ))
                (Y :=
                Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                  (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                  (op
                      (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                        ProjectiveSpectrum.basicOpen 𝒜 c) :
                    (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ))
                (CategoryTheory.Functor.map (Sheaf.presheaf (Proj.structureSheaf 𝒜))
                    (Quiver.Hom.op (homOfLE ⋯ ≫ homOfLE ⋯)) :
                  Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                      (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                      (op (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A)) :
                        (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ) ⟶
                    Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                      (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                      (op
                          (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                            ProjectiveSpectrum.basicOpen 𝒜 c) :
                        (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)) :
              (↑(Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                      (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                      (op (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A)) :
                        (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)) :
                  Type u_1) →+*
                (↑(Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                      (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                      (op
                          (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                            ProjectiveSpectrum.basicOpen 𝒜 c) :
                        (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)) :
                  Type u_1)) :
            (a :
                (↑((Proj.structureSheaf 𝒜).presheaf.obj (op (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A)))) :
                  Type u_1)) →
              (↑((Proj.structureSheaf 𝒜).presheaf.obj
                    (op
                      (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                        ProjectiveSpectrum.basicOpen 𝒜 c))) :
                Type u_1))
          (sectionInBasicOpen 𝒜 x f)) :
      (x_1 :
          ↥(unop
              (op
                (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                  ProjectiveSpectrum.basicOpen 𝒜 c)))) →
        (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x) (↑x_1 : (↑(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 𝒜 (↑g.den : A)) :
                    (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ))
                (Y :=
                Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                  (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                  (op
                      (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                        ProjectiveSpectrum.basicOpen 𝒜 c) :
                    (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ))
                (CategoryTheory.Functor.map (Sheaf.presheaf (Proj.structureSheaf 𝒜))
                    (Quiver.Hom.op (homOfLE ⋯ ≫ homOfLE ⋯)) :
                  Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                      (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                      (op (ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A)) :
                        (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ) ⟶
                    Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                      (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                      (op
                          (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                            ProjectiveSpectrum.basicOpen 𝒜 c) :
                        (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)) :
              (↑(Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                      (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                      (op (ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A)) :
                        (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)) :
                  Type u_1) →+*
                (↑(Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                      (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                      (op
                          (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                            ProjectiveSpectrum.basicOpen 𝒜 c) :
                        (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)) :
                  Type u_1)) :
            (a :
                (↑((Proj.structureSheaf 𝒜).presheaf.obj (op (ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A)))) :
                  Type u_1)) →
              (↑((Proj.structureSheaf 𝒜).presheaf.obj
                    (op
                      (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                        ProjectiveSpectrum.basicOpen 𝒜 c))) :
                Type u_1))
          (sectionInBasicOpen 𝒜 x g)) :
      (x_1 :
          ↥(unop
              (op
                (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                  ProjectiveSpectrum.basicOpen 𝒜 c)))) →
        (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x) (↑x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))

Tactic:
ext ⟨t, ⟨htf, htg⟩, ht'⟩