-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean
@[reassoc]
lemma toStalk_stalkMap_toSpec (f) (x) :
    StructureSheaf.toStalk _ _ ≫ (toSpec 𝒜 f).stalkMap x =
      awayToΓ 𝒜 f ≫ (Proj| pbo f).presheaf.Γgerm x

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 : ↑(Proj.restrict ⋯).toTopCat
⊢ StructureSheaf.toOpen (A⁰_ f) ⊤ ≫
      (Spec A⁰_ f).presheaf.germ ⊤ ((ConcreteCategory.hom (toSpec 𝒜 f).base) x) True.intro ≫
        LocallyRingedSpace.Hom.stalkMap (toSpec 𝒜 f) x =
    awayToΓ 𝒜 f ≫ (Proj.restrict ⋯).presheaf.Γgerm x

Tactic:
rw [LocallyRingedSpace.stalkMap_germ (toSpec 𝒜 f),
  toOpen_toSpec_val_c_app_assoc, Presheaf.germ_res]

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 : ↑(Proj.restrict ⋯).toTopCat
⊢ awayToΓ 𝒜 f ≫ (Proj.restrict ⋯).presheaf.germ ⊤ x ⋯ = awayToΓ 𝒜 f ≫ (Proj.restrict ⋯).presheaf.Γgerm x

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 : ↑(Proj.restrict ⋯).toTopCat
⊢ StructureSheaf.toStalk (↑(CommRingCat.of (A⁰_ f))) ((ConcreteCategory.hom (toSpec 𝒜 f).base) x) ≫
      LocallyRingedSpace.Hom.stalkMap (toSpec 𝒜 f) x =
    awayToΓ 𝒜 f ≫ (Proj.restrict ⋯).presheaf.Γgerm x

Tactic:
rw [StructureSheaf.toStalk, 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 : ↑(Proj.restrict ⋯).toTopCat
⊢ StructureSheaf.toOpen ↑(CommRingCat.of (A⁰_ f)) ⊤ ≫
      («Spec».structureSheaf ↑(CommRingCat.of (A⁰_ f))).presheaf.germ ⊤ ((ConcreteCategory.hom (toSpec 𝒜 f).base) x)
          True.intro ≫
        LocallyRingedSpace.Hom.stalkMap (toSpec 𝒜 f) x =
    awayToΓ 𝒜 f ≫ (Proj.restrict ⋯).presheaf.Γgerm x

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 : ↑(Proj.restrict ⋯).toTopCat
⊢ StructureSheaf.toOpen ↑(CommRingCat.of (A⁰_ f)) ⊤ ≫
      («Spec».structureSheaf ↑(CommRingCat.of (A⁰_ f))).presheaf.germ ⊤ ((ConcreteCategory.hom (toSpec 𝒜 f).base) x)
          True.intro ≫
        LocallyRingedSpace.Hom.stalkMap (toSpec 𝒜 f) x =
    awayToΓ 𝒜 f ≫ (Proj.restrict ⋯).presheaf.Γgerm x

Tactic:
simp_rw [← Spec.locallyRingedSpaceObj_presheaf']

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 : ↑(Proj.restrict ⋯).toTopCat
⊢ StructureSheaf.toOpen (A⁰_ f) ⊤ ≫
      (Spec A⁰_ f).presheaf.germ ⊤ ((ConcreteCategory.hom (toSpec 𝒜 f).base) x) True.intro ≫
        LocallyRingedSpace.Hom.stalkMap (toSpec 𝒜 f) x =
    awayToΓ 𝒜 f ≫ (Proj.restrict ⋯).presheaf.Γgerm x

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 : ↑(Proj.restrict ⋯).toTopCat
⊢ awayToΓ 𝒜 f ≫ (Proj.restrict ⋯).presheaf.germ ⊤ x ⋯ = awayToΓ 𝒜 f ≫ (Proj.restrict ⋯).presheaf.Γgerm x

Tactic:
rfl

Result:
no goals