-- Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean
theorem toStalk_stalkMap_toΓSpec (x : X) :
    toStalk _ _ ≫ X.toΓSpecSheafedSpace.stalkMap x = X.presheaf.Γgerm x

Proof state:
X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ (ConcreteCategory.hom X.toΓSpecSheafedSpace.base) x ∈ ⊤

Tactic:
trivial

Result:
no goals

Proof state:
X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ toStalk (↑(unop (op (Γ.obj (op X))))) ((ConcreteCategory.hom X.toΓSpecSheafedSpace.base) x) ≫
      PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace x =
    X.presheaf.Γgerm x

Tactic:
rw [PresheafedSpace.Hom.stalkMap,
  ← toOpen_germ _ (basicOpen (1 : Γ.obj (op X))) _ (by rw [basicOpen_one]; trivial),
  ← Category.assoc, Category.assoc (toOpen _ _), stalkFunctor_map_germ, ← Category.assoc,
  toΓSpecSheafedSpace_app_spec, Γgerm]

Result:
X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ (X.toToΓSpecMapBasicOpen 1 ≫
        ((pushforward CommRingCat X.toΓSpecSheafedSpace.base).obj X.presheaf).germ (basicOpen 1)
          ((ConcreteCategory.hom X.toΓSpecSheafedSpace.base) x) ⋯) ≫
      stalkPushforward CommRingCat X.toΓSpecSheafedSpace.base X.presheaf x =
    X.presheaf.germ ⊤ x True.intro

Proof state:
X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ (X.toToΓSpecMapBasicOpen 1 ≫
        ((pushforward CommRingCat X.toΓSpecSheafedSpace.base).obj X.presheaf).germ (basicOpen 1)
          ((ConcreteCategory.hom X.toΓSpecSheafedSpace.base) x) ⋯) ≫
      stalkPushforward CommRingCat X.toΓSpecSheafedSpace.base X.presheaf x =
    ((pushforward CommRingCat ?m.56082).obj X.presheaf).germ ⊤ ((ConcreteCategory.hom ?m.56082) x) True.intro ≫
      stalkPushforward CommRingCat ?m.56082 X.presheaf x

X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ TopCat

X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ ↑X.toPresheafedSpace ⟶ ?m.56081

Tactic:
congr 1

Result:
case e_a
X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ X.toToΓSpecMapBasicOpen 1 ≫
      ((pushforward CommRingCat X.toΓSpecSheafedSpace.base).obj X.presheaf).germ (basicOpen 1)
        ((ConcreteCategory.hom X.toΓSpecSheafedSpace.base) x) ⋯ =
    ((pushforward CommRingCat X.toΓSpecSheafedSpace.base).obj X.presheaf).germ ⊤
      ((ConcreteCategory.hom X.toΓSpecSheafedSpace.base) x) True.intro

Proof state:
case e_a
X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ X.toToΓSpecMapBasicOpen 1 ≫
      ((pushforward CommRingCat X.toΓSpecSheafedSpace.base).obj X.presheaf).germ (basicOpen 1)
        ((ConcreteCategory.hom X.toΓSpecSheafedSpace.base) x) ⋯ =
    ((pushforward CommRingCat X.toΓSpecSheafedSpace.base).obj X.presheaf).germ ⊤
      ((ConcreteCategory.hom X.toΓSpecSheafedSpace.base) x) True.intro

Tactic:
exact (X.toΓSpecBase _* X.presheaf).germ_res le_top.hom _ _

Result:
no goals

Proof state:
X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ (X.toToΓSpecMapBasicOpen 1 ≫
        ((pushforward CommRingCat X.toΓSpecSheafedSpace.base).obj X.presheaf).germ (basicOpen 1)
          ((ConcreteCategory.hom X.toΓSpecSheafedSpace.base) x) ⋯) ≫
      stalkPushforward CommRingCat X.toΓSpecSheafedSpace.base X.presheaf x =
    X.presheaf.germ ⊤ x True.intro

Tactic:
erw [← stalkPushforward_germ _ _ X.presheaf ⊤]

Result:
X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ (X.toToΓSpecMapBasicOpen 1 ≫
        ((pushforward CommRingCat X.toΓSpecSheafedSpace.base).obj X.presheaf).germ (basicOpen 1)
          ((ConcreteCategory.hom X.toΓSpecSheafedSpace.base) x) ⋯) ≫
      stalkPushforward CommRingCat X.toΓSpecSheafedSpace.base X.presheaf x =
    ((pushforward CommRingCat ?m.56082).obj X.presheaf).germ ⊤ ((ConcreteCategory.hom ?m.56082) x) True.intro ≫
      stalkPushforward CommRingCat ?m.56082 X.presheaf x

X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ TopCat

X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ ↑X.toPresheafedSpace ⟶ ?m.56081

Proof state:
X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ (ConcreteCategory.hom X.toΓSpecSheafedSpace.base) x ∈ basicOpen 1

Tactic:
rw [basicOpen_one]

Result:
X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ (ConcreteCategory.hom X.toΓSpecSheafedSpace.base) x ∈ ⊤