-- 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)
z : (↑(Presheaf.stalk (Sheaf.presheaf (Proj.structureSheaf 𝒜)) x) : Type u_1)
obtain :
  ∀ (U : Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) (hxU : x ∈ U)
    (s :
      ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier)
        (Functor.obj (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
          (op U))),
    Eq (α := (↑(Presheaf.stalk (Sheaf.presheaf (Proj.structureSheaf 𝒜)) x) : Type u_1))
      (homogeneousLocalizationToStalk 𝒜 x
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (X := Presheaf.stalk (Sheaf.presheaf (Proj.structureSheaf 𝒜)) x)
              (stalkToFiberRingHom 𝒜 x) :
            (a : (↑((Proj.structureSheaf 𝒜).presheaf.stalk x) : Type u_1)) → (↑(CommRingCat.of (at x)) : 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 (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                    (op U))
                  (Y := Presheaf.stalk (Sheaf.presheaf (Proj.structureSheaf 𝒜)) x)
                  (Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) U x hxU :
                    Functor.obj
                        (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                        (op U) ⟶
                      Presheaf.stalk (Sheaf.presheaf (Proj.structureSheaf 𝒜)) x) :
                (↑(Functor.obj
                        (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                        (op U)) :
                    Type u_1) →+*
                  (↑(Presheaf.stalk (Sheaf.presheaf (Proj.structureSheaf 𝒜)) x) : Type u_1)) :
              (a : (↑((Proj.structureSheaf 𝒜).presheaf.obj (op U)) : Type u_1)) →
                (↑((Proj.structureSheaf 𝒜).presheaf.stalk x) : Type u_1))
            s)))
      (((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (X :=
              Functor.obj (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                (op U))
              (Y := Presheaf.stalk (Sheaf.presheaf (Proj.structureSheaf 𝒜)) x)
              (Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) U x hxU :
                Functor.obj (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                    (op U) ⟶
                  Presheaf.stalk (Sheaf.presheaf (Proj.structureSheaf 𝒜)) x) :
            (↑(Functor.obj (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                    (op U)) :
                Type u_1) →+*
              (↑(Presheaf.stalk (Sheaf.presheaf (Proj.structureSheaf 𝒜)) x) : Type u_1)) :
          (a : (↑((Proj.structureSheaf 𝒜).presheaf.obj (op U)) : Type u_1)) →
            (↑((Proj.structureSheaf 𝒜).presheaf.stalk x) : Type u_1))
        s)
⊢ homogeneousLocalizationToStalk 𝒜 x
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X := Presheaf.stalk (Sheaf.presheaf (Proj.structureSheaf 𝒜)) x)
            (stalkToFiberRingHom 𝒜 x) :
          (a : (↑((Proj.structureSheaf 𝒜).presheaf.stalk x) : Type u_1)) → (↑(CommRingCat.of (at x)) : Type u_1))
        z) =
    z

Tactic:
obtain ⟨U, hxU, s, rfl⟩ := (Proj.structureSheaf 𝒜).presheaf.exists_germ_eq z

Premises used: TopCat.Presheaf.exists_germ_eq, AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf, TopCat.Sheaf.presheaf, rfl