awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R : CommRingCat
h :
  ∀ (U : TopologicalSpace.Opens (↑(↑(sheafedSpaceObj R).toPresheafedSpace : TopCat) : Type u))
    (x : (↑((sheafedSpaceObj R).presheaf.obj (op U)) : Type u)),
    Eq (α :=
      (↑(((TopologicalSpace.Opens.map (InducedCategory.Hom.hom (𝟙 (sheafedSpaceObj R))).base).op ⋙
                (sheafedSpaceObj R).presheaf).obj
            (op U)) :
        Type u))
      ((CommRingCat.Hom.hom
              (NatTrans.app
                ((sheafedSpaceMap (𝟙 R)).hom.c ≫ Functor.whiskerRight (eqToHom ⋯) (sheafedSpaceObj R).presheaf)
                (op U)) :
            (a : (↑((sheafedSpaceObj R).presheaf.obj (op U)) : Type u)) →
              (↑(((TopologicalSpace.Opens.map (𝟙 (sheafedSpaceObj R)).hom.base).op ⋙ (sheafedSpaceObj R).presheaf).obj
                    (op U)) :
                Type u))
          x :
        (↑(((TopologicalSpace.Opens.map (InducedCategory.Hom.hom (𝟙 (sheafedSpaceObj R))).base).op ⋙
                  (sheafedSpaceObj R).presheaf).obj
              (op U)) :
          Type u))
      ((CommRingCat.Hom.hom ((InducedCategory.Hom.hom (𝟙 (sheafedSpaceObj R))).c.app (op U)) :
            (a : (↑((sheafedSpaceObj R).presheaf.obj (op U)) : Type u)) →
              (↑(((TopologicalSpace.Opens.map (𝟙 (sheafedSpaceObj R)).hom.base).op ⋙ (sheafedSpaceObj R).presheaf).obj
                    (op U)) :
                Type u))
          x :
        (↑(((TopologicalSpace.Opens.map (InducedCategory.Hom.hom (𝟙 (sheafedSpaceObj R))).base).op ⋙
                  (sheafedSpaceObj R).presheaf).obj
              (op U)) :
          Type u))
