awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
this :
  CommRingCat.ofHom
        (algebraMap (↑(Γ.obj (op X)) : Type u)
          (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(unop (op (Γ.obj (op X)))) : Type u)) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf
                (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(unop (op (Γ.obj (op X)))) : Type u)) : Type u)))
              (structureSheafInType (↑(unop (op (Γ.obj (op X)))) : Type u) (↑(unop (op (Γ.obj (op X)))) : Type u)))
            (op ⊤))) ≫
      X.toΓSpecSheafedSpace.hom.c.app (op ⊤) =
    X.presheaf.map ((Opens.map X.toΓSpecBase).obj ⊤).leTop.op
e_1 :
  (Γ.obj (op X) ⟶ (Functor.obj (pushforward CommRingCat X.toΓSpec.base) X.presheaf).obj (op ⊤)) =
    (CommRingCat.of (↑(Γ.obj (op X)) : Type u) ⟶
      (Functor.obj (pushforward CommRingCat X.toΓSpecSheafedSpace.hom.base) X.presheaf).obj (op ⊤))
⊢ 𝟙 (Γ.obj (op X)) = X.presheaf.map ((Opens.map X.toΓSpecBase).obj ⊤).leTop.op

Tactic:
exact (X.presheaf.map_id ..).symm

Premises used: AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, CategoryTheory.Functor.map_id, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
symm :
  X.toΓSpec ≫ (Γ.rightOp ⋙ Spec.toLocallyRingedSpace).map f =
    CategoryTheory.Functor.map (𝟭 LocallyRingedSpace) f ≫ Y.toΓSpec
⊢ CategoryTheory.Functor.map (𝟭 LocallyRingedSpace) f ≫ Y.toΓSpec =
    X.toΓSpec ≫ (Γ.rightOp ⋙ Spec.toLocallyRingedSpace).map f

Tactic:
symm
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
w :
  PresheafedSpace.Hom.base (Hom.toHom (Functor.obj (𝟭 LocallyRingedSpace) X).toΓSpec) ≫
      (Spec.locallyRingedSpaceMap (Γ.rightOp.map f).unop).base =
    PresheafedSpace.Hom.base (Hom.toHom (CategoryTheory.Functor.map (𝟭 LocallyRingedSpace) f ≫ Y.toΓSpec))
h :
  ∀ (r : (↑(unop (Γ.rightOp.obj Y)) : Type u)),
    Eq (α :=
      unop (Γ.rightOp.obj Y) ⟶
        (Functor.obj (𝟭 LocallyRingedSpace) X).presheaf.obj
          (op
            (Functor.obj (C :=
              Opens (↑(↑(Spec.locallyRingedSpaceObj (unop (Γ.rightOp.obj Y))).toPresheafedSpace : TopCat) : Type u))
              (Opens.map
                (PresheafedSpace.Hom.base
                  (Hom.toHom (CategoryTheory.Functor.map (𝟭 LocallyRingedSpace) f ≫ Y.toΓSpec))))
              (basicOpen r))))
      ((Γ.rightOp.map f).unop ≫ (Functor.obj (𝟭 LocallyRingedSpace) X).presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
      (CommRingCat.ofHom
          (algebraMap (↑(unop (Γ.rightOp.obj Y)) : Type u)
            (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(unop (Γ.rightOp.obj Y)) : Type u)) : Type u))ᵒᵖ)
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf
                  (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(unop (Γ.rightOp.obj Y)) : Type u)) : Type u)))
                (structureSheafInType (↑(unop (Γ.rightOp.obj Y)) : Type u) (↑(unop (Γ.rightOp.obj Y)) : Type u)))
              (op (basicOpen r)))) ≫
        NatTrans.app
          (PresheafedSpace.Hom.c (Hom.toHom (CategoryTheory.Functor.map (𝟭 LocallyRingedSpace) f ≫ Y.toΓSpec)))
          (op (basicOpen r)))
