awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst_2 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_3 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
F G : Presheaf C X
U : Opens (↑X : Type v)
x : (↑X : Type v)
hx : x ∈ U
f : F ⟶ G
s : CC (F.obj (op U))
⊢ Eq (α := CC (obj (stalkFunctor C x) G))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (map (stalkFunctor C x) f) :
          (a : CC ((stalkFunctor C x).obj F)) → CC ((stalkFunctor C x).obj G))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx) : (a : CC (F.obj (op U))) → CC (F.stalk x)) s :
          CC (F.stalk x)) :
      CC (obj (stalkFunctor C x) G))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (map (stalkFunctor C x) f) : (a : CC (F.stalk x)) → CC (G.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx) : (a : CC (F.obj (op U))) → CC (F.stalk x)) s :
          CC (F.stalk x)) :
      CC (G.stalk x))

Tactic:
rfl
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst_2 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_3 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
F G : Presheaf C X
U : Opens (↑X : Type v)
x : (↑X : Type v)
hx : x ∈ U
f : F ⟶ G
s : CC (F.obj (op U))
⊢ Eq (α := CC (G.stalk x))
    ((ConcreteCategory.hom (FC := ToHom.{u_2, v, u, u_1} (FC := FC) (CC := CC)) (CC := CC) (map (stalkFunctor C x) f) :
          (a : CC (F.stalk x)) → CC (G.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx) : (a : CC (F.obj (op U))) → CC (F.stalk x)) s :
          CC (F.stalk x)) :
      CC (G.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (G.germ U x hx) : (a : CC (G.obj (op U))) → CC (G.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op U)) : (a : CC (F.obj (op U))) → CC (G.obj (op U))) s :
          CC (G.obj (op U))) :
      CC (G.stalk x))

Tactic:
stalkFunctor_map_germ_apply U x hx f s

Premises used: TopCat.Presheaf.stalk, TopCat.Presheaf.stalkFunctor_map_germ_apply
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y Z : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst_2 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
f : X ⟶ Y
F : Presheaf C X
x : (↑X : Type v)
refine :
  (obj (pushforward C f) F).stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
          (a : (↑X : Type v)) → (↑Y : Type v))
        x) ⟶
    colimit
      ((OpenNhds.map f x).op ⋙
        obj (obj (whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion x).op) F)
⊢ (obj (pushforward C f) F).stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
          (a : (↑X : Type v)) → (↑Y : Type v))
        x) ⟶
    F.stalk x

Tactic:
refine ?_ ≫ colimit.pre _ (OpenNhds.map f x).op

Premises used: CategoryTheory.Functor.op, TopologicalSpace.OpenNhds.map, CategoryTheory.Limits.colimit.pre
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y Z : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst_2 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
f : X ⟶ Y
F : Presheaf C X
x : (↑X : Type v)
⊢ (obj (pushforward C f) F).stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
          (a : (↑X : Type v)) → (↑Y : Type v))
        x) ⟶
    colimit
      ((OpenNhds.map f x).op ⋙
        obj (obj (whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion x).op) F)

Tactic:
exact colim.map (whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso f x).inv) F)

Premises used: CategoryTheory.Limits.colim, CategoryTheory.Functor.map, CategoryTheory.NatTrans.op, CategoryTheory.Functor.whiskerRight, TopologicalSpace.OpenNhds.inclusionMapIso, CategoryTheory.Iso.inv
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : Presheaf C X
U : Opens (↑Y : Type v)
x : (↑X : Type v)
hx :
  Membership.mem (α := (↑Y : Type v)) U
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
          (a : (↑X : Type v)) → (↑Y : Type v))
        x :
      (↑Y : Type v))
⊢ Eq (α := (obj (pushforward C f) F).obj (op U) ⟶ F.stalk x)
    ((obj (pushforward C f) F).germ U
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
            (a : (↑X : Type v)) → (↑Y : Type v))
          x)
        hx ≫
      stalkPushforward C f F x)
    (F.germ ((Opens.map f).obj U) x hx)

Tactic:
simp [germ, stalkPushforward]

