awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.RingedSpace.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y : PresheafedSpace.{v, u, v} C
α : X ⟶ Y
U : Opens (↑(↑Y : TopCat) : Type v)
x : (↑(↑X : TopCat) : Type v)
hx :
  Membership.mem (α := (↑(↑Y : TopCat) : Type v)) U
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            α.base :
          (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
        x :
      (↑(↑Y : TopCat) : Type v))
rw :
  Eq (α := Y.presheaf.obj (op U) ⟶ X.presheaf.stalk x)
    (Y.presheaf.germ U
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              α.base :
            (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
          x)
        hx ≫
      map
          (stalkFunctor C
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                  TopCat.carrier) α.base :
                (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
              x))
          α.c ≫
        stalkPushforward C α.base X.presheaf x)
    (α.c.app (op U) ≫ X.presheaf.germ ((Opens.map α.base).obj U) x hx)
rw₁ :
  Eq (α := Y.presheaf.obj (op U) ⟶ X.presheaf.stalk x)
    (α.c.app (op U) ≫
      (obj (pushforward C α.base) X.presheaf).germ U
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                α.base :
              (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
            x)
          hx ≫
        stalkPushforward C α.base X.presheaf x)
    (α.c.app (op U) ≫ X.presheaf.germ ((Opens.map α.base).obj U) x hx)
rw₂ rw₃ :
  Eq (α := Y.presheaf.obj (op U) ⟶ X.presheaf.stalk x)
    (α.c.app (op U) ≫ X.presheaf.germ ((Opens.map α.base).obj U) x hx)
    (α.c.app (op U) ≫ X.presheaf.germ ((Opens.map α.base).obj U) x hx)
⊢ Eq (α := Y.presheaf.obj (op U) ⟶ X.presheaf.stalk x)
    (Y.presheaf.germ U
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              α.base :
            (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
          x)
        hx ≫
      Hom.stalkMap α x)
    (α.c.app (op U) ≫ X.presheaf.germ ((Opens.map α.base).obj U) x hx)

Tactic:
rw [Hom.stalkMap, stalkFunctor_map_germ_assoc, stalkPushforward_germ]

Premises used: AlgebraicGeometry.PresheafedSpace.Hom.stalkMap, TopCat.Presheaf.stalkPushforward_germ, TopCat.Presheaf.stalkFunctor_map_germ_assoc
-- Module: Mathlib.Geometry.RingedSpace.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
U : TopCat
X : PresheafedSpace.{v, u, v} C
f : U ⟶ (↑X : TopCat)
h :
  IsOpenEmbedding (X := (↑U : Type v)) (Y := (↑(↑X : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) f) :
      (a : (↑U : Type v)) → (↑(↑X : TopCat) : Type v))
V : Opens (↑U : Type v)
x : (↑U : Type v)
hx : x ∈ V
⊢ Eq (α :=
    (X.restrict h).presheaf.obj (op V) ⟶
      X.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              f :
            (a : (↑U : Type v)) → (↑(↑X : TopCat) : Type v))
          x))
    ((X.restrict h).presheaf.germ V x hx ≫ Iso.hom (X.restrictStalkIso h x))
    (X.presheaf.germ (h.functor.obj V)
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) f :
          (a : (↑U : Type v)) → (↑(↑X : TopCat) : Type v))
        x)
      ⋯)

Tactic:
colimit.ι_pre ((OpenNhds.inclusion (f x)).op ⋙ X.presheaf) (h.functorNhds x).op
    (op ⟨V, hx⟩)

Premises used: CategoryTheory.Functor.op, IsOpenMap.functorMap, CategoryTheory.ConcreteCategory.hom, Set.Mem, IsOpenMap.functorNhds, CategoryTheory.Functor.comp, CategoryTheory.Limits.colimit.ι_pre, TopCat.Presheaf.stalk, CategoryTheory.Limits.colimit, Subtype.mk, TopCat.Presheaf.germ, Monotone.functor, CategoryTheory.Limits.colimit.desc, Opposite.op, CategoryTheory.homOfLE, AlgebraicGeometry.PresheafedSpace.presheaf, TopologicalSpace.OpenNhds, CategoryTheory.Limits.colimit.pre, Topology.IsOpenEmbedding.functorNhds, DFunLike.coe, TopologicalSpace.OpenNhds.inclusion
-- Module: Mathlib.Geometry.RingedSpace.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
U : TopCat
X : PresheafedSpace.{v, u, v} C
f : U ⟶ (↑X : TopCat)
h :
  IsOpenEmbedding (X := (↑U : Type v)) (Y := (↑(↑X : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) f) :
      (a : (↑U : Type v)) → (↑(↑X : TopCat) : Type v))