⊢ X.toΓSpec ≫ (Γ.rightOp ⋙ Spec.toLocallyRingedSpace).map f =
    CategoryTheory.Functor.map (𝟭 LocallyRingedSpace) f ≫ Y.toΓSpec

Tactic:
apply LocallyRingedSpace.comp_ring_hom_ext

Premises used: AlgebraicGeometry.LocallyRingedSpace.comp_ring_hom_ext
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
w :
  ∀ (x : (↑(↑(Functor.obj (𝟭 LocallyRingedSpace) X).toPresheafedSpace : TopCat) : Type u)),
    Eq (α := (↑(↑(Spec.locallyRingedSpaceObj (unop (Γ.rightOp.obj Y))).toPresheafedSpace : TopCat) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (PresheafedSpace.Hom.base (Hom.toHom (Functor.obj (𝟭 LocallyRingedSpace) X).toΓSpec) ≫
                (Spec.locallyRingedSpaceMap (Γ.rightOp.map f).unop).base) :
            (a : (↑(↑((𝟭 LocallyRingedSpace).obj X).toPresheafedSpace : TopCat) : Type u)) →
              (↑(↑(Spec.locallyRingedSpaceObj (unop (Γ.rightOp.obj Y))).toPresheafedSpace : TopCat) : Type u))
          x :
        (↑(↑(Spec.locallyRingedSpaceObj (unop (Γ.rightOp.obj Y))).toPresheafedSpace : TopCat) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (X := (↑(Functor.obj (𝟭 LocallyRingedSpace) X).toPresheafedSpace : TopCat)) (Y :=
              (↑(Spec.locallyRingedSpaceObj (unop (Γ.rightOp.obj Y))).toPresheafedSpace : TopCat))
              (PresheafedSpace.Hom.base (Hom.toHom (CategoryTheory.Functor.map (𝟭 LocallyRingedSpace) f ≫ Y.toΓSpec))) :
            (a : (↑(↑((𝟭 LocallyRingedSpace).obj X).toPresheafedSpace : TopCat) : Type u)) →
              (↑(↑(Spec.locallyRingedSpaceObj (unop (Γ.rightOp.obj Y))).toPresheafedSpace : TopCat) : Type u))
          x :
        (↑(↑(Spec.locallyRingedSpaceObj (unop (Γ.rightOp.obj Y))).toPresheafedSpace : TopCat) : Type u))
⊢ PresheafedSpace.Hom.base (Hom.toHom (Functor.obj (𝟭 LocallyRingedSpace) X).toΓSpec) ≫
      (Spec.locallyRingedSpaceMap (Γ.rightOp.map f).unop).base =
    PresheafedSpace.Hom.base (Hom.toHom (CategoryTheory.Functor.map (𝟭 LocallyRingedSpace) f ≫ Y.toΓSpec))

Tactic:
ext1 x
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
x : (↑(↑(Functor.obj (𝟭 LocallyRingedSpace) X).toPresheafedSpace : TopCat) : Type u)
w :
  Eq (α := PrimeSpectrum (↑(Y.presheaf.obj (op ⊤)) : Type u))
    (((TopCat.Hom.hom (Spec.topMap (f.c.app (op ⊤))) :
            C((↑(Spec.topObj (X.presheaf.obj (op ⊤))) : Type u), (↑(Spec.topObj (Y.presheaf.obj (op ⊤))) : Type u))) :
          (a : PrimeSpectrum (↑(X.presheaf.obj (op ⊤)) : Type u)) → PrimeSpectrum (↑(Y.presheaf.obj (op ⊤)) : Type u))
        ((TopCat.Hom.hom X.toΓSpecBase :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → PrimeSpectrum (↑(X.presheaf.obj (op ⊤)) : Type u))
          x) :
      PrimeSpectrum (↑(Y.presheaf.obj (op ⊤)) : Type u))
    ((TopCat.Hom.hom Y.toΓSpecBase :
          (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u)) → PrimeSpectrum (↑(Y.presheaf.obj (op ⊤)) : Type u))
        ((TopCat.Hom.hom f.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
          x) :
      PrimeSpectrum (↑(Y.presheaf.obj (op ⊤)) : Type u))