⊢ (sheafedSpaceMap (𝟙 R)).hom.c ≫ Functor.whiskerRight (eqToHom ⋯) (sheafedSpaceObj R).presheaf =
    (InducedCategory.Hom.hom (𝟙 (sheafedSpaceObj R))).c

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R : CommRingCat
U : TopologicalSpace.Opens (↑(↑(sheafedSpaceObj R).toPresheafedSpace : TopCat) : Type u)
x : (↑((sheafedSpaceObj R).presheaf.obj (op U)) : Type u)
⊢ U = (TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R : CommRingCat
U : TopologicalSpace.Opens (↑(↑(sheafedSpaceObj R).toPresheafedSpace : TopCat) : Type u)
x : (↑((sheafedSpaceObj R).presheaf.obj (op U)) : Type u)
⊢ Eq (α :=
    (↑(Functor.obj
          (ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
            (structureSheaf (↑R : Type u)))
          (op ((TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U))) :
      Type u))
    ((RingHom.id
            (↑(Functor.obj
                  (ObjectProperty.FullSubcategory.obj (P :=
                    Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
                    (structureSheaf (↑R : Type u)))
                  (op ((TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U))) :
              Type u) :
          (a : (↑((structureSheaf (↑R : Type u)).obj.obj (op U)) : Type u)) →
            (↑((structureSheaf (↑R : Type u)).obj.obj (op ((TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U))) :
              Type u))
        x :
      (↑(Functor.obj
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
              (structureSheaf (↑R : Type u)))
            (op ((TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U))) :
        Type u))
    ((RingHom.id
            (↑(Functor.obj
                  (ObjectProperty.FullSubcategory.obj (P :=
                    Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
                    (structureSheaf (↑R : Type u)))
                  (op U)) :
              Type u) :
          (a : (↑((structureSheaf (↑R : Type u)).obj.obj (op U)) : Type u)) →
            (↑((structureSheaf (↑R : Type u)).obj.obj (op ((TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U))) :
              Type u))
        x :
      (↑(Functor.obj
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
              (structureSheaf (↑R : Type u)))
            (op ((TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U))) :
        Type u))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
w : (sheafedSpaceMap (f ≫ g)).hom.base = (sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.base
h :
  (sheafedSpaceMap (f ≫ g)).hom.c ≫ Functor.whiskerRight (eqToHom ⋯) (sheafedSpaceObj T).presheaf =
    (sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.c
⊢ sheafedSpaceMap (f ≫ g) = sheafedSpaceMap g ≫ sheafedSpaceMap f

Tactic:
ext : 1
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
⊢ (sheafedSpaceMap (f ≫ g)).hom.base = (sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.base

Tactic:
Spec.topMap_comp f g

Premises used: AlgebraicGeometry.Spec.topObj, AlgebraicGeometry.Spec.topMap, AlgebraicGeometry.Spec.topMap_comp
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
⊢ (sheafedSpaceMap (f ≫ g)).hom.base = (sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.base

Tactic:
exact Spec.topMap_comp f g

Premises used: AlgebraicGeometry.Spec.topMap_comp
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
h :
  ∀ (U : TopologicalSpace.Opens (↑(↑(sheafedSpaceObj R).toPresheafedSpace : TopCat) : Type u))
    (x : (↑((sheafedSpaceObj R).presheaf.obj (op U)) : Type u)),
    Eq (α :=
      (↑(((TopologicalSpace.Opens.map (sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.base).op ⋙
                (sheafedSpaceObj T).presheaf).obj
            (op U)) :
        Type u))
      ((CommRingCat.Hom.hom
              (NatTrans.app
                ((sheafedSpaceMap (f ≫ g)).hom.c ≫ Functor.whiskerRight (eqToHom ⋯) (sheafedSpaceObj T).presheaf)
                (op U)) :
            (a : (↑((sheafedSpaceObj R).presheaf.obj (op U)) : Type u)) →
              (↑(((TopologicalSpace.Opens.map (sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.base).op ⋙
                        (sheafedSpaceObj T).presheaf).obj
                    (op U)) :
                Type u))
          x :
        (↑(((TopologicalSpace.Opens.map (sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.base).op ⋙
                  (sheafedSpaceObj T).presheaf).obj
              (op U)) :
          Type u))
      ((CommRingCat.Hom.hom ((sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.c.app (op U)) :
            (a : (↑((sheafedSpaceObj R).presheaf.obj (op U)) : Type u)) →
              (↑(((TopologicalSpace.Opens.map (sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.base).op ⋙
                        (sheafedSpaceObj T).presheaf).obj
                    (op U)) :
                Type u))
          x :
        (↑(((TopologicalSpace.Opens.map (sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.base).op ⋙
                  (sheafedSpaceObj T).presheaf).obj
              (op U)) :
          Type u))
⊢ (sheafedSpaceMap (f ≫ g)).hom.c ≫ Functor.whiskerRight (eqToHom ⋯) (sheafedSpaceObj T).presheaf =
    (sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.c

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
X Y Z : CommRingCatᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
⊢ sheafedSpaceMap (f ≫ g).unop = sheafedSpaceMap f.unop ≫ sheafedSpaceMap g.unop

Tactic:
simp [Spec.sheafedSpaceMap_comp]

Premises used: AlgebraicGeometry.Spec.sheafedSpaceMap_comp
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R : CommRingCatᵒᵖ
⊢ toPresheafedSpace.obj R = (sheafedSpaceObj (unop R)).toPresheafedSpace

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R : CommRingCat
⊢ toPresheafedSpace.obj (op R) = (sheafedSpaceObj R).toPresheafedSpace

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R S : CommRingCatᵒᵖ
f : R ⟶ S
⊢ toPresheafedSpace.map f = (sheafedSpaceMap f.unop).hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R S : CommRingCat
f : R ⟶ S
⊢ toPresheafedSpace.map f.op = (sheafedSpaceMap f).hom

Tactic:
rfl

Premises used: Set.Mem, Quiver.Hom.unop, rfl
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.hom.base = β.hom.base
r : (↑R : Type u)
U : TopologicalSpace.Opens (PrimeSpectrum (↑R : Type u)) := PrimeSpectrum.basicOpen r
rw rw₁ : (TopologicalSpace.Opens.map β.hom.base).op.obj (op U) = (TopologicalSpace.Opens.map β.hom.base).op.obj (op U)
⊢ (TopologicalSpace.Opens.map α.hom.base).op.obj (op U) = (TopologicalSpace.Opens.map β.hom.base).op.obj (op U)

Tactic:
rw [w]
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.hom.base = β.hom.base
h :
  ∀ (r : (↑R : Type u)),
    let U : TopologicalSpace.Opens (PrimeSpectrum (↑R : Type u)) := PrimeSpectrum.basicOpen r;
    Eq (α := CommRingCat.of (↑R : Type u) ⟶ X.presheaf.obj ((TopologicalSpace.Opens.map β.hom.base).op.obj (op U)))
      ((CommRingCat.ofHom
            (algebraMap (↑R : Type u)
              (Functor.obj
                (ObjectProperty.FullSubcategory.obj (P :=
                  Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
                  (structureSheafInType (↑R : Type u) (↑R : Type u)))
                (op U))) ≫
          α.hom.c.app (op U)) ≫
        X.presheaf.map (eqToHom ⋯))
      (CommRingCat.ofHom
          (algebraMap (↑R : Type u)
            (Functor.obj
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
                (structureSheafInType (↑R : Type u) (↑R : Type u)))
              (op U))) ≫
        β.hom.c.app (op U))
w₁ : α.hom.base = β.hom.base
h₁ : α.hom.c ≫ Functor.whiskerRight (eqToHom ⋯) X.presheaf = β.hom.c
⊢ α = β

Tactic:
ext : 1
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.hom.base = β.hom.base
h :
  ∀ (r : (↑R : Type u)),
    let U : TopologicalSpace.Opens (PrimeSpectrum (↑R : Type u)) := PrimeSpectrum.basicOpen r;
    Eq (α := CommRingCat.of (↑R : Type u) ⟶ X.presheaf.obj ((TopologicalSpace.Opens.map β.hom.base).op.obj (op U)))
      ((CommRingCat.ofHom
            (algebraMap (↑R : Type u)
              (Functor.obj
                (ObjectProperty.FullSubcategory.obj (P :=
                  Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
                  (structureSheafInType (↑R : Type u) (↑R : Type u)))
                (op U))) ≫
          α.hom.c.app (op U)) ≫
        X.presheaf.map (eqToHom ⋯))
      (CommRingCat.ofHom
          (algebraMap (↑R : Type u)
            (Functor.obj
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
                (structureSheafInType (↑R : Type u) (↑R : Type u)))
              (op U))) ≫
        β.hom.c.app (op U))
⊢ α.hom.base = β.hom.base

Tactic:
w
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.hom.base = β.hom.base
h :
  ∀ (r : (↑R : Type u)),
    let U : TopologicalSpace.Opens (PrimeSpectrum (↑R : Type u)) := PrimeSpectrum.basicOpen r;
    Eq (α := CommRingCat.of (↑R : Type u) ⟶ X.presheaf.obj ((TopologicalSpace.Opens.map β.hom.base).op.obj (op U)))
      ((CommRingCat.ofHom
            (algebraMap (↑R : Type u)
              (Functor.obj
                (ObjectProperty.FullSubcategory.obj (P :=
                  Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
                  (structureSheafInType (↑R : Type u) (↑R : Type u)))
                (op U))) ≫
          α.hom.c.app (op U)) ≫
        X.presheaf.map (eqToHom ⋯))
      (CommRingCat.ofHom
          (algebraMap (↑R : Type u)
            (Functor.obj
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
                (structureSheafInType (↑R : Type u) (↑R : Type u)))
              (op U))) ≫
        β.hom.c.app (op U))
⊢ α.hom.base = β.hom.base

Tactic:
exact w
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.hom.base = β.hom.base
h :
  ∀ (r : (↑R : Type u)),
    let U : TopologicalSpace.Opens (PrimeSpectrum (↑R : Type u)) := PrimeSpectrum.basicOpen r;
    Eq (α := CommRingCat.of (↑R : Type u) ⟶ X.presheaf.obj ((TopologicalSpace.Opens.map β.hom.base).op.obj (op U)))
      ((CommRingCat.ofHom
            (algebraMap (↑R : Type u)
              (Functor.obj
                (ObjectProperty.FullSubcategory.obj (P :=
                  Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
                  (structureSheafInType (↑R : Type u) (↑R : Type u)))
                (op U))) ≫
          α.hom.c.app (op U)) ≫
        X.presheaf.map (eqToHom ⋯))
      (CommRingCat.ofHom
          (algebraMap (↑R : Type u)
            (Functor.obj
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
                (structureSheafInType (↑R : Type u) (↑R : Type u)))
              (op U))) ≫
        β.hom.c.app (op U))
h₁ :
  ∀ (i : (↑R : Type u)),
    Eq (α :=
      (sheafedSpaceObj R).presheaf.obj (op (PrimeSpectrum.basicOpen i)) ⟶
        (Functor.obj (TopCat.Sheaf.pushforward CommRingCat β.hom.base) (SheafedSpace.sheaf X)).obj (P :=
              Presheaf.IsSheaf
                (Opens.grothendieckTopology (↑(↑(sheafedSpaceObj R).toPresheafedSpace : TopCat) : Type u))).obj
          (op (PrimeSpectrum.basicOpen i)))
      ((α.hom.c ≫ Functor.whiskerRight (eqToHom ⋯) X.presheaf).app (op (PrimeSpectrum.basicOpen i)))
      (β.hom.c.app (op (PrimeSpectrum.basicOpen i)))
⊢ α.hom.c ≫ Functor.whiskerRight (eqToHom ⋯) X.presheaf = β.hom.c

Tactic:
apply ((TopCat.Sheaf.pushforward _ β.hom.base).obj X.sheaf).hom_ext _
      PrimeSpectrum.isBasis_basic_opens

Premises used: AlgebraicGeometry.PresheafedSpace.Hom.base, TopCat.Sheaf.hom_ext, CategoryTheory.InducedCategory.Hom.hom, AlgebraicGeometry.SheafedSpace.sheaf, CategoryTheory.Functor.obj, PrimeSpectrum.isBasis_basic_opens, TopCat.Sheaf.pushforward
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.hom.base = β.hom.base
h :
  ∀ (r : (↑R : Type u)),
    let U : TopologicalSpace.Opens (PrimeSpectrum (↑R : Type u)) := PrimeSpectrum.basicOpen r;
    Eq (α := CommRingCat.of (↑R : Type u) ⟶ X.presheaf.obj ((TopologicalSpace.Opens.map β.hom.base).op.obj (op U)))
      ((CommRingCat.ofHom
            (algebraMap (↑R : Type u)
              (Functor.obj
                (ObjectProperty.FullSubcategory.obj (P :=
                  Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
                  (structureSheafInType (↑R : Type u) (↑R : Type u)))
                (op U))) ≫
          α.hom.c.app (op U)) ≫
        X.presheaf.map (eqToHom ⋯))
      (CommRingCat.ofHom
          (algebraMap (↑R : Type u)
            (Functor.obj
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
                (structureSheafInType (↑R : Type u) (↑R : Type u)))
              (op U))) ≫
        β.hom.c.app (op U))
r : (↑R : Type u)
⊢ Eq (α :=
    CommRingCat.of (↑R : Type u) ⟶
      (Functor.obj (TopCat.Sheaf.pushforward CommRingCat β.hom.base) (SheafedSpace.sheaf X)).obj (P :=
            Presheaf.IsSheaf
              (Opens.grothendieckTopology (↑(↑(sheafedSpaceObj R).toPresheafedSpace : TopCat) : Type u))).obj
        (op (PrimeSpectrum.basicOpen r)))
    (CommRingCat.ofHom
        (algebraMap (↑R : Type u)
          (↑(Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u))ᵒᵖ)
                (ObjectProperty.FullSubcategory.obj (P :=
                  Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
                  (structureSheaf (↑R : Type u)))
                (op (PrimeSpectrum.basicOpen r))) :
            Type u)) ≫
      (α.hom.c ≫ Functor.whiskerRight (eqToHom ⋯) X.presheaf).app (op (PrimeSpectrum.basicOpen r)))
    (CommRingCat.ofHom
        (algebraMap (↑R : Type u)
          (↑(Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u))ᵒᵖ)
                (ObjectProperty.FullSubcategory.obj (P :=
                  Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
                  (structureSheaf (↑R : Type u)))
                (op (PrimeSpectrum.basicOpen r))) :
            Type u)) ≫
      β.hom.c.app (op (PrimeSpectrum.basicOpen r)))

Tactic:
simpa using h r
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R : CommRingCat
⊢ (locallyRingedSpaceObj R).sheaf = structureSheaf (↑R : Type u)

Tactic:
rfl

Premises used: Set.Mem, AlgebraicGeometry.Spec.structureSheaf, AlgebraicGeometry.structurePresheafInCommRingCat, AlgebraicGeometry.SheafedSpace.sheaf, rfl
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R : Type u
inst : CommRing R
⊢ (locallyRingedSpaceObj (CommRingCat.of R)).sheaf = structureSheaf R

Tactic:
rfl

Premises used: Set.Mem, setOf, AlgebraicGeometry.Spec.structureSheaf, AlgebraicGeometry.structurePresheafInCommRingCat, AlgebraicGeometry.SheafedSpace.sheaf, rfl
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R : CommRingCat
U V : (TopologicalSpace.Opens (↑(↑(locallyRingedSpaceObj R).toPresheafedSpace : TopCat) : Type u))ᵒᵖ
i : U ⟶ V
⊢ (locallyRingedSpaceObj R).presheaf.map i =
    CategoryTheory.Functor.map
      (ObjectProperty.FullSubcategory.obj (P :=
        Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
        (structureSheaf (↑R : Type u)))
      i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R : Type u
inst : CommRing R
⊢ (locallyRingedSpaceObj (CommRingCat.of R)).presheaf =
    ObjectProperty.FullSubcategory.obj (P :=
      Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u))) (structureSheaf R)

Tactic:
rfl

Premises used: Set.Mem, setOf, AlgebraicGeometry.structurePresheafInCommRingCat, rfl
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R : Type u
inst : CommRing R
U V : (TopologicalSpace.Opens (↑(↑(locallyRingedSpaceObj (CommRingCat.of R)).toPresheafedSpace : TopCat) : Type u))ᵒᵖ
i : U ⟶ V
⊢ (locallyRingedSpaceObj (CommRingCat.of R)).presheaf.map i =
    CategoryTheory.Functor.map
      (ObjectProperty.FullSubcategory.obj (P :=
        Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u))) (structureSheaf R))
      i

Tactic:
rfl

Premises used: Set.Mem, setOf, rfl
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum (↑S : Type u)
rw :
  Eq (α := CommRingCat.of (↑R : Type u) ⟶ (Spec.sheafedSpaceObj S).presheaf.stalk p)
    (CategoryStruct.comp (Y :=
      CommRingCat.of
        (Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
            (structureSheafInType (↑R : Type u) (↑R : Type u)))
          (op ⊤)))
      (CommRingCat.ofHom
        (algebraMap (↑R : Type u)
          (Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
              (structureSheafInType (↑R : Type u) (↑R : Type u)))
            (op ⊤))))
      (TopCat.Presheaf.germ (structurePresheafInCommRingCat (↑R : Type u)) ⊤
          (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p) trivial ≫
        PresheafedSpace.Hom.stalkMap (Spec.sheafedSpaceMap f).hom p))
    (f ≫
      CategoryStruct.comp (Y :=
        CommRingCat.of
          (Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
              (structureSheafInType (↑S : Type u) (↑S : Type u)))
            (op ⊤)))
        (CommRingCat.ofHom
          (algebraMap (↑S : Type u)
            (Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u))ᵒᵖ)
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
                (structureSheafInType (↑S : Type u) (↑S : Type u)))
              (op ⊤))))
        (TopCat.Presheaf.germ (structurePresheafInCommRingCat (↑S : Type u)) ⊤ p trivial))
⊢ toStalk (↑R : Type u) (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p) ≫
      PresheafedSpace.Hom.stalkMap (Spec.sheafedSpaceMap f).hom p =
    f ≫ toStalk (↑S : Type u) p

Tactic:
rw [← algebraMap_germ ⊤ p trivial, ← algebraMap_germ ⊤ (PrimeSpectrum.comap f.hom p) trivial,
    Category.assoc]

Premises used: CategoryTheory.Category.assoc, CommRingCat.Hom.hom, trivial, AlgebraicGeometry.StructureSheaf.algebraMap_germ, PrimeSpectrum.comap, Top.top