V : Opens (↑U : Type v)
x : (↑U : Type v)
hx : x ∈ V
rw :
  Eq (α := X.presheaf.obj (op (h.functor.obj V)) ⟶ (X.restrict h).presheaf.stalk x)
    (((X.restrict h).presheaf.germ V x hx ≫ Iso.hom (X.restrictStalkIso h x)) ≫ Iso.inv (X.restrictStalkIso h x))
    ((X.restrict h).presheaf.germ V x hx)
hx₁ : x ∈ V
rw₁ :
  Eq (α := X.presheaf.obj (op (h.functor.obj V)) ⟶ (X.restrict h).presheaf.stalk x)
    ((X.restrict h).presheaf.germ V x hx ≫ Iso.hom (X.restrictStalkIso h x) ≫ Iso.inv (X.restrictStalkIso h x))
    ((X.restrict h).presheaf.germ V x hx)
hx₂ : x ∈ V
rw₂ : (X.restrict h).presheaf.germ V x hx ≫ 𝟙 ((X.restrict h).presheaf.stalk x) = (X.restrict h).presheaf.germ V x hx
hx₃ : x ∈ V
rw₃ :
  Eq (α := X.presheaf.obj (op (h.functor.obj V)) ⟶ (X.restrict h).presheaf.stalk x)
    ((X.restrict h).presheaf.germ V x hx) ((X.restrict h).presheaf.germ V x hx)
hx₄ : x ∈ V
rw₄ :
  Eq (α := X.presheaf.obj (op (h.functor.obj V)) ⟶ (X.restrict h).presheaf.stalk x)
    ((X.restrict h).presheaf.germ V x hx) ((X.restrict h).presheaf.germ V x hx)
hx₅ : x ∈ V
⊢ Eq (α := X.presheaf.obj (op (h.functor.obj V)) ⟶ (X.restrict h).presheaf.stalk x)
    (X.presheaf.germ (h.functor.obj V)
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              f :
            (a : (↑U : Type v)) → (↑(↑X : TopCat) : Type v))
          x)
        ⋯ ≫
      Iso.inv (X.restrictStalkIso h x))
    ((X.restrict h).presheaf.germ V x hx)

Tactic:
rw [← restrictStalkIso_hom_eq_germ, Category.assoc, Iso.hom_inv_id, Category.comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.hom_inv_id, AlgebraicGeometry.PresheafedSpace.restrictStalkIso_hom_eq_germ, CategoryTheory.Category.comp_id
-- Module: Mathlib.Geometry.RingedSpace.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
U : TopCat
X : PresheafedSpace.{v, u, v} C
f : U ⟶ (↑X : TopCat)
h :
  IsOpenEmbedding (X := (↑U : Type v)) (Y := (↑(↑X : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) f) :
      (a : (↑U : Type v)) → (↑(↑X : TopCat) : Type v))
x : (↑U : Type v)
⊢ Eq (α :=
    X.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              f :
            (a : (↑U : Type v)) → (↑(↑X : TopCat) : Type v))
          x) ⟶
      (X.restrict h).presheaf.stalk x)
    (Iso.inv (X.restrictStalkIso h x)) (Hom.stalkMap (X.ofRestrict h) x)

Tactic:
colimit.hom_ext fun V => ?_