⊢ Eq (α := (↑(↑(Spec.locallyRingedSpaceObj (unop (Γ.rightOp.obj Y))).toPresheafedSpace : TopCat) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (PresheafedSpace.Hom.base (Hom.toHom (Functor.obj (𝟭 LocallyRingedSpace) X).toΓSpec) ≫
              (Spec.locallyRingedSpaceMap (Γ.rightOp.map f).unop).base) :
          (a : (↑(↑((𝟭 LocallyRingedSpace).obj X).toPresheafedSpace : TopCat) : Type u)) →
            (↑(↑(Spec.locallyRingedSpaceObj (unop (Γ.rightOp.obj Y))).toPresheafedSpace : TopCat) : Type u))
        x :
      (↑(↑(Spec.locallyRingedSpaceObj (unop (Γ.rightOp.obj Y))).toPresheafedSpace : TopCat) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (X :=
            (↑(Functor.obj (𝟭 LocallyRingedSpace) X).toPresheafedSpace : TopCat)) (Y :=
            (↑(Spec.locallyRingedSpaceObj (unop (Γ.rightOp.obj Y))).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base (Hom.toHom (CategoryTheory.Functor.map (𝟭 LocallyRingedSpace) f ≫ Y.toΓSpec))) :
          (a : (↑(↑((𝟭 LocallyRingedSpace).obj X).toPresheafedSpace : TopCat) : Type u)) →
            (↑(↑(Spec.locallyRingedSpaceObj (unop (Γ.rightOp.obj Y))).toPresheafedSpace : TopCat) : Type u))
        x :
      (↑(↑(Spec.locallyRingedSpaceObj (unop (Γ.rightOp.obj Y))).toPresheafedSpace : TopCat) : Type u))

Tactic:
dsimp
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
x : (↑(↑(Functor.obj (𝟭 LocallyRingedSpace) X).toPresheafedSpace : TopCat) : Type u)
w :
  PrimeSpectrum.comap (CommRingCat.Hom.hom (f.c.app (op ⊤))) (X.toΓSpecFun x) =
    Y.toΓSpecFun
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            f.base :
          (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
        x)
⊢ Eq (α := PrimeSpectrum (↑(Y.presheaf.obj (op ⊤)) : Type u))
    (((TopCat.Hom.hom (Spec.topMap (f.c.app (op ⊤))) :
            C((↑(Spec.topObj (X.presheaf.obj (op ⊤))) : Type u), (↑(Spec.topObj (Y.presheaf.obj (op ⊤))) : Type u))) :
          (a : PrimeSpectrum (↑(X.presheaf.obj (op ⊤)) : Type u)) → PrimeSpectrum (↑(Y.presheaf.obj (op ⊤)) : Type u))
        ((TopCat.Hom.hom X.toΓSpecBase :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → PrimeSpectrum (↑(X.presheaf.obj (op ⊤)) : Type u))
          x) :
      PrimeSpectrum (↑(Y.presheaf.obj (op ⊤)) : Type u))
    ((TopCat.Hom.hom Y.toΓSpecBase :
          (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u)) → PrimeSpectrum (↑(Y.presheaf.obj (op ⊤)) : Type u))
        ((TopCat.Hom.hom f.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
          x) :
      PrimeSpectrum (↑(Y.presheaf.obj (op ⊤)) : Type u))

Tactic:
change PrimeSpectrum.comap (f.c.app (op ⊤)).hom (X.toΓSpecFun x) = Y.toΓSpecFun (f.base x)

Premises used: AlgebraicGeometry.LocallyRingedSpace.toΓSpecFun, CommRingCat.Hom.hom, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, Opposite.op, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.PresheafedSpace.Hom.c, PrimeSpectrum.comap, Top.top, DFunLike.coe, CategoryTheory.NatTrans.app
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
x : (↑(↑(Functor.obj (𝟭 LocallyRingedSpace) X).toPresheafedSpace : TopCat) : Type u)
w :
  PrimeSpectrum.comap (CommRingCat.Hom.hom (f.c.app (op ⊤)))
      (PrimeSpectrum.comap (S := (↑(X.presheaf.stalk x) : Type u)) (CommRingCat.Hom.hom (X.presheaf.Γgerm x))
        (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u))) =
    PrimeSpectrum.comap (S :=
      (↑(Y.presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                  TopCat.carrier) f.base :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
              x)) :
        Type u))
      (CommRingCat.Hom.hom
        (Y.presheaf.Γgerm
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                f.base :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
            x)))
      (IsLocalRing.closedPoint
        (↑(Y.presheaf.stalk
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                    TopCat.carrier) f.base :
                  (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                x)) :
          Type u))