Premises used: TopCat.Presheaf.germ, TopCat.Presheaf.stalkPushforward
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
ℱ : Presheaf C X
x : (↑X : Type v)
ih :
  ∀ (U : Opens (↑X : Type v))
    (hxU :
      Membership.mem (α := (↑X : Type v)) U
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) (𝟙 X) :
              (a : (↑X : Type v)) → (↑X : Type v))
            x :
          (↑X : Type v))),
    Eq (α := (obj (pushforward C (𝟙 X)) ℱ).obj (op U) ⟶ ℱ.stalk x)
      ((obj (pushforward C (𝟙 X)) ℱ).germ U
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
                (𝟙 X) :
              (a : (↑X : Type v)) → (↑X : Type v))
            x)
          hxU ≫
        stalkPushforward C (𝟙 X) ℱ x)
      ((obj (pushforward C (𝟙 X)) ℱ).germ U
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
                (𝟙 X) :
              (a : (↑X : Type v)) → (↑X : Type v))
            x)
          hxU ≫
        map (stalkFunctor C x) (Pushforward.id ℱ).hom)
⊢ Eq (α :=
    (obj (pushforward C (𝟙 X)) ℱ).stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) (𝟙 X) :
            (a : (↑X : Type v)) → (↑X : Type v))
          x) ⟶
      ℱ.stalk x)
    (stalkPushforward C (𝟙 X) ℱ x) (map (stalkFunctor C x) (Pushforward.id ℱ).hom)

Tactic:
ext
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y Z : TopCat
ℱ : Presheaf C X
f : X ⟶ Y
g : Y ⟶ Z
x : (↑X : Type v)
ih :
  ∀ (U : Opens (↑Z : Type v))
    (hxU :
      Membership.mem (α := (↑Z : Type v)) U
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
                (f ≫ g) :
              (a : (↑X : Type v)) → (↑Z : Type v))
            x :
          (↑Z : Type v))),
    Eq (α := (obj (pushforward C (f ≫ g)) ℱ).obj (op U) ⟶ ℱ.stalk x)
      ((obj (pushforward C (f ≫ g)) ℱ).germ U
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
                (f ≫ g) :
              (a : (↑X : Type v)) → (↑Z : Type v))
            x)
          hxU ≫
        stalkPushforward C (f ≫ g) ℱ x)
      ((obj (pushforward C (f ≫ g)) ℱ).germ U
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
                (f ≫ g) :
              (a : (↑X : Type v)) → (↑Z : Type v))
            x)
          hxU ≫
        stalkPushforward C g (obj (pushforward C f) ℱ)
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
                (a : (↑X : Type v)) → (↑Y : Type v))
              x) ≫
          stalkPushforward C f ℱ x)
⊢ Eq (α :=
    (obj (pushforward C (f ≫ g)) ℱ).stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
              (f ≫ g) :
            (a : (↑X : Type v)) → (↑Z : Type v))
          x) ⟶
      ℱ.stalk x)
    (stalkPushforward C (f ≫ g) ℱ x)
    (stalkPushforward C g (obj (pushforward C f) ℱ)
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
            (a : (↑X : Type v)) → (↑Y : Type v))
          x) ≫
      stalkPushforward C f ℱ x)

Tactic:
ext
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y Z : TopCat
ℱ : Presheaf C X
f : X ⟶ Y
g : Y ⟶ Z
x : (↑X : Type v)
U : Opens (↑Z : Type v)
hxU :
  Membership.mem (α := (↑Z : Type v)) U
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) (f ≫ g) :
          (a : (↑X : Type v)) → (↑Z : Type v))
        x :
      (↑Z : Type v))
⊢ Eq (α := (obj (pushforward C (f ≫ g)) ℱ).obj (op U) ⟶ ℱ.stalk x)
    ((obj (pushforward C (f ≫ g)) ℱ).germ U
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
              (f ≫ g) :
            (a : (↑X : Type v)) → (↑Z : Type v))
          x)
        hxU ≫
      stalkPushforward C (f ≫ g) ℱ x)
    ((obj (pushforward C (f ≫ g)) ℱ).germ U
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
              (f ≫ g) :
            (a : (↑X : Type v)) → (↑Z : Type v))
          x)
        hxU ≫
      stalkPushforward C g (obj (pushforward C f) ℱ)
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
              (a : (↑X : Type v)) → (↑Y : Type v))
            x) ≫
        stalkPushforward C f ℱ x)

Tactic:
simp [germ, stalkPushforward]