Premises used: TopCat.Presheaf.stalk, CategoryTheory.Limits.colimit, CategoryTheory.Limits.colimit.hom_ext
-- Module: Mathlib.Geometry.RingedSpace.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
U : TopCat
X : PresheafedSpace.{v, u, v} C
f : U ⟶ (↑X : TopCat)
h :
  IsOpenEmbedding (X := (↑U : Type v)) (Y := (↑(↑X : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) f) :
      (a : (↑U : Type v)) → (↑(↑X : TopCat) : Type v))
x : (↑U : Type v)
V :
  OpenNhds (X := (↑X : TopCat))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) f :
        (a : (↑U : Type v)) → (↑(↑X : TopCat) : Type v))
      x)
⊢ Eq (α :=
    obj
        (obj
          (obj
            (whiskeringLeft
              (OpenNhds (X := (↑X : TopCat))
                  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                        TopCat.carrier) f :
                      (a : (↑U : Type v)) → (↑(↑X : TopCat) : Type v))
                    x))ᵒᵖ
              (Opens (↑(↑X : TopCat) : Type v))ᵒᵖ C)
            (Functor.op
              (OpenNhds.inclusion
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                      TopCat.carrier) f :
                    (a : (↑U : Type v)) → (↑(↑X : TopCat) : Type v))
                  x))))
          X.presheaf)
        (op V) ⟶
      (X.restrict h).presheaf.stalk x)
    (colimit.ι
        (obj
          (obj
            (whiskeringLeft
              (OpenNhds (X := (↑X : TopCat))
                  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                        TopCat.carrier) f :
                      (a : (↑U : Type v)) → (↑(↑X : TopCat) : Type v))
                    x))ᵒᵖ
              (Opens (↑(↑X : TopCat) : Type v))ᵒᵖ C)
            (Functor.op
              (OpenNhds.inclusion
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                      TopCat.carrier) f :
                    (a : (↑U : Type v)) → (↑(↑X : TopCat) : Type v))
                  x))))
          X.presheaf)
        (op V) ≫
      Iso.inv (X.restrictStalkIso h x))
    (colimit.ι
        (obj
          (obj
            (whiskeringLeft
              (OpenNhds (X := (↑X : TopCat))
                  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                        TopCat.carrier) f :
                      (a : (↑U : Type v)) → (↑(↑X : TopCat) : Type v))
                    x))ᵒᵖ
              (Opens (↑(↑X : TopCat) : Type v))ᵒᵖ C)
            (Functor.op
              (OpenNhds.inclusion
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                      TopCat.carrier) f :
                    (a : (↑U : Type v)) → (↑(↑X : TopCat) : Type v))
                  x))))
          X.presheaf)
        (op V) ≫
      Hom.stalkMap (X.ofRestrict h) x)

Tactic:
?_
-- Module: Mathlib.Geometry.RingedSpace.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
U : TopCat
X : PresheafedSpace.{v, u, v} C
f : U ⟶ (↑X : TopCat)
h :
  IsOpenEmbedding (X := (↑U : Type v)) (Y := (↑(↑X : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) f) :
      (a : (↑U : Type v)) → (↑(↑X : TopCat) : Type v))
x : (↑U : Type v)
rw :
  IsIso (X :=
    X.presheaf.stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (X.ofRestrict h).base :
          (a : (↑(↑(X.restrict h) : TopCat) : Type v)) → (↑(↑X : TopCat) : Type v))
        x))
    (Iso.inv (X.restrictStalkIso h x))
⊢ IsIso (X :=
    X.presheaf.stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (X.ofRestrict h).base :
          (a : (↑(↑(X.restrict h) : TopCat) : Type v)) → (↑(↑X : TopCat) : Type v))
        x))
    (Hom.stalkMap (X.ofRestrict h) x)

Tactic:
rw [← restrictStalkIso_inv_eq_ofRestrict]

Premises used: AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_ofRestrict
-- Module: Mathlib.Geometry.RingedSpace.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
U : TopCat
X : PresheafedSpace.{v, u, v} C
f : U ⟶ (↑X : TopCat)
h :
  IsOpenEmbedding (X := (↑U : Type v)) (Y := (↑(↑X : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) f) :
      (a : (↑U : Type v)) → (↑(↑X : TopCat) : Type v))