⊢ PrimeSpectrum.comap (CommRingCat.Hom.hom (f.c.app (op ⊤))) (X.toΓSpecFun x) =
    Y.toΓSpecFun
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            f.base :
          (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
        x)

Tactic:
dsimp [toΓSpecFun]

Premises used: AlgebraicGeometry.LocallyRingedSpace.toΓSpecFun
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
x : (↑(↑(Functor.obj (𝟭 LocallyRingedSpace) X).toPresheafedSpace : TopCat) : Type u)
w :
  PrimeSpectrum.comap (S := (↑(X.presheaf.stalk x) : Type u))
      (CommRingCat.Hom.hom (f.c.app (op ⊤) ≫ X.presheaf.Γgerm x))
      (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u)) =
    PrimeSpectrum.comap
      (CommRingCat.Hom.hom
        (Y.presheaf.Γgerm
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                  TopCat.carrier) f.base :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
              x) ≫
          Hom.stalkMap f x))
      (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u))
⊢ PrimeSpectrum.comap (CommRingCat.Hom.hom (f.c.app (op ⊤)))
      (PrimeSpectrum.comap (S := (↑(X.presheaf.stalk x) : Type u)) (CommRingCat.Hom.hom (X.presheaf.Γgerm x))
        (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u))) =
    PrimeSpectrum.comap (S :=
      (↑(Y.presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                  TopCat.carrier) f.base :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
              x)) :
        Type u))
      (CommRingCat.Hom.hom
        (Y.presheaf.Γgerm
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                f.base :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
            x)))
      (IsLocalRing.closedPoint
        (↑(Y.presheaf.stalk
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                    TopCat.carrier) f.base :
                  (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                x)) :
          Type u))

Tactic:
rw [← IsLocalRing.comap_closedPoint (f.stalkMap x).hom, ←
        PrimeSpectrum.comap_comp_apply, ← PrimeSpectrum.comap_comp_apply,
        ← CommRingCat.hom_comp, ← CommRingCat.hom_comp]

Premises used: CommRingCat.Hom.hom, PrimeSpectrum.comap_comp_apply, IsLocalRing.comap_closedPoint, CommRingCat.hom_comp, AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
x : (↑(↑(Functor.obj (𝟭 LocallyRingedSpace) X).toPresheafedSpace : TopCat) : Type u)
w :
  f.c.app (op ⊤) ≫ X.presheaf.Γgerm x =
    Y.presheaf.Γgerm
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              f.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
          x) ≫
      Hom.stalkMap f x
⊢ PrimeSpectrum.comap (S := (↑(X.presheaf.stalk x) : Type u))
      (CommRingCat.Hom.hom (f.c.app (op ⊤) ≫ X.presheaf.Γgerm x))
      (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u)) =
    PrimeSpectrum.comap
      (CommRingCat.Hom.hom
        (Y.presheaf.Γgerm
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                  TopCat.carrier) f.base :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
              x) ≫
          Hom.stalkMap f x))
      (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u))

