-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (goal)
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
⊢ 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)))
have a : ∀ (a : A⁰_ f),
  Eq (α :=
    (↑((Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                sorry).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))
                                sorry).toPresheafedSpace :
                          TopCat))
                        (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f))) :
                      (a : (↑(↑(Proj.restrict sorry).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))
                                  sorry).toPresheafedSpace :
                            TopCat))
                          (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f))) :
                        (a : (↑(↑(Proj.restrict sorry).toPresheafedSpace : TopCat) : Type u_1)) →
                          (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
                      x)) :
                Type u_1)) :
          (a : A⁰_ f) → (↑((Proj.restrict sorry).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))
                  sorry).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))
                                sorry).toPresheafedSpace :
                          TopCat))
                        (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f))) :
                      (a : (↑(↑(Proj.restrict sorry).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 sorry 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))
                                  sorry).toPresheafedSpace :
                            TopCat))
                          (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f))) :
                        (a : (↑(↑(Proj.restrict sorry).toPresheafedSpace : TopCat) : Type u_1)) →
                          (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
                      x)) :
                Type u_1)) :
          (a : A⁰_ f) → (↑((Proj.restrict sorry).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))
                  sorry).presheaf.stalk
            x) :
        Type u_1))
Tactic: ext a