-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
Goal:
A B σ τ : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : CommRing B
inst_4 : SetLike τ B
inst_5 : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst_6 : GradedRing 𝒜
inst_7 : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (HomogeneousIdeal.map f (𝒜₊))
p : ProjectiveSpectrum ℬ
c :
  NumDenSameDeg 𝒜
    (Ideal.primeCompl
      (toIdeal (σ := σ) (𝒜 := 𝒜)
        (asHomogeneousIdeal
          (((ProjectiveSpectrum.comap f hf : C(ProjectiveSpectrum ℬ, ProjectiveSpectrum 𝒜)) :
              (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
            p))))
⊢ Eq (α := (↑((toSheafedSpace ℬ).presheaf.stalk p) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X :=
            (toSheafedSpace ℬ).presheaf.obj
              (Opposite.op
                (Functor.obj (C := Opens (↑(↑(toSheafedSpace 𝒜).toPresheafedSpace : TopCat) : Type u))
                  (Opens.map (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (sheafedSpaceMap f hf))))
                  (Opposite.unop (Opposite.op (ProjectiveSpectrum.basicOpen 𝒜 (↑c.den : A)))))))
            (Y := (toSheafedSpace ℬ).presheaf.stalk p)
            ((toSheafedSpace ℬ).presheaf.germ
              (Functor.obj (C := Opens (↑(↑(toSheafedSpace 𝒜).toPresheafedSpace : TopCat) : Type u))
                (Opens.map (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (sheafedSpaceMap f hf))))
                (Opposite.unop (Opposite.op (ProjectiveSpectrum.basicOpen 𝒜 (↑c.den : A)))))
              p ⋯) :
          (a :
              (↑((toSheafedSpace ℬ).presheaf.obj
                    (Opposite.op
                      ((Opens.map (sheafedSpaceMap f hf).hom.base).obj
                        (Opposite.unop (Opposite.op (ProjectiveSpectrum.basicOpen 𝒜 (↑c.den : A))))))) :
                Type u)) →
            (↑((toSheafedSpace ℬ).presheaf.stalk p) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X :=
                (toSheafedSpace 𝒜).presheaf.obj (Opposite.op (ProjectiveSpectrum.basicOpen 𝒜 (↑c.den : A)))) (Y :=
                Functor.obj (C := (Opens (↑(↑(toSheafedSpace 𝒜).toPresheafedSpace : TopCat) : Type u))ᵒᵖ)
                  (Functor.obj
                    (TopCat.Presheaf.pushforward CommRingCat
                      (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (sheafedSpaceMap f hf))))
                    (toSheafedSpace ℬ).presheaf)
                  (Opposite.op (ProjectiveSpectrum.basicOpen 𝒜 (↑c.den : A))))
                (NatTrans.app (PresheafedSpace.Hom.c (InducedCategory.Hom.hom (sheafedSpaceMap f hf)))
                  (Opposite.op (ProjectiveSpectrum.basicOpen 𝒜 (↑c.den : A)))) :
              (a :
                  (↑((toSheafedSpace 𝒜).presheaf.obj (Opposite.op (ProjectiveSpectrum.basicOpen 𝒜 (↑c.den : A)))) :
                    Type u)) →
                (↑(((TopCat.Presheaf.pushforward CommRingCat (sheafedSpaceMap f hf).hom.base).obj
                          (toSheafedSpace ℬ).presheaf).obj
                      (Opposite.op (ProjectiveSpectrum.basicOpen 𝒜 (↑c.den : A)))) :
                  Type u))
            (sectionInBasicOpen 𝒜
              (((ProjectiveSpectrum.comap f hf : C(ProjectiveSpectrum ℬ, ProjectiveSpectrum 𝒜)) :
                  (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
                p)
              c) :
          (↑(Functor.obj (C := (Opens (↑(↑(toSheafedSpace 𝒜).toPresheafedSpace : TopCat) : Type u))ᵒᵖ)
                (Functor.obj
                  (TopCat.Presheaf.pushforward CommRingCat
                    (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (sheafedSpaceMap f hf))))
                  (toSheafedSpace ℬ).presheaf)
                (Opposite.op (ProjectiveSpectrum.basicOpen 𝒜 (↑c.den : A)))) :
            Type u)) :
      (↑((toSheafedSpace ℬ).presheaf.stalk p) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X :=
            (toSheafedSpace ℬ).presheaf.obj
              (Opposite.op (ProjectiveSpectrum.basicOpen ℬ ((f : (a : A) → B) (↑c.den : A)))))
            (Y := (toSheafedSpace ℬ).presheaf.stalk p)
            ((toSheafedSpace ℬ).presheaf.germ (ProjectiveSpectrum.basicOpen ℬ ((f : (a : A) → B) (↑c.den : A))) p ⋯) :
          (a :
              (↑((toSheafedSpace ℬ).presheaf.obj
                    (Opposite.op (ProjectiveSpectrum.basicOpen ℬ ((f : (a : A) → B) (↑c.den : A))))) :
                Type u)) →
            (↑((toSheafedSpace ℬ).presheaf.stalk p) : Type u))
        (sectionInBasicOpen ℬ p (NumDenSameDeg.map f ⋯ c) :
          (↑(Functor.obj (C := (Opens (↑(top ℬ) : Type u))ᵒᵖ)
                (ObjectProperty.FullSubcategory.obj (P :=
                    (Presheaf.IsSheaf (Opens.grothendieckTopology (↑(top ℬ) : Type u)) :
                      (P : (Opens (↑(top ℬ) : Type u))ᵒᵖ ⥤ CommRingCat) → Prop))
                    (structureSheaf ℬ : TopCat.Sheaf CommRingCat (top ℬ)) :
                  (Opens (↑(top ℬ) : Type u))ᵒᵖ ⥤ CommRingCat)
                (Opposite.op (ProjectiveSpectrum.basicOpen ℬ (↑(NumDenSameDeg.den (NumDenSameDeg.map f ⋯ c)) : B)) :
                  (Opens (↑(top ℬ) : Type u))ᵒᵖ)) :
            Type u)) :
      (↑((toSheafedSpace ℬ).presheaf.stalk p) : Type u))

Tactic:
rfl

Premises used: ProjectiveSpectrum.basicOpen, Set.Mem, setOf, AlgebraicGeometry.sectionInBasicOpen, Set.preimage, Quot.map, Quotient.map', Not, rfl, AlgebraicGeometry.Proj.comapStructureSheafFun