Premises used: TopCat.Presheaf.germ, TopCat.Presheaf.stalkPushforward
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y : TopCat
f : X ⟶ Y
hf :
  IsInducing (X := (↑X : Type v)) (Y := (↑Y : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
      (a : (↑X : Type v)) → (↑Y : Type v))
F : Presheaf C X
x : (↑X : Type v)
⊢ (OpenNhds.map f x).Initial

Tactic:
haveI := Functor.initial_of_adjunction (hf.adjunctionNhds x)
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y : TopCat
f : X ⟶ Y
hf :
  IsInducing (X := (↑X : Type v)) (Y := (↑Y : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
      (a : (↑X : Type v)) → (↑Y : Type v))
F : Presheaf C X
x : (↑X : Type v)
this : (OpenNhds.map f x).Initial
⊢ IsIso (X := colimit ((OpenNhds.map f x).op ⋙ (OpenNhds.inclusion x).op ⋙ F)) (Y :=
    colimit ((OpenNhds.inclusion x).op ⋙ F))
    (Iso.hom (Final.colimitIso (OpenNhds.map f x).op ((OpenNhds.inclusion x).op ⋙ F)) :
      colimit ((OpenNhds.map f x).op ⋙ (OpenNhds.inclusion x).op ⋙ F) ⟶ colimit ((OpenNhds.inclusion x).op ⋙ F))

Tactic:
(Functor.Final.colimitIso (OpenNhds.map f x).op ((OpenNhds.inclusion x).op ⋙ F)).isIso_hom

Premises used: CategoryTheory.Functor.op, CategoryTheory.Functor.comp, TopologicalSpace.OpenNhds.map, CategoryTheory.Iso.isIso_hom, CategoryTheory.Functor.Final.colimitIso, TopologicalSpace.OpenNhds.inclusion
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y : TopCat
f : X ⟶ Y
hf :
  IsInducing (X := (↑X : Type v)) (Y := (↑Y : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
      (a : (↑X : Type v)) → (↑Y : Type v))
F : Presheaf C X
x : (↑X : Type v)
this : (OpenNhds.map f x).Initial
h :
  (obj (pushforward C f) F).stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
            (a : (↑X : Type v)) → (↑Y : Type v))
          x) =
      colimit ((OpenNhds.map f x).op ⋙ (OpenNhds.inclusion x).op ⋙ F) →
    F.stalk x = colimit ((OpenNhds.inclusion x).op ⋙ F) →
      Eq (α :=
        (obj (pushforward C f) F).stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
                (a : (↑X : Type v)) → (↑Y : Type v))
              x) ⟶
          F.stalk x)
        (stalkPushforward C f F x) (Iso.hom (Final.colimitIso (OpenNhds.map f x).op ((OpenNhds.inclusion x).op ⋙ F)))
⊢ IsIso (X :=
    (obj (pushforward C f) F).stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
          (a : (↑X : Type v)) → (↑Y : Type v))
        x))
    (stalkPushforward C f F x)

Tactic:
convert!
    (Functor.Final.colimitIso (OpenNhds.map f x).op ((OpenNhds.inclusion x).op ⋙ F)).isIso_hom

Premises used: CategoryTheory.Functor.op, CategoryTheory.Functor.comp, TopologicalSpace.OpenNhds.map, CategoryTheory.Iso.isIso_hom, CategoryTheory.Functor.Final.colimitIso, TopologicalSpace.OpenNhds.inclusion
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y : TopCat
f : X ⟶ Y
hf :
  IsInducing (X := (↑X : Type v)) (Y := (↑Y : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
      (a : (↑X : Type v)) → (↑Y : Type v))
F : Presheaf C X
x : (↑X : Type v)
this : (OpenNhds.map f x).Initial
e_3 :
  (obj (pushforward C f) F).stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
          (a : (↑X : Type v)) → (↑Y : Type v))
        x) =
    colimit ((OpenNhds.map f x).op ⋙ (OpenNhds.inclusion x).op ⋙ F)
e_4 : F.stalk x = colimit ((OpenNhds.inclusion x).op ⋙ F)
⊢ Eq (α :=
    (obj (pushforward C f) F).stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
            (a : (↑X : Type v)) → (↑Y : Type v))
          x) ⟶
      F.stalk x)
    (stalkPushforward C f F x) (Iso.hom (Final.colimitIso (OpenNhds.map f x).op ((OpenNhds.inclusion x).op ⋙ F)))

Tactic:
stalk_hom_ext _ fun U hU ↦ (stalkPushforward_germ _ f F _ x hU).trans ?_