x : (↑U : Type v)
⊢ IsIso (X :=
    X.presheaf.stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (X.ofRestrict h).base :
          (a : (↑(↑(X.restrict h) : TopCat) : Type v)) → (↑(↑X : TopCat) : Type v))
        x))
    (Iso.inv (X.restrictStalkIso h x))

Tactic:
infer_instance
-- Module: Mathlib.Geometry.RingedSpace.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : PresheafedSpace.{v, u, v} C
x : (↑(↑X : TopCat) : Type v)
dsimp :
  map (stalkFunctor C x) (Hom.c (𝟙 X)) ≫ stalkPushforward C (𝟙 (↑X : TopCat)) X.presheaf x = 𝟙 (X.presheaf.stalk x)
⊢ Hom.stalkMap (𝟙 X) x = 𝟙 (X.presheaf.stalk x)

Tactic:
dsimp [Hom.stalkMap]

Premises used: AlgebraicGeometry.PresheafedSpace.Hom.stalkMap
-- Module: Mathlib.Geometry.RingedSpace.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : PresheafedSpace.{v, u, v} C
x : (↑(↑X : TopCat) : Type v)
ih :
  ∀ (U : Opens (↑(↑X : TopCat) : Type v)) (hxU : x ∈ U),
    X.presheaf.germ U x hxU ≫ map (stalkFunctor C x) (Hom.c (𝟙 X)) ≫ stalkPushforward C (𝟙 (↑X : TopCat)) X.presheaf x =
      X.presheaf.germ U x hxU ≫ 𝟙 (X.presheaf.stalk x)
⊢ map (stalkFunctor C x) (Hom.c (𝟙 X)) ≫ stalkPushforward C (𝟙 (↑X : TopCat)) X.presheaf x = 𝟙 (X.presheaf.stalk x)

Tactic:
ext
-- Module: Mathlib.Geometry.RingedSpace.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : PresheafedSpace.{v, u, v} C
x : (↑(↑X : TopCat) : Type v)
U : Opens (↑(↑X : TopCat) : Type v)
hxU : x ∈ U
⊢ X.presheaf.germ U x hxU ≫ map (stalkFunctor C x) (Hom.c (𝟙 X)) ≫ stalkPushforward C (𝟙 (↑X : TopCat)) X.presheaf x =
    X.presheaf.germ U x hxU ≫ 𝟙 (X.presheaf.stalk x)

Tactic:
simp
-- Module: Mathlib.Geometry.RingedSpace.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y : PresheafedSpace.{v, u, v} C
α β : X ⟶ Y
h₁ : α = β
x x' : (↑(↑X : TopCat) : Type v)
h₂ : x = x'
rw rw₁ : X.presheaf.stalk x' = X.presheaf.stalk x'
⊢ X.presheaf.stalk x = X.presheaf.stalk x'

