-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
U V : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ
i : V ⟶ U
s :
  (↑(Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
            (CategoryTheory.Presheaf.IsSheaf (grothendieckTopology (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) :
              (P : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ CommRingCat) → Prop))
            (Proj.structureSheaf 𝒜 : TopCat.Sheaf CommRingCat (ProjectiveSpectrum.top 𝒜)) :
          (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ CommRingCat)
        V) :
    Type u_1)
x : ↥(unop U)
⊢ (↑(((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                  CommRingCat.carrier) (X :=
                  Functor.obj
                    (ObjectProperty.FullSubcategory.obj (P :=
                        (CategoryTheory.Presheaf.IsSheaf
                            (grothendieckTopology (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) :
                          (P : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ CommRingCat) → Prop))
                        (Proj.structureSheaf 𝒜 : TopCat.Sheaf CommRingCat (ProjectiveSpectrum.top 𝒜)) :
                      (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ CommRingCat)
                    V)
                  (Y :=
                  Functor.obj
                    (ObjectProperty.FullSubcategory.obj (P :=
                        (CategoryTheory.Presheaf.IsSheaf
                            (grothendieckTopology (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) :
                          (P : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ CommRingCat) → Prop))
                        (Proj.structureSheaf 𝒜 : TopCat.Sheaf CommRingCat (ProjectiveSpectrum.top 𝒜)) :
                      (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ CommRingCat)
                    U)
                  (CategoryTheory.Functor.map
                      (ObjectProperty.FullSubcategory.obj (P :=
                        (CategoryTheory.Presheaf.IsSheaf
                            (grothendieckTopology (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) :
                          (P : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ CommRingCat) → Prop))
                        (Proj.structureSheaf 𝒜 : TopCat.Sheaf CommRingCat (ProjectiveSpectrum.top 𝒜)))
                      i :
                    Functor.obj
                        (ObjectProperty.FullSubcategory.obj (P :=
                            (CategoryTheory.Presheaf.IsSheaf
                                (grothendieckTopology (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) :
                              (P : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ CommRingCat) → Prop))
                            (Proj.structureSheaf 𝒜 : TopCat.Sheaf CommRingCat (ProjectiveSpectrum.top 𝒜)) :
                          (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ CommRingCat)
                        V ⟶
                      Functor.obj
                        (ObjectProperty.FullSubcategory.obj (P :=
                            (CategoryTheory.Presheaf.IsSheaf
                                (grothendieckTopology (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) :
                              (P : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ CommRingCat) → Prop))
                            (Proj.structureSheaf 𝒜 : TopCat.Sheaf CommRingCat (ProjectiveSpectrum.top 𝒜)) :
                          (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ CommRingCat)
                        U) :
                (↑(Functor.obj
                        (ObjectProperty.FullSubcategory.obj (P :=
                            (CategoryTheory.Presheaf.IsSheaf
                                (grothendieckTopology (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) :
                              (P : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ CommRingCat) → Prop))
                            (Proj.structureSheaf 𝒜 : TopCat.Sheaf CommRingCat (ProjectiveSpectrum.top 𝒜)) :
                          (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ CommRingCat)
                        V) :
                    Type u_1) →+*
                  (↑(Functor.obj
                        (ObjectProperty.FullSubcategory.obj (P :=
                            (CategoryTheory.Presheaf.IsSheaf
                                (grothendieckTopology (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) :
                              (P : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ CommRingCat) → Prop))
                            (Proj.structureSheaf 𝒜 : TopCat.Sheaf CommRingCat (ProjectiveSpectrum.top 𝒜)) :
                          (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ CommRingCat)
                        U) :
                    Type u_1)) :
              (a : (↑((Proj.structureSheaf 𝒜).obj.obj V) : Type u_1)) →
                (↑((Proj.structureSheaf 𝒜).obj.obj U) : Type u_1))
            s) :
        (x : ↥(unop U)) →
          (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x) (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
      x =
    (↑s :
        (x : ↥(unop V)) →
          (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x) (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
      ((i.unop : (a : ↥(unop U)) → ↥(unop V)) x)

Tactic:
rfl

Premises used: Set.Mem, rfl