Premises used: TopCat.Presheaf.stalk_hom_ext, TopCat.Presheaf.stalkPushforward_germ, Eq.trans
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y : TopCat
f : X ⟶ Y
hf :
  IsInducing (X := (↑X : Type v)) (Y := (↑Y : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
      (a : (↑X : Type v)) → (↑Y : Type v))
F : Presheaf C X
x : (↑X : Type v)
this : (OpenNhds.map f x).Initial
e_3 :
  (obj (pushforward C f) F).stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
          (a : (↑X : Type v)) → (↑Y : Type v))
        x) =
    colimit ((OpenNhds.map f x).op ⋙ (OpenNhds.inclusion x).op ⋙ F)
e_4 : F.stalk x = colimit ((OpenNhds.inclusion x).op ⋙ F)
h :
  ∀ (U : Opens (↑Y : Type v))
    (hU :
      Membership.mem (α := (↑Y : Type v)) U
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
              (a : (↑X : Type v)) → (↑Y : Type v))
            x :
          (↑Y : Type v))),
    Eq (α := (obj (pushforward C f) F).obj (op U) ⟶ F.stalk x) (F.germ ((Opens.map f).obj U) x hU)
      (CategoryStruct.comp (Y :=
        (obj (pushforward C f) F).stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
              (a : (↑X : Type v)) → (↑Y : Type v))
            x))
        ((obj (pushforward C f) F).germ U
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
              (a : (↑X : Type v)) → (↑Y : Type v))
            x)
          hU)
        (Iso.hom (Final.colimitIso (OpenNhds.map f x).op ((OpenNhds.inclusion x).op ⋙ F))))
⊢ Eq (α :=
    (obj (pushforward C f) F).stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
            (a : (↑X : Type v)) → (↑Y : Type v))
          x) ⟶
      F.stalk x)
    (stalkPushforward C f F x) (Iso.hom (Final.colimitIso (OpenNhds.map f x).op ((OpenNhds.inclusion x).op ⋙ F)))

Tactic:
refine stalk_hom_ext _ fun U hU ↦ (stalkPushforward_germ _ f F _ x hU).trans ?_

Premises used: TopCat.Presheaf.stalk_hom_ext, TopCat.Presheaf.stalkPushforward_germ, Eq.trans
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y : TopCat
f : X ⟶ Y
hf :
  IsInducing (X := (↑X : Type v)) (Y := (↑Y : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
      (a : (↑X : Type v)) → (↑Y : Type v))
F : Presheaf C X
x : (↑X : Type v)
this : (OpenNhds.map f x).Initial
e_3 :
  (obj (pushforward C f) F).stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
          (a : (↑X : Type v)) → (↑Y : Type v))
        x) =
    colimit ((OpenNhds.map f x).op ⋙ (OpenNhds.inclusion x).op ⋙ F)
e_4 : F.stalk x = colimit ((OpenNhds.inclusion x).op ⋙ F)
U : Opens (↑Y : Type v)
hU :
  Membership.mem (α := (↑Y : Type v)) U
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
          (a : (↑X : Type v)) → (↑Y : Type v))
        x :
      (↑Y : Type v))
h :
  Eq (α := (obj (pushforward C f) F).obj (op U) ⟶ F.stalk x)
    (CategoryStruct.comp (Y :=
        (obj (pushforward C f) F).stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
              (a : (↑X : Type v)) → (↑Y : Type v))
            x))
        ((obj (pushforward C f) F).germ U
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
              (a : (↑X : Type v)) → (↑Y : Type v))
            x)
          hU)
        (Iso.hom (Final.colimitIso (OpenNhds.map f x).op ((OpenNhds.inclusion x).op ⋙ F))) :
      (obj (pushforward C f) F).obj (op U) ⟶ F.stalk x)
    (F.germ ((Opens.map f).obj U) x hU : F.obj (op ((Opens.map f).obj U)) ⟶ F.stalk x)
⊢ Eq (α := (obj (pushforward C f) F).obj (op U) ⟶ F.stalk x) (F.germ ((Opens.map f).obj U) x hU)
    (CategoryStruct.comp (Y :=
      (obj (pushforward C f) F).stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
            (a : (↑X : Type v)) → (↑Y : Type v))
          x))
      ((obj (pushforward C f) F).germ U
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
            (a : (↑X : Type v)) → (↑Y : Type v))
          x)
        hU)
      (Iso.hom (Final.colimitIso (OpenNhds.map f x).op ((OpenNhds.inclusion x).op ⋙ F))))