Tactic:
rw [h₂]
-- Module: Mathlib.Geometry.RingedSpace.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y : PresheafedSpace.{v, u, v} C
α β : X ⟶ Y
h₁ : α = β
x x' : (↑(↑X : TopCat) : Type v)
h₂ : x = x'
rw :
  Y.presheaf.stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            β.base :
          (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
        x) =
    Y.presheaf.stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            β.base :
          (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
        x')
rw₁ rw₂ :
  Y.presheaf.stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            β.base :
          (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
        x') =
    Y.presheaf.stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            β.base :
          (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
        x')
⊢ Y.presheaf.stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            α.base :
          (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
        x) =
    Y.presheaf.stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            β.base :
          (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
        x')

Tactic:
rw [h₁, h₂]
-- Module: Mathlib.Geometry.RingedSpace.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y : PresheafedSpace.{v, u, v} C
α β : X ⟶ Y
h₁ : α = β
x x' : (↑(↑X : TopCat) : Type v)
h₂ : x = x'
ih :
  ∀ (U : Opens (↑(↑Y : TopCat) : Type v))
    (hxU :
      Membership.mem (α := (↑(↑Y : TopCat) : Type v)) U
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                α.base :
              (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
            x :
          (↑(↑Y : TopCat) : Type v))),
    Eq (α := Y.presheaf.obj (op U) ⟶ X.presheaf.stalk x')
      (CategoryStruct.comp (Y :=
        Y.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                α.base :
              (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
            x))
        (Y.presheaf.germ U
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                α.base :
              (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
            x)
          hxU)
        (Hom.stalkMap α x ≫ eqToHom ⋯))
      (CategoryStruct.comp (Y :=
        Y.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                α.base :
              (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
            x))
        (Y.presheaf.germ U
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                α.base :
              (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
            x)
          hxU)
        (eqToHom ⋯ ≫ Hom.stalkMap β x'))
⊢ Eq (α :=
    Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              α.base :
            (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
          x) ⟶
      X.presheaf.stalk x')
    (Hom.stalkMap α x ≫ eqToHom ⋯) (eqToHom ⋯ ≫ Hom.stalkMap β x')

Tactic:
ext
-- Module: Mathlib.Geometry.RingedSpace.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y : PresheafedSpace.{v, u, v} C
α β : X ⟶ Y
h₁ : α = β
x x' : (↑(↑X : TopCat) : Type v)
h₂ : x = x'
U : Opens (↑(↑Y : TopCat) : Type v)
hxU :
  Membership.mem (α := (↑(↑Y : TopCat) : Type v)) U
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            α.base :
          (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
        x :
      (↑(↑Y : TopCat) : Type v))
ih :
  Eq (α := Y.presheaf.obj (op U) ⟶ X.presheaf.stalk x)
    (CategoryStruct.comp (Y :=
      Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              α.base :
            (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
          x))
      (Y.presheaf.germ U
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              α.base :
            (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
          x)
        hxU)
      (Hom.stalkMap α x ≫ eqToHom ⋯))
    (CategoryStruct.comp (Y :=
      Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              α.base :
            (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
          x))
      (Y.presheaf.germ U
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              α.base :
            (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
          x)
        hxU)
      (eqToHom ⋯ ≫ Hom.stalkMap α x))
⊢ Eq (α := Y.presheaf.obj (op U) ⟶ X.presheaf.stalk x')
    (CategoryStruct.comp (Y :=
      Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              α.base :
            (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
          x))
      (Y.presheaf.germ U
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              α.base :
            (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
          x)
        hxU)
      (Hom.stalkMap α x ≫ eqToHom ⋯))
    (CategoryStruct.comp (Y :=
      Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              α.base :
            (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
          x))
      (Y.presheaf.germ U
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              α.base :
            (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
          x)
        hxU)
      (eqToHom ⋯ ≫ Hom.stalkMap β x'))

Tactic:
substs h₁ h₂
-- Module: Mathlib.Geometry.RingedSpace.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y : PresheafedSpace.{v, u, v} C
α : X ⟶ Y
x : (↑(↑X : TopCat) : Type v)
U : Opens (↑(↑Y : TopCat) : Type v)
hxU :
  Membership.mem (α := (↑(↑Y : TopCat) : Type v)) U
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            α.base :
          (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
        x :
      (↑(↑Y : TopCat) : Type v))
⊢ Eq (α := Y.presheaf.obj (op U) ⟶ X.presheaf.stalk x)
    (CategoryStruct.comp (Y :=
      Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              α.base :
            (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
          x))
      (Y.presheaf.germ U
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              α.base :
            (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
          x)
        hxU)
      (Hom.stalkMap α x ≫ eqToHom ⋯))
    (CategoryStruct.comp (Y :=
      Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              α.base :
            (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
          x))
      (Y.presheaf.germ U
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              α.base :
            (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
          x)
        hxU)
      (eqToHom ⋯ ≫ Hom.stalkMap α x))

Tactic:
simp
-- Module: Mathlib.Geometry.RingedSpace.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y : PresheafedSpace.{v, u, v} C
α β : X ⟶ Y
h : α = β
x : (↑(↑X : TopCat) : Type v)
rw rw₁ :
  Y.presheaf.stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            β.base :
          (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
        x) =
    Y.presheaf.stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            β.base :
          (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
        x)
⊢ Y.presheaf.stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            α.base :
          (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
        x) =
    Y.presheaf.stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            β.base :
          (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
        x)

Tactic:
rw [h]