-- 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))))
hf₁ :
  Eq (α := Localization (M := B) p.asHomogeneousIdeal.toIdeal.primeCompl)
    (Localization.mk ((f : (a : A) → B) (↑c.num : A))
        (Subtype.mk (p := fun (x : B) ↦ x ∈ p.asHomogeneousIdeal.toIdeal.primeCompl) ((f : (a : A) → B) (↑c.den : A))
          ⋯) :
      Localization (M := B) p.asHomogeneousIdeal.toIdeal.primeCompl)
    (val (ι := ℕ) (σ := τ) (𝒜 := ℬ)
        ((CommRingCat.Hom.hom
              (CommRingCat.ofHom
                (↑(stalkIso' ℬ p) :
                  (↑((structureSheaf ℬ).presheaf.stalk p) : Type u) →+* AtPrime ℬ p.asHomogeneousIdeal.toIdeal)) :
            (a : (↑((Proj ℬ).presheaf.stalk p) : Type u)) → AtPrime ℬ p.asHomogeneousIdeal.toIdeal)
          ((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)))) :
      Localization (M := B) p.asHomogeneousIdeal.toIdeal.primeCompl)
⊢ Eq (α := Localization (M := B) p.asHomogeneousIdeal.toIdeal.primeCompl)
    (Localization.mk ((f : (a : A) → B) (↑c.num : A))
        (Subtype.mk (p := fun (x : B) ↦ x ∈ p.asHomogeneousIdeal.toIdeal.primeCompl) ((f : (a : A) → B) (↑c.den : A))
          ⋯) :
      Localization (M := B) p.asHomogeneousIdeal.toIdeal.primeCompl)
    (val (ι := ℕ) (σ := τ) (𝒜 := ℬ)
        ((CommRingCat.Hom.hom
              (CommRingCat.ofHom
                (↑(stalkIso' ℬ p) :
                  (↑((structureSheaf ℬ).presheaf.stalk p) : Type u) →+* AtPrime ℬ p.asHomogeneousIdeal.toIdeal)) :
            (a : (↑((Proj ℬ).presheaf.stalk p) : Type u)) → AtPrime ℬ p.asHomogeneousIdeal.toIdeal)
          ((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))))
                      (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))))
                    (ProjectiveSpectrum.basicOpen 𝒜 (↑c.den : A)))
                  p ⋯) :
              (a :
                  (↑((toSheafedSpace ℬ).presheaf.obj
                        (Opposite.op
                          ((Opens.map (sheafedSpaceMap f hf).hom.base).obj
                            (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 :=
                    (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))))
                          (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)) →
                    (↑((toSheafedSpace ℬ).presheaf.obj
                          (Opposite.op
                            ((Opens.map (sheafedSpaceMap f hf).hom.base).obj
                              (ProjectiveSpectrum.basicOpen 𝒜 (↑c.den : A))))) :
                      Type u))
                (sectionInBasicOpen 𝒜
                  (((ProjectiveSpectrum.comap f hf : C(ProjectiveSpectrum ℬ, ProjectiveSpectrum 𝒜)) :
                      (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
                    p)
                  c) :
              (↑((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))))
                        (ProjectiveSpectrum.basicOpen 𝒜 (↑c.den : A))))) :
                Type u)))) :
      Localization (M := B) p.asHomogeneousIdeal.toIdeal.primeCompl)

Tactic:
erw [germ_map_sectionInBasicOpen]

Premises used: AlgebraicGeometry.Proj.germ_map_sectionInBasicOpen