-- 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 𝒜
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  ∀ {X Y : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ} (f : X ⟶ Y),
    Eq (α :=
      Functor.obj
          (structurePresheafInCommRing 𝒜 ⋙
              forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) :
            (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
          X ⟶
        Functor.obj
          (ObjectProperty.FullSubcategory.obj (P :=
              (CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) :
                (P : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1) → Prop))
              (structureSheafInType 𝒜 : TopCat.Sheaf (Type u_1) (ProjectiveSpectrum.top 𝒜)) :
            (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
          Y)
      (CategoryStruct.comp (Y :=
          Functor.obj
            (structurePresheafInCommRing 𝒜 ⋙
                forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                  CommRingCat.carrier) :
              (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
            Y)
          (CategoryTheory.Functor.map
              (structurePresheafInCommRing 𝒜 ⋙
                forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                  CommRingCat.carrier))
              f :
            Functor.obj
                (structurePresheafInCommRing 𝒜 ⋙
                    forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1))
                      (CC := CommRingCat.carrier) :
                  (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
                X ⟶
              Functor.obj
                (structurePresheafInCommRing 𝒜 ⋙
                    forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1))
                      (CC := CommRingCat.carrier) :
                  (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
                Y)
          (Iso.hom
              ((fun (x : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ) ↦
                  (Iso.refl
                      (Functor.obj
                        (structurePresheafInCommRing 𝒜 ⋙
                            forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦
                              (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier) :
                          (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
                        x) :
                    Functor.obj
                        (structurePresheafInCommRing 𝒜 ⋙
                            forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦
                              (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier) :
                          (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
                        x ≅
                      Functor.obj
                        (structurePresheafInCommRing 𝒜 ⋙
                            forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦
                              (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier) :
                          (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
                        x))
                Y) :
            Functor.obj
                (structurePresheafInCommRing 𝒜 ⋙
                    forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1))
                      (CC := CommRingCat.carrier) :
                  (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
                Y ⟶
              Functor.obj
                (ObjectProperty.FullSubcategory.obj (P :=
                    (CategoryTheory.Presheaf.IsSheaf
                        (Opens.grothendieckTopology (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) :
                      (P : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1) → Prop))
                    (structureSheafInType 𝒜 : TopCat.Sheaf (Type u_1) (ProjectiveSpectrum.top 𝒜)) :
                  (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
                Y) :
        Functor.obj
            (structurePresheafInCommRing 𝒜 ⋙
                forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                  CommRingCat.carrier) :
              (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
            X ⟶
          Functor.obj
            (ObjectProperty.FullSubcategory.obj (P :=
                (CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) :
                  (P : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1) → Prop))
                (structureSheafInType 𝒜 : TopCat.Sheaf (Type u_1) (ProjectiveSpectrum.top 𝒜)) :
              (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
            Y)
      (CategoryStruct.comp (Y :=
          Functor.obj
            (ObjectProperty.FullSubcategory.obj (P :=
                (CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) :
                  (P : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1) → Prop))
                (structureSheafInType 𝒜 : TopCat.Sheaf (Type u_1) (ProjectiveSpectrum.top 𝒜)) :
              (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
            X)
          (Iso.hom
              ((fun (x : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ) ↦
                  (Iso.refl
                      (Functor.obj
                        (structurePresheafInCommRing 𝒜 ⋙
                            forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦
                              (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier) :
                          (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
                        x) :
                    Functor.obj
                        (structurePresheafInCommRing 𝒜 ⋙
                            forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦
                              (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier) :
                          (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
                        x ≅
                      Functor.obj
                        (structurePresheafInCommRing 𝒜 ⋙
                            forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦
                              (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier) :
                          (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
                        x))
                X) :
            Functor.obj
                (structurePresheafInCommRing 𝒜 ⋙
                    forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1))
                      (CC := CommRingCat.carrier) :
                  (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
                X ⟶
              Functor.obj
                (ObjectProperty.FullSubcategory.obj (P :=
                    (CategoryTheory.Presheaf.IsSheaf
                        (Opens.grothendieckTopology (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) :
                      (P : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1) → Prop))
                    (structureSheafInType 𝒜 : TopCat.Sheaf (Type u_1) (ProjectiveSpectrum.top 𝒜)) :
                  (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
                X)
          (CategoryTheory.Functor.map
              (ObjectProperty.FullSubcategory.obj (P :=
                (CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) :
                  (P : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1) → Prop))
                (structureSheafInType 𝒜 : TopCat.Sheaf (Type u_1) (ProjectiveSpectrum.top 𝒜)))
              f :
            Functor.obj
                (ObjectProperty.FullSubcategory.obj (P :=
                    (CategoryTheory.Presheaf.IsSheaf
                        (Opens.grothendieckTopology (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) :
                      (P : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1) → Prop))
                    (structureSheafInType 𝒜 : TopCat.Sheaf (Type u_1) (ProjectiveSpectrum.top 𝒜)) :
                  (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
                X ⟶
              Functor.obj
                (ObjectProperty.FullSubcategory.obj (P :=
                    (CategoryTheory.Presheaf.IsSheaf
                        (Opens.grothendieckTopology (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) :
                      (P : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1) → Prop))
                    (structureSheafInType 𝒜 : TopCat.Sheaf (Type u_1) (ProjectiveSpectrum.top 𝒜)) :
                  (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
                Y) :
        Functor.obj
            (structurePresheafInCommRing 𝒜 ⋙
                forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                  CommRingCat.carrier) :
              (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
            X ⟶
          Functor.obj
            (ObjectProperty.FullSubcategory.obj (P :=
                (CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) :
                  (P : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1) → Prop))
                (structureSheafInType 𝒜 : TopCat.Sheaf (Type u_1) (ProjectiveSpectrum.top 𝒜)) :
              (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
            Y)
⊢ ∀ {X Y : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ} (f : X ⟶ Y),
    Eq (α :=
      Functor.obj
          (structurePresheafInCommRing 𝒜 ⋙
              forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) :
            (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
          X ⟶
        Functor.obj
          (ObjectProperty.FullSubcategory.obj (P :=
              (CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) :
                (P : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1) → Prop))
              (structureSheafInType 𝒜 : TopCat.Sheaf (Type u_1) (ProjectiveSpectrum.top 𝒜)) :
            (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
          Y)
      (CategoryStruct.comp (Y :=
          Functor.obj
            (structurePresheafInCommRing 𝒜 ⋙
                forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                  CommRingCat.carrier) :
              (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
            Y)
          (CategoryTheory.Functor.map
              (structurePresheafInCommRing 𝒜 ⋙
                forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                  CommRingCat.carrier))
              f :
            Functor.obj
                (structurePresheafInCommRing 𝒜 ⋙
                    forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1))
                      (CC := CommRingCat.carrier) :
                  (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
                X ⟶
              Functor.obj
                (structurePresheafInCommRing 𝒜 ⋙
                    forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1))
                      (CC := CommRingCat.carrier) :
                  (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
                Y)
          (Iso.hom
              ((fun (x : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ) ↦
                  (Iso.refl
                      (Functor.obj
                        (structurePresheafInCommRing 𝒜 ⋙
                            forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦
                              (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier) :
                          (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
                        x) :
                    Functor.obj
                        (structurePresheafInCommRing 𝒜 ⋙
                            forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦
                              (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier) :
                          (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
                        x ≅
                      Functor.obj
                        (structurePresheafInCommRing 𝒜 ⋙
                            forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦
                              (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier) :
                          (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
                        x))
                Y) :
            Functor.obj
                (structurePresheafInCommRing 𝒜 ⋙
                    forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1))
                      (CC := CommRingCat.carrier) :
                  (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
                Y ⟶
              Functor.obj
                (ObjectProperty.FullSubcategory.obj (P :=
                    (CategoryTheory.Presheaf.IsSheaf
                        (Opens.grothendieckTopology (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) :
                      (P : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1) → Prop))
                    (structureSheafInType 𝒜 : TopCat.Sheaf (Type u_1) (ProjectiveSpectrum.top 𝒜)) :
                  (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
                Y) :
        Functor.obj
            (structurePresheafInCommRing 𝒜 ⋙
                forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                  CommRingCat.carrier) :
              (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
            X ⟶
          Functor.obj
            (ObjectProperty.FullSubcategory.obj (P :=
                (CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) :
                  (P : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1) → Prop))
                (structureSheafInType 𝒜 : TopCat.Sheaf (Type u_1) (ProjectiveSpectrum.top 𝒜)) :
              (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
            Y)
      (CategoryStruct.comp (Y :=
          Functor.obj
            (ObjectProperty.FullSubcategory.obj (P :=
                (CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) :
                  (P : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1) → Prop))
                (structureSheafInType 𝒜 : TopCat.Sheaf (Type u_1) (ProjectiveSpectrum.top 𝒜)) :
              (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
            X)
          (Iso.hom
              ((fun (x : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ) ↦
                  (Iso.refl
                      (Functor.obj
                        (structurePresheafInCommRing 𝒜 ⋙
                            forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦
                              (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier) :
                          (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
                        x) :
                    Functor.obj
                        (structurePresheafInCommRing 𝒜 ⋙
                            forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦
                              (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier) :
                          (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
                        x ≅
                      Functor.obj
                        (structurePresheafInCommRing 𝒜 ⋙
                            forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦
                              (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier) :
                          (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
                        x))
                X) :
            Functor.obj
                (structurePresheafInCommRing 𝒜 ⋙
                    forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1))
                      (CC := CommRingCat.carrier) :
                  (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
                X ⟶
              Functor.obj
                (ObjectProperty.FullSubcategory.obj (P :=
                    (CategoryTheory.Presheaf.IsSheaf
                        (Opens.grothendieckTopology (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) :
                      (P : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1) → Prop))
                    (structureSheafInType 𝒜 : TopCat.Sheaf (Type u_1) (ProjectiveSpectrum.top 𝒜)) :
                  (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
                X)
          (CategoryTheory.Functor.map
              (ObjectProperty.FullSubcategory.obj (P :=
                (CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) :
                  (P : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1) → Prop))
                (structureSheafInType 𝒜 : TopCat.Sheaf (Type u_1) (ProjectiveSpectrum.top 𝒜)))
              f :
            Functor.obj
                (ObjectProperty.FullSubcategory.obj (P :=
                    (CategoryTheory.Presheaf.IsSheaf
                        (Opens.grothendieckTopology (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) :
                      (P : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1) → Prop))
                    (structureSheafInType 𝒜 : TopCat.Sheaf (Type u_1) (ProjectiveSpectrum.top 𝒜)) :
                  (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
                X ⟶
              Functor.obj
                (ObjectProperty.FullSubcategory.obj (P :=
                    (CategoryTheory.Presheaf.IsSheaf
                        (Opens.grothendieckTopology (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) :
                      (P : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1) → Prop))
                    (structureSheafInType 𝒜 : TopCat.Sheaf (Type u_1) (ProjectiveSpectrum.top 𝒜)) :
                  (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
                Y) :
        Functor.obj
            (structurePresheafInCommRing 𝒜 ⋙
                forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                  CommRingCat.carrier) :
              (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
            X ⟶
          Functor.obj
            (ObjectProperty.FullSubcategory.obj (P :=
                (CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) :
                  (P : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1) → Prop))
                (structureSheafInType 𝒜 : TopCat.Sheaf (Type u_1) (ProjectiveSpectrum.top 𝒜)) :
              (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ Type u_1)
            Y)

Tactic:
cat_disch