Tactic:
congr 2
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
x : (↑(↑(Functor.obj (𝟭 LocallyRingedSpace) X).toPresheafedSpace : TopCat) : Type u)
⊢ f.c.app (op ⊤) ≫ X.presheaf.Γgerm x =
    Y.presheaf.Γgerm
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              f.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
          x) ≫
      Hom.stalkMap f x

Tactic:
(PresheafedSpace.stalkMap_germ f.1 ⊤ x trivial).symm

Premises used: AlgebraicGeometry.PresheafedSpace.stalkMap_germ, trivial, Set.Mem, Set.univ, setOf, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, Set.preimage, Top.top, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
x : (↑(↑(Functor.obj (𝟭 LocallyRingedSpace) X).toPresheafedSpace : TopCat) : Type u)
⊢ f.c.app (op ⊤) ≫ X.presheaf.Γgerm x =
    Y.presheaf.Γgerm
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              f.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
          x) ≫
      Hom.stalkMap f x

Tactic:
exact (PresheafedSpace.stalkMap_germ f.1 ⊤ x trivial).symm

Premises used: AlgebraicGeometry.PresheafedSpace.stalkMap_germ, trivial, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, Top.top, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
r : (↑(unop (Γ.rightOp.obj Y)) : Type u)
h :
  Eq (α :=
    unop (Γ.rightOp.obj Y) ⟶
      (Functor.obj (𝟭 LocallyRingedSpace) X).presheaf.obj
        (op
          (Functor.obj (C :=
            Opens (↑(↑(Spec.locallyRingedSpaceObj (unop (Γ.rightOp.obj Y))).toPresheafedSpace : TopCat) : Type u))
            (Opens.map
              (PresheafedSpace.Hom.base (Hom.toHom (CategoryTheory.Functor.map (𝟭 LocallyRingedSpace) f ≫ Y.toΓSpec))))
            (basicOpen r))))
    ((Γ.rightOp.map f).unop ≫ (Functor.obj (𝟭 LocallyRingedSpace) X).presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
    ((CommRingCat.ofHom
          (algebraMap (↑(unop (Γ.rightOp.obj Y)) : Type u)
            (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(unop (Γ.rightOp.obj Y)) : Type u)) : Type u))ᵒᵖ)
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf
                  (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(unop (Γ.rightOp.obj Y)) : Type u)) : Type u)))
                (structureSheafInType (↑(unop (Γ.rightOp.obj Y)) : Type u) (↑(unop (Γ.rightOp.obj Y)) : Type u)))
              (op (basicOpen r)))) ≫
        Y.toΓSpec.c.app (op (basicOpen r))) ≫
      NatTrans.app (PresheafedSpace.Hom.c (Hom.toHom (CategoryTheory.Functor.map (𝟭 LocallyRingedSpace) f)))
        (op ((Opens.map Y.toΓSpec.base).obj (unop (op (basicOpen r))))))
⊢ Eq (α :=
    unop (Γ.rightOp.obj Y) ⟶
      (Functor.obj (𝟭 LocallyRingedSpace) X).presheaf.obj
        (op
          (Functor.obj (C :=
            Opens (↑(↑(Spec.locallyRingedSpaceObj (unop (Γ.rightOp.obj Y))).toPresheafedSpace : TopCat) : Type u))
            (Opens.map
              (PresheafedSpace.Hom.base (Hom.toHom (CategoryTheory.Functor.map (𝟭 LocallyRingedSpace) f ≫ Y.toΓSpec))))
            (basicOpen r))))
    ((Γ.rightOp.map f).unop ≫ (Functor.obj (𝟭 LocallyRingedSpace) X).presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
    (CommRingCat.ofHom
        (algebraMap (↑(unop (Γ.rightOp.obj Y)) : Type u)
          (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(unop (Γ.rightOp.obj Y)) : Type u)) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf
                (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(unop (Γ.rightOp.obj Y)) : Type u)) : Type u)))
              (structureSheafInType (↑(unop (Γ.rightOp.obj Y)) : Type u) (↑(unop (Γ.rightOp.obj Y)) : Type u)))
            (op (basicOpen r)))) ≫
      NatTrans.app (PresheafedSpace.Hom.c (Hom.toHom (CategoryTheory.Functor.map (𝟭 LocallyRingedSpace) f ≫ Y.toΓSpec)))
        (op (basicOpen r)))

