-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean
lemma stalkMap_toSpec (f) (x : pbo f) {m} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) :
    (toSpec 𝒜 f).stalkMap x =
      (specStalkEquiv 𝒜 f x f_deg hm).hom ≫ (Proj.stalkIso' 𝒜 x.1).toCommRingCatIso.inv ≫
      ((Proj.toLocallyRingedSpace 𝒜).restrictStalkIso (Opens.isOpenEmbedding _) x).inv :=
  CommRingCat.hom_ext <|
    IsLocalization.ringHom_ext (R := A⁰_ f) ((toSpec 𝒜 f).base x).asIdeal.primeCompl
      (S := (Spec.structureSheaf (A⁰_ f)).presheaf.stalk ((toSpec 𝒜 f).base x)) <|
      CommRingCat.hom_ext_iff.mp <|
        (toStalk_stalkMap_toSpec _ _ _).trans <| by
        rw [awayToΓ_ΓToStalk, ← toStalk_specStalkEquiv, Category.assoc]; rfl

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
⊢ awayToΓ 𝒜 f ≫ (Proj.restrict ⋯).presheaf.Γgerm x =
    {
      hom' :=
        {
          toFun :=
            ⇑(CommRingCat.Hom.hom
                  ((specStalkEquiv 𝒜 f x f_deg hm).hom ≫
                    («Proj».stalkIso' 𝒜 ↑x).toCommRingCatIso.inv ≫ (Proj.restrictStalkIso ⋯ x).inv)) ∘
              ⇑(algebraMap (A⁰_ f)
                  ↑((«Spec».structureSheaf (A⁰_ f)).presheaf.stalk ((ConcreteCategory.hom (toSpec 𝒜 f).base) x))),
          map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } }

Tactic:
rw [awayToΓ_ΓToStalk, ← toStalk_specStalkEquiv, Category.assoc]

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
⊢ StructureSheaf.toStalk (A⁰_ f) ((ConcreteCategory.hom (toSpec 𝒜 f).base) x) ≫
      (specStalkEquiv 𝒜 f x ?f_deg ?hm).hom ≫
        («Proj».stalkIso' 𝒜 ↑x).toCommRingCatIso.inv ≫ (Proj.restrictStalkIso ⋯ x).inv =
    {
      hom' :=
        {
          toFun :=
            ⇑(CommRingCat.Hom.hom
                  ((specStalkEquiv 𝒜 f x f_deg hm).hom ≫
                    («Proj».stalkIso' 𝒜 ↑x).toCommRingCatIso.inv ≫ (Proj.restrictStalkIso ⋯ x).inv)) ∘
              ⇑(algebraMap (A⁰_ f)
                  ↑((«Spec».structureSheaf (A⁰_ f)).presheaf.stalk ((ConcreteCategory.hom (toSpec 𝒜 f).base) x))),
          map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } }

case m
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
⊢ ℕ

case f_deg
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
⊢ f ∈ 𝒜 ?m

case hm
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
⊢ 0 < ?m

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
⊢ StructureSheaf.toStalk (A⁰_ f) ((ConcreteCategory.hom (toSpec 𝒜 f).base) x) ≫
      (specStalkEquiv 𝒜 f x ?f_deg ?hm).hom ≫
        («Proj».stalkIso' 𝒜 ↑x).toCommRingCatIso.inv ≫ (Proj.restrictStalkIso ⋯ x).inv =
    {
      hom' :=
        {
          toFun :=
            ⇑(CommRingCat.Hom.hom
                  ((specStalkEquiv 𝒜 f x f_deg hm).hom ≫
                    («Proj».stalkIso' 𝒜 ↑x).toCommRingCatIso.inv ≫ (Proj.restrictStalkIso ⋯ x).inv)) ∘
              ⇑(algebraMap (A⁰_ f)
                  ↑((«Spec».structureSheaf (A⁰_ f)).presheaf.stalk ((ConcreteCategory.hom (toSpec 𝒜 f).base) x))),
          map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } }

case m
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
⊢ ℕ

case f_deg
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
⊢ f ∈ 𝒜 ?m

case hm
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
⊢ 0 < ?m

Tactic:
rfl

Result:
no goals