-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
a :
  ∀ (a : A⁰_ f),
    Eq (α :=
      (↑((Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                  ⋯).presheaf.stalk
            x) :
        Type u_1))
      ((RingHom.comp (β :=
              (↑(Presheaf.stalk (X := PrimeSpectrum.Top (A⁰_ f)) (Sheaf.presheaf («Spec».structureSheaf (A⁰_ f)))
                    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                          carrier) (X :=
                          (↑(Proj.restrict (U :=
                                  Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                                  ⋯).toPresheafedSpace :
                            TopCat))
                          (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f))) :
                        (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
                          (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
                      x)) :
                Type u_1))
              (CommRingCat.Hom.hom (LocallyRingedSpace.Hom.stalkMap (toSpec 𝒜 f) x))
              (algebraMap (A⁰_ f)
                (↑(Presheaf.stalk (X := PrimeSpectrum.Top (A⁰_ f)) (Sheaf.presheaf («Spec».structureSheaf (A⁰_ f)))
                      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1)))
                            (CC := carrier) (X :=
                            (↑(Proj.restrict (U :=
                                    Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                                    ⋯).toPresheafedSpace :
                              TopCat))
                            (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f))) :
                          (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
                            (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
                        x)) :
                  Type u_1)) :
            (a : A⁰_ f) → (↑((Proj.restrict ⋯).presheaf.stalk x) : Type u_1))
          a :
        (↑((Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                    ⋯).presheaf.stalk
              x) :
          Type u_1))
      ((RingHom.comp (β :=
              (↑(Presheaf.stalk (X := PrimeSpectrum.Top (A⁰_ f)) (Sheaf.presheaf («Spec».structureSheaf (A⁰_ f)))
                    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                          carrier) (X :=
                          (↑(Proj.restrict (U :=
                                  Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                                  ⋯).toPresheafedSpace :
                            TopCat))
                          (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f))) :
                        (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
                          (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
                      x)) :
                Type u_1))
              (CommRingCat.Hom.hom
                (Iso.hom (specStalkEquiv 𝒜 f x f_deg hm) ≫
                  Iso.inv (RingEquiv.toCommRingCatIso («Proj».stalkIso' 𝒜 (↑x : ProjectiveSpectrum 𝒜))) ≫
                    Iso.inv (Proj.restrictStalkIso ⋯ x)))
              (algebraMap (A⁰_ f)
                (↑(Presheaf.stalk (X := PrimeSpectrum.Top (A⁰_ f)) (Sheaf.presheaf («Spec».structureSheaf (A⁰_ f)))
                      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1)))
                            (CC := carrier) (X :=
                            (↑(Proj.restrict (U :=
                                    Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                                    ⋯).toPresheafedSpace :
                              TopCat))
                            (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f))) :
                          (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
                            (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
                        x)) :
                  Type u_1)) :
            (a : A⁰_ f) → (↑((Proj.restrict ⋯).presheaf.stalk x) : Type u_1))
          a :
        (↑((Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                    ⋯).presheaf.stalk
              x) :
          Type u_1))
⊢ Eq (α :=
    (A⁰_ f) →+*
      (↑((Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                  ⋯).presheaf.stalk
            x) :
        Type u_1))
    (RingHom.comp (β :=
      (↑(Presheaf.stalk (X := PrimeSpectrum.Top (A⁰_ f)) (Sheaf.presheaf («Spec».structureSheaf (A⁰_ f)))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                  carrier) (X :=
                  (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                          ⋯).toPresheafedSpace :
                    TopCat))
                  (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f))) :
                (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
                  (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
              x)) :
        Type u_1))
      (CommRingCat.Hom.hom (LocallyRingedSpace.Hom.stalkMap (toSpec 𝒜 f) x))
      (algebraMap (A⁰_ f)
        (↑(Presheaf.stalk (X := PrimeSpectrum.Top (A⁰_ f)) (Sheaf.presheaf («Spec».structureSheaf (A⁰_ f)))
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                    carrier) (X :=
                    (↑(Proj.restrict (U :=
                            Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                            ⋯).toPresheafedSpace :
                      TopCat))
                    (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f))) :
                  (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
                    (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
                x)) :
          Type u_1)))
    (RingHom.comp (β :=
      (↑(Presheaf.stalk (X := PrimeSpectrum.Top (A⁰_ f)) (Sheaf.presheaf («Spec».structureSheaf (A⁰_ f)))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                  carrier) (X :=
                  (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                          ⋯).toPresheafedSpace :
                    TopCat))
                  (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f))) :
                (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
                  (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
              x)) :
        Type u_1))
      (CommRingCat.Hom.hom
        (Iso.hom (specStalkEquiv 𝒜 f x f_deg hm) ≫
          Iso.inv (RingEquiv.toCommRingCatIso («Proj».stalkIso' 𝒜 (↑x : ProjectiveSpectrum 𝒜))) ≫
            Iso.inv (Proj.restrictStalkIso ⋯ x)))
      (algebraMap (A⁰_ f)
        (↑(Presheaf.stalk (X := PrimeSpectrum.Top (A⁰_ f)) (Sheaf.presheaf («Spec».structureSheaf (A⁰_ f)))
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                    carrier) (X :=
                    (↑(Proj.restrict (U :=
                            Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                            ⋯).toPresheafedSpace :
                      TopCat))
                    (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f))) :
                  (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
                    (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
                x)) :
          Type u_1)))

Tactic:
ext a