Tactic:
rw [LocallyRingedSpace.comp_c_app, ← Category.assoc]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.LocallyRingedSpace.comp_c_app
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
r : (↑(unop (Γ.rightOp.obj Y)) : Type u)
h :
  (Γ.rightOp.map f).unop ≫ (Functor.obj (𝟭 LocallyRingedSpace) X).presheaf.map (Quiver.Hom.op (homOfLE ⋯)) =
    f.c.app (op ⊤) ≫ (Functor.obj (pushforward CommRingCat f.base) X.presheaf).map (Y.toΓSpecMapBasicOpen r).leTop.op
⊢ Eq (α :=
    unop (Γ.rightOp.obj Y) ⟶
      (Functor.obj (𝟭 LocallyRingedSpace) X).presheaf.obj
        (op
          (Functor.obj (C :=
            Opens (↑(↑(Spec.locallyRingedSpaceObj (unop (Γ.rightOp.obj Y))).toPresheafedSpace : TopCat) : Type u))
            (Opens.map
              (PresheafedSpace.Hom.base (Hom.toHom (CategoryTheory.Functor.map (𝟭 LocallyRingedSpace) f ≫ Y.toΓSpec))))
            (basicOpen r))))
    ((Γ.rightOp.map f).unop ≫ (Functor.obj (𝟭 LocallyRingedSpace) X).presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
    ((CommRingCat.ofHom
          (algebraMap (↑(unop (Γ.rightOp.obj Y)) : Type u)
            (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(unop (Γ.rightOp.obj Y)) : Type u)) : Type u))ᵒᵖ)
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf
                  (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(unop (Γ.rightOp.obj Y)) : Type u)) : Type u)))
                (structureSheafInType (↑(unop (Γ.rightOp.obj Y)) : Type u) (↑(unop (Γ.rightOp.obj Y)) : Type u)))
              (op (basicOpen r)))) ≫
        Y.toΓSpec.c.app (op (basicOpen r))) ≫
      NatTrans.app (PresheafedSpace.Hom.c (Hom.toHom (CategoryTheory.Functor.map (𝟭 LocallyRingedSpace) f)))
        (op ((Opens.map Y.toΓSpec.base).obj (unop (op (basicOpen r))))))

Tactic:
erw [Y.toΓSpecSheafedSpace_app_spec, f.c.naturality]

Premises used: AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, CategoryTheory.NatTrans.naturality, AlgebraicGeometry.PresheafedSpace.Hom.c, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
r : (↑(unop (Γ.rightOp.obj Y)) : Type u)
⊢ (Γ.rightOp.map f).unop ≫ (Functor.obj (𝟭 LocallyRingedSpace) X).presheaf.map (Quiver.Hom.op (homOfLE ⋯)) =
    f.c.app (op ⊤) ≫ (Functor.obj (pushforward CommRingCat f.base) X.presheaf).map (Y.toΓSpecMapBasicOpen r).leTop.op

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
⊢ SpecΓIdentity.inv.app (Γ.obj (op X)) ≫ (identityToΓSpec.app X).c.app (op ⊤) =
    𝟙 (Functor.obj (𝟭 CommRingCat) (Γ.obj (op X)))

Tactic:
X.Γ_Spec_left_triangle

Premises used: Set.Mem, AlgebraicGeometry.LocallyRingedSpace.Γ_Spec_left_triangle