Tactic:
symm
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y : TopCat
f : X ⟶ Y
hf :
  IsInducing (X := (↑X : Type v)) (Y := (↑Y : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
      (a : (↑X : Type v)) → (↑Y : Type v))
F : Presheaf C X
x : (↑X : Type v)
this : (OpenNhds.map f x).Initial
e_3 :
  (obj (pushforward C f) F).stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
          (a : (↑X : Type v)) → (↑Y : Type v))
        x) =
    colimit ((OpenNhds.map f x).op ⋙ (OpenNhds.inclusion x).op ⋙ F)
e_4 : F.stalk x = colimit ((OpenNhds.inclusion x).op ⋙ F)
U : Opens (↑Y : Type v)
hU :
  Membership.mem (α := (↑Y : Type v)) U
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
          (a : (↑X : Type v)) → (↑Y : Type v))
        x :
      (↑Y : Type v))
⊢ Eq (α := (obj (pushforward C f) F).obj (op U) ⟶ F.stalk x)
    (CategoryStruct.comp (Y :=
        (obj (pushforward C f) F).stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
              (a : (↑X : Type v)) → (↑Y : Type v))
            x))
        ((obj (pushforward C f) F).germ U
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
              (a : (↑X : Type v)) → (↑Y : Type v))
            x)
          hU)
        (Iso.hom (Final.colimitIso (OpenNhds.map f x).op ((OpenNhds.inclusion x).op ⋙ F))) :
      (obj (pushforward C f) F).obj (op U) ⟶ F.stalk x)
    (F.germ ((Opens.map f).obj U) x hU : F.obj (op ((Opens.map f).obj U)) ⟶ F.stalk x)

Tactic:
colimit.ι_pre ((OpenNhds.inclusion x).op ⋙ F) (OpenNhds.map f x).op _

Premises used: CategoryTheory.Functor.op, Set.Mem, CategoryTheory.Functor.comp, CategoryTheory.Limits.colimit.ι_pre, TopCat.Presheaf.stalk, TopologicalSpace.OpenNhds.map, CategoryTheory.Limits.colimit, TopCat.Presheaf.germ, Monotone.functor, CategoryTheory.Limits.colimit.desc, CategoryTheory.homOfLE, TopologicalSpace.OpenNhds, CategoryTheory.Limits.colimit.pre, TopologicalSpace.OpenNhds.inclusion
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y : TopCat
f : X ⟶ Y
hf :
  IsInducing (X := (↑X : Type v)) (Y := (↑Y : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
      (a : (↑X : Type v)) → (↑Y : Type v))
F : Presheaf C X
x : (↑X : Type v)
this : (OpenNhds.map f x).Initial
e_3 :
  (obj (pushforward C f) F).stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
          (a : (↑X : Type v)) → (↑Y : Type v))
        x) =
    colimit ((OpenNhds.map f x).op ⋙ (OpenNhds.inclusion x).op ⋙ F)
e_4 : F.stalk x = colimit ((OpenNhds.inclusion x).op ⋙ F)
U : Opens (↑Y : Type v)
hU :
  Membership.mem (α := (↑Y : Type v)) U
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
          (a : (↑X : Type v)) → (↑Y : Type v))
        x :
      (↑Y : Type v))
⊢ Eq (α := (obj (pushforward C f) F).obj (op U) ⟶ F.stalk x)
    (CategoryStruct.comp (Y :=
        (obj (pushforward C f) F).stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
              (a : (↑X : Type v)) → (↑Y : Type v))
            x))
        ((obj (pushforward C f) F).germ U
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
              (a : (↑X : Type v)) → (↑Y : Type v))
            x)
          hU)
        (Iso.hom (Final.colimitIso (OpenNhds.map f x).op ((OpenNhds.inclusion x).op ⋙ F))) :
      (obj (pushforward C f) F).obj (op U) ⟶ F.stalk x)
    (F.germ ((Opens.map f).obj U) x hU : F.obj (op ((Opens.map f).obj U)) ⟶ F.stalk x)

Tactic:
exact colimit.ι_pre ((OpenNhds.inclusion x).op ⋙ F) (OpenNhds.map f x).op _

Premises used: CategoryTheory.Functor.op, CategoryTheory.Functor.comp, CategoryTheory.Limits.colimit.ι_pre, TopologicalSpace.OpenNhds.map, TopologicalSpace.OpenNhds.inclusion