awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sheaves.Skyscraper
Goal:
X : TopCat
p₀ : (↑X : Type u)
inst : (U : Opens (↑X : Type u)) → Decidable (p₀ ∈ U)
C : Type v
inst_1 : Category.{u, v} C
A : C
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
𝓕 𝓖 : Presheaf C X
f : 𝓕 ⟶ 𝓖
w :
  ∀ (U : Opens (↑X : Type u)),
    Eq (α :=
      (Functor.obj (𝟭 (Presheaf C X)) 𝓕).obj (op U) ⟶
        (Functor.obj (Presheaf.stalkFunctor C p₀ ⋙ skyscraperPresheafFunctor p₀) 𝓖).obj (op U))
      (NatTrans.app
        (CategoryTheory.Functor.map (𝟭 (Presheaf C X)) f ≫
          toSkyscraperPresheaf p₀ (𝟙 ((Functor.obj (𝟭 (Presheaf C X)) 𝓖).stalk p₀)))
        (op U))
      (NatTrans.app
        (CategoryStruct.comp (Y := Functor.obj (Presheaf.stalkFunctor C p₀ ⋙ skyscraperPresheafFunctor p₀) 𝓕)
          (toSkyscraperPresheaf p₀ (𝟙 ((Functor.obj (𝟭 (Presheaf C X)) 𝓕).stalk p₀)))
          (CategoryTheory.Functor.map (Presheaf.stalkFunctor C p₀ ⋙ skyscraperPresheafFunctor p₀) f))
        (op U))
⊢ Eq (α := Functor.obj (𝟭 (Presheaf C X)) 𝓕 ⟶ Functor.obj (Presheaf.stalkFunctor C p₀ ⋙ skyscraperPresheafFunctor p₀) 𝓖)
    (CategoryTheory.Functor.map (𝟭 (Presheaf C X)) f ≫
      toSkyscraperPresheaf p₀ (𝟙 ((Functor.obj (𝟭 (Presheaf C X)) 𝓖).stalk p₀)))
    (CategoryStruct.comp (Y := Functor.obj (Presheaf.stalkFunctor C p₀ ⋙ skyscraperPresheafFunctor p₀) 𝓕)
      (toSkyscraperPresheaf p₀ (𝟙 ((Functor.obj (𝟭 (Presheaf C X)) 𝓕).stalk p₀)))
      (CategoryTheory.Functor.map (Presheaf.stalkFunctor C p₀ ⋙ skyscraperPresheafFunctor p₀) f))

Tactic:
ext U
-- Module: Mathlib.Topology.Sheaves.Skyscraper
Goal:
X : TopCat
p₀ : (↑X : Type u)
inst : (U : Opens (↑X : Type u)) → Decidable (p₀ ∈ U)
C : Type v
inst_1 : Category.{u, v} C
A : C
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
𝓕 𝓖 : Presheaf C X
f : 𝓕 ⟶ 𝓖
U : Opens (↑X : Type u)
w :
  Eq (α := 𝓕.obj (op U) ⟶ if p₀ ∈ U then 𝓖.stalk p₀ else terminal.{u, v} C)
    (f.app (op U) ≫
      if h : p₀ ∈ U then 𝓖.germ U p₀ h ≫ 𝟙 (𝓖.stalk p₀) ≫ eqToHom ⋯
      else
        IsTerminal.from
          (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
            (if p₀ ∈ U then 𝓖.stalk p₀ else terminal.{u, v} C) ⋯)
          (𝓖.obj (op U)))
    (CategoryStruct.comp (Y := if p₀ ∈ U then 𝓕.stalk p₀ else terminal.{u, v} C)
      (if h : p₀ ∈ U then 𝓕.germ U p₀ h ≫ 𝟙 (𝓕.stalk p₀) ≫ eqToHom ⋯
      else
        IsTerminal.from
          (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
            (if p₀ ∈ U then 𝓕.stalk p₀ else terminal.{u, v} C) ⋯)
          (𝓕.obj (op U)))
      (if h : p₀ ∈ U then eqToHom ⋯ ≫ CategoryTheory.Functor.map (Presheaf.stalkFunctor C p₀) f ≫ eqToHom ⋯
      else
        IsTerminal.from
          (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
            (if p₀ ∈ U then 𝓖.stalk p₀ else terminal.{u, v} C) ⋯)
          (if p₀ ∈ U then 𝓕.stalk p₀ else terminal.{u, v} C)))
⊢ Eq (α :=
    (Functor.obj (𝟭 (Presheaf C X)) 𝓕).obj (op U) ⟶
      (Functor.obj (Presheaf.stalkFunctor C p₀ ⋙ skyscraperPresheafFunctor p₀) 𝓖).obj (op U))
    (NatTrans.app
      (CategoryTheory.Functor.map (𝟭 (Presheaf C X)) f ≫
        toSkyscraperPresheaf p₀ (𝟙 ((Functor.obj (𝟭 (Presheaf C X)) 𝓖).stalk p₀)))
      (op U))
    (NatTrans.app
      (CategoryStruct.comp (Y := Functor.obj (Presheaf.stalkFunctor C p₀ ⋙ skyscraperPresheafFunctor p₀) 𝓕)
        (toSkyscraperPresheaf p₀ (𝟙 ((Functor.obj (𝟭 (Presheaf C X)) 𝓕).stalk p₀)))
        (CategoryTheory.Functor.map (Presheaf.stalkFunctor C p₀ ⋙ skyscraperPresheafFunctor p₀) f))
      (op U))

Tactic:
dsimp
-- Module: Mathlib.Topology.Sheaves.Skyscraper
Goal:
X : TopCat
p₀ : (↑X : Type u)
inst : (U : Opens (↑X : Type u)) → Decidable (p₀ ∈ U)
C : Type v
inst_1 : Category.{u, v} C
A : C
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
𝓕 𝓖 : Presheaf C X
f : 𝓕 ⟶ 𝓖
U : Opens (↑X : Type u)
pos :
  ∀ (h : p₀ ∈ U),
    Eq (α := 𝓕.obj (op U) ⟶ if p₀ ∈ U then 𝓖.stalk p₀ else terminal.{u, v} C)
      (f.app (op U) ≫ 𝓖.germ U p₀ h ≫ 𝟙 (𝓖.stalk p₀) ≫ eqToHom ⋯)
      (CategoryStruct.comp (Y := if p₀ ∈ U then 𝓕.stalk p₀ else terminal.{u, v} C)
        (𝓕.germ U p₀ h ≫ 𝟙 (𝓕.stalk p₀) ≫ eqToHom ⋯)
        (eqToHom ⋯ ≫ CategoryTheory.Functor.map (Presheaf.stalkFunctor C p₀) f ≫ eqToHom ⋯))
neg :
  ∀ (h : p₀ ∉ U),
    Eq (α := 𝓕.obj (op U) ⟶ if p₀ ∈ U then 𝓖.stalk p₀ else terminal.{u, v} C)
      (f.app (op U) ≫
        IsTerminal.from
          (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
            (if p₀ ∈ U then 𝓖.stalk p₀ else terminal.{u, v} C) ⋯)
          (𝓖.obj (op U)))
      (IsTerminal.from
          (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
            (if p₀ ∈ U then 𝓕.stalk p₀ else terminal.{u, v} C) ⋯)
          (𝓕.obj (op U)) ≫
        IsTerminal.from
          (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
            (if p₀ ∈ U then 𝓖.stalk p₀ else terminal.{u, v} C) ⋯)
          (if p₀ ∈ U then 𝓕.stalk p₀ else terminal.{u, v} C))
⊢ Eq (α := 𝓕.obj (op U) ⟶ if p₀ ∈ U then 𝓖.stalk p₀ else terminal.{u, v} C)
    (f.app (op U) ≫
      if h : p₀ ∈ U then 𝓖.germ U p₀ h ≫ 𝟙 (𝓖.stalk p₀) ≫ eqToHom ⋯
      else
        IsTerminal.from
          (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
            (if p₀ ∈ U then 𝓖.stalk p₀ else terminal.{u, v} C) ⋯)
          (𝓖.obj (op U)))
    (CategoryStruct.comp (Y := if p₀ ∈ U then 𝓕.stalk p₀ else terminal.{u, v} C)
      (if h : p₀ ∈ U then 𝓕.germ U p₀ h ≫ 𝟙 (𝓕.stalk p₀) ≫ eqToHom ⋯
      else
        IsTerminal.from
          (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
            (if p₀ ∈ U then 𝓕.stalk p₀ else terminal.{u, v} C) ⋯)
          (𝓕.obj (op U)))
      (if h : p₀ ∈ U then eqToHom ⋯ ≫ CategoryTheory.Functor.map (Presheaf.stalkFunctor C p₀) f ≫ eqToHom ⋯
      else
        IsTerminal.from
          (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
            (if p₀ ∈ U then 𝓖.stalk p₀ else terminal.{u, v} C) ⋯)
          (if p₀ ∈ U then 𝓕.stalk p₀ else terminal.{u, v} C)))

Tactic:
split_ifs with h
-- Module: Mathlib.Topology.Sheaves.Skyscraper
Goal:
X : TopCat
p₀ : (↑X : Type u)
inst : (U : Opens (↑X : Type u)) → Decidable (p₀ ∈ U)
C : Type v
inst_1 : Category.{u, v} C
A : C
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
𝓕 𝓖 : Presheaf C X
f : 𝓕 ⟶ 𝓖
U : Opens (↑X : Type u)
h : p₀ ∈ U
⊢ Eq (α := 𝓕.obj (op U) ⟶ if p₀ ∈ U then 𝓖.stalk p₀ else terminal.{u, v} C)
    (f.app (op U) ≫ 𝓖.germ U p₀ h ≫ 𝟙 (𝓖.stalk p₀) ≫ eqToHom ⋯)
    (CategoryStruct.comp (Y := if p₀ ∈ U then 𝓕.stalk p₀ else terminal.{u, v} C)
      (𝓕.germ U p₀ h ≫ 𝟙 (𝓕.stalk p₀) ≫ eqToHom ⋯)
      (eqToHom ⋯ ≫ CategoryTheory.Functor.map (Presheaf.stalkFunctor C p₀) f ≫ eqToHom ⋯))

Tactic:
simp only [Category.id_comp, Category.assoc, eqToHom_trans_assoc, eqToHom_refl,
        Presheaf.stalkFunctor_map_germ_assoc, Presheaf.stalkFunctor_obj]

Premises used: CategoryTheory.Category.assoc, TopCat.Presheaf.stalkFunctor_obj, CategoryTheory.eqToHom_refl, CategoryTheory.eqToHom_trans_assoc, TopCat.Presheaf.stalkFunctor_map_germ_assoc, CategoryTheory.Category.id_comp
-- Module: Mathlib.Topology.Sheaves.Skyscraper
Goal:
X : TopCat
p₀ : (↑X : Type u)
inst : (U : Opens (↑X : Type u)) → Decidable (p₀ ∈ U)
C : Type v
inst_1 : Category.{u, v} C
A : C
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
𝓕 𝓖 : Presheaf C X
f : 𝓕 ⟶ 𝓖
U : Opens (↑X : Type u)
h : p₀ ∉ U
⊢ Eq (α := 𝓕.obj (op U) ⟶ if p₀ ∈ U then 𝓖.stalk p₀ else terminal.{u, v} C)
    (f.app (op U) ≫
      IsTerminal.from
        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
          (if p₀ ∈ U then 𝓖.stalk p₀ else terminal.{u, v} C) ⋯)
        (𝓖.obj (op U)))
    (IsTerminal.from
        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
          (if p₀ ∈ U then 𝓕.stalk p₀ else terminal.{u, v} C) ⋯)
        (𝓕.obj (op U)) ≫
      IsTerminal.from
        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
          (if p₀ ∈ U then 𝓖.stalk p₀ else terminal.{u, v} C) ⋯)
        (if p₀ ∈ U then 𝓕.stalk p₀ else terminal.{u, v} C))

Tactic:
apply ((if_neg h).symm.ndrec terminalIsTerminal).hom_ext

Premises used: Eq.ndrec, CategoryTheory.Limits.IsTerminal.hom_ext, CategoryTheory.Limits.terminalIsTerminal, Eq.symm, if_neg
-- Module: Mathlib.Topology.Sheaves.Skyscraper
Goal:
X : TopCat
p₀ : (↑X : Type u)
inst : (U : Opens (↑X : Type u)) → Decidable (p₀ ∈ U)
C : Type v
inst_1 : Category.{u, v} C
A : C
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
x y : C
f : x ⟶ y
U : Opens (↑X : Type u)
hxU : p₀ ∈ U
⊢ Eq (α := Functor.obj (Functor.obj (skyscraperPresheafFunctor p₀) x) (op U) ⟶ Functor.obj.{u, u, v, v} (𝟭 C) y)
    (CategoryStruct.comp (Y := Presheaf.stalk (Functor.obj (skyscraperPresheafFunctor p₀) x) p₀)
      (Presheaf.germ (Functor.obj (skyscraperPresheafFunctor p₀) x) U p₀ hxU)
      (CategoryTheory.Functor.map (skyscraperPresheafFunctor p₀ ⋙ Presheaf.stalkFunctor C p₀) f ≫
        Iso.hom (skyscraperPresheafStalkOfSpecializes p₀ y ⋯)))
    (CategoryStruct.comp (Y := Presheaf.stalk (Functor.obj (skyscraperPresheafFunctor p₀) x) p₀)
      (Presheaf.germ (Functor.obj (skyscraperPresheafFunctor p₀) x) U p₀ hxU)
      (Iso.hom (skyscraperPresheafStalkOfSpecializes p₀ x ⋯) ≫ CategoryTheory.Functor.map (𝟭 C) f))

Tactic:
simp [hxU]
-- Module: Mathlib.Topology.Sheaves.Skyscraper
Goal:
X_1 : TopCat
p₀ : (↑X_1 : Type u)
inst : (U : Opens (↑X_1 : Type u)) → Decidable (p₀ ∈ U)
C : Type v
inst_1 : Category.{u, v} C
A : C
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
X : Presheaf C X_1
dsimp :
  CategoryStruct.comp (Y :=
      colimit ((OpenNhds.inclusion p₀).op ⋙ skyscraperPresheaf p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X))))
      (colimMap
          ((OpenNhds.inclusion p₀).op.whiskerLeft
            {
              app := fun (U : (Opens (↑X_1 : Type u))ᵒᵖ) ↦
                if h : p₀ ∈ unop U then X.germ (unop U) p₀ h ≫ 𝟙 (X.stalk p₀) ≫ eqToHom ⋯
                else
                  IsTerminal.from
                    (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
                      (if p₀ ∈ unop U then colimit ((OpenNhds.inclusion p₀).op ⋙ X) else terminal.{u, v} C) ⋯)
                    (X.obj U),
              naturality := ⋯ }) :
        colimit ((OpenNhds.inclusion p₀).op ⋙ X) ⟶
          colimit ((OpenNhds.inclusion p₀).op ⋙ skyscraperPresheaf p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X))))
      (Iso.hom (skyscraperPresheafStalkOfSpecializes p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X)) ⋯) :
        Presheaf.stalk (skyscraperPresheaf p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X))) p₀ ⟶
          colimit ((OpenNhds.inclusion p₀).op ⋙ X)) =
    𝟙 (colimit ((OpenNhds.inclusion p₀).op ⋙ X))
⊢ CategoryStruct.comp (Y :=
      Functor.obj (C := Presheaf C X_1) (Presheaf.stalkFunctor C p₀)
        (Functor.obj (skyscraperPresheafFunctor p₀) (Functor.obj (Presheaf.stalkFunctor C p₀) X)))
      (CategoryTheory.Functor.map (Presheaf.stalkFunctor C p₀)
        (NatTrans.app (StalkSkyscraperPresheafAdjunctionAuxs.unit p₀) X))
      (NatTrans.app (StalkSkyscraperPresheafAdjunctionAuxs.counit p₀) (Functor.obj (Presheaf.stalkFunctor C p₀) X)) =
    𝟙 (Functor.obj (Presheaf.stalkFunctor C p₀) X)

Tactic:
dsimp [Presheaf.stalkFunctor, toSkyscraperPresheaf]

Premises used: StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf, TopCat.Presheaf.stalkFunctor
-- Module: Mathlib.Topology.Sheaves.Skyscraper
Goal:
X_1 : TopCat
p₀ : (↑X_1 : Type u)
inst : (U : Opens (↑X_1 : Type u)) → Decidable (p₀ ∈ U)
C : Type v
inst_1 : Category.{u, v} C
A : C
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
X : Presheaf C X_1
w :
  ∀ (j : (OpenNhds p₀)ᵒᵖ),
    CategoryStruct.comp (Y := colimit ((OpenNhds.inclusion p₀).op ⋙ X)) (colimit.ι ((OpenNhds.inclusion p₀).op ⋙ X) j)
        (CategoryStruct.comp (Y :=
          colimit ((OpenNhds.inclusion p₀).op ⋙ skyscraperPresheaf p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X))))
          (colimMap
              ((OpenNhds.inclusion p₀).op.whiskerLeft
                {
                  app := fun (U : (Opens (↑X_1 : Type u))ᵒᵖ) ↦
                    if h : p₀ ∈ unop U then X.germ (unop U) p₀ h ≫ 𝟙 (X.stalk p₀) ≫ eqToHom ⋯
                    else
                      IsTerminal.from
                        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x)
                          terminalIsTerminal
                          (if p₀ ∈ unop U then colimit ((OpenNhds.inclusion p₀).op ⋙ X) else terminal.{u, v} C) ⋯)
                        (X.obj U),
                  naturality := ⋯ : NatTrans X (skyscraperPresheaf p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X))) }) :
            colimit ((OpenNhds.inclusion p₀).op ⋙ X) ⟶
              colimit ((OpenNhds.inclusion p₀).op ⋙ skyscraperPresheaf p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X))))
          (Iso.hom (skyscraperPresheafStalkOfSpecializes p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X)) ⋯) :
            Presheaf.stalk (skyscraperPresheaf p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X))) p₀ ⟶
              colimit ((OpenNhds.inclusion p₀).op ⋙ X))) =
      colimit.ι ((OpenNhds.inclusion p₀).op ⋙ X) j ≫ 𝟙 (colimit ((OpenNhds.inclusion p₀).op ⋙ X))
⊢ CategoryStruct.comp (Y :=
      colimit ((OpenNhds.inclusion p₀).op ⋙ skyscraperPresheaf p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X))))
      (colimMap
          ((OpenNhds.inclusion p₀).op.whiskerLeft
            {
              app := fun (U : (Opens (↑X_1 : Type u))ᵒᵖ) ↦
                if h : p₀ ∈ unop U then X.germ (unop U) p₀ h ≫ 𝟙 (X.stalk p₀) ≫ eqToHom ⋯
                else
                  IsTerminal.from
                    (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
                      (if p₀ ∈ unop U then colimit ((OpenNhds.inclusion p₀).op ⋙ X) else terminal.{u, v} C) ⋯)
                    (X.obj U),
              naturality := ⋯ }) :
        colimit ((OpenNhds.inclusion p₀).op ⋙ X) ⟶
          colimit ((OpenNhds.inclusion p₀).op ⋙ skyscraperPresheaf p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X))))
      (Iso.hom (skyscraperPresheafStalkOfSpecializes p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X)) ⋯) :
        Presheaf.stalk (skyscraperPresheaf p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X))) p₀ ⟶
          colimit ((OpenNhds.inclusion p₀).op ⋙ X)) =
    𝟙 (colimit ((OpenNhds.inclusion p₀).op ⋙ X))

Tactic:
ext
-- Module: Mathlib.Topology.Sheaves.Skyscraper
Goal:
X_1 : TopCat
p₀ : (↑X_1 : Type u)
inst : (U : Opens (↑X_1 : Type u)) → Decidable (p₀ ∈ U)
C : Type v
inst_1 : Category.{u, v} C
A : C
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
X : Presheaf C X_1
j : (OpenNhds p₀)ᵒᵖ
h : p₀ ∈ (OpenNhds.inclusion p₀).obj (unop j)
pos :
  Eq (α := X.obj (op ((OpenNhds.inclusion p₀).obj (unop j))) ⟶ colimit ((OpenNhds.inclusion p₀).op ⋙ X))
    (X.germ ((OpenNhds.inclusion p₀).obj (unop j)) p₀ ⋯ :
      X.obj (op ((OpenNhds.inclusion p₀).obj (unop j))) ⟶ X.stalk p₀)
    (colimit.ι ((OpenNhds.inclusion p₀).op ⋙ X) j)
⊢ CategoryStruct.comp (Y :=
      if p₀ ∈ (OpenNhds.inclusion p₀).obj (unop j) then colimit ((OpenNhds.inclusion p₀).op ⋙ X) else terminal.{u, v} C)
      (X.germ ((OpenNhds.inclusion p₀).obj (unop j)) p₀ ⋯ ≫ 𝟙 (X.stalk p₀) ≫ eqToHom ⋯)
      (CategoryStruct.comp (Y :=
        colimit ((OpenNhds.inclusion p₀).op ⋙ skyscraperPresheaf p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X))))
        (colimit.ι ((OpenNhds.inclusion p₀).op ⋙ skyscraperPresheaf p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X))) j :
          Functor.obj ((OpenNhds.inclusion p₀).op ⋙ skyscraperPresheaf p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X)))
              j ⟶
            colimit ((OpenNhds.inclusion p₀).op ⋙ skyscraperPresheaf p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X))))
        (Iso.hom (skyscraperPresheafStalkOfSpecializes p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X)) ⋯) :
          Presheaf.stalk (skyscraperPresheaf p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X))) p₀ ⟶
            colimit ((OpenNhds.inclusion p₀).op ⋙ X))) =
    colimit.ι ((OpenNhds.inclusion p₀).op ⋙ X) j

Tactic:
simp [skyscraperPresheafStalkOfSpecializes]

Premises used: skyscraperPresheafStalkOfSpecializes
-- Module: Mathlib.Topology.Sheaves.Skyscraper
Goal:
X_1 : TopCat
p₀ : (↑X_1 : Type u)
inst : (U : Opens (↑X_1 : Type u)) → Decidable (p₀ ∈ U)
C : Type v
inst_1 : Category.{u, v} C
A : C
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
X : Presheaf C X_1
j : (OpenNhds p₀)ᵒᵖ
h : p₀ ∈ (OpenNhds.inclusion p₀).obj (unop j)
⊢ Eq (α := X.obj (op ((OpenNhds.inclusion p₀).obj (unop j))) ⟶ colimit ((OpenNhds.inclusion p₀).op ⋙ X))
    (X.germ ((OpenNhds.inclusion p₀).obj (unop j)) p₀ ⋯ :
      X.obj (op ((OpenNhds.inclusion p₀).obj (unop j))) ⟶ X.stalk p₀)
    (colimit.ι ((OpenNhds.inclusion p₀).op ⋙ X) j)

Tactic:
rfl
-- Module: Mathlib.Topology.Sheaves.Skyscraper
Goal:
X_1 : TopCat
p₀ : (↑X_1 : Type u)
inst : (U : Opens (↑X_1 : Type u)) → Decidable (p₀ ∈ U)
C : Type v
inst_1 : Category.{u, v} C
A : C
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
X : Presheaf C X_1
j : (OpenNhds p₀)ᵒᵖ
h : p₀ ∉ (OpenNhds.inclusion p₀).obj (unop j)
neg :
  CategoryStruct.comp (Y :=
      if p₀ ∈ (OpenNhds.inclusion p₀).obj (unop j) then colimit ((OpenNhds.inclusion p₀).op ⋙ X) else terminal.{u, v} C)
      (IsTerminal.from
        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
          (if p₀ ∈ (OpenNhds.inclusion p₀).obj (unop j) then colimit ((OpenNhds.inclusion p₀).op ⋙ X)
          else terminal.{u, v} C)
          ⋯)
        (X.obj (op ((OpenNhds.inclusion p₀).obj (unop j)))))
      (eqToHom ⋯) =
    colimit.ι ((OpenNhds.inclusion p₀).op ⋙ X) j
⊢ CategoryStruct.comp (Y :=
      if p₀ ∈ (OpenNhds.inclusion p₀).obj (unop j) then colimit ((OpenNhds.inclusion p₀).op ⋙ X) else terminal.{u, v} C)
      (IsTerminal.from
        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
          (if p₀ ∈ (OpenNhds.inclusion p₀).obj (unop j) then colimit ((OpenNhds.inclusion p₀).op ⋙ X)
          else terminal.{u, v} C)
          ⋯)
        (X.obj (op ((OpenNhds.inclusion p₀).obj (unop j)))))
      (CategoryStruct.comp (Y :=
        colimit ((OpenNhds.inclusion p₀).op ⋙ skyscraperPresheaf p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X))))
        (colimit.ι ((OpenNhds.inclusion p₀).op ⋙ skyscraperPresheaf p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X))) j :
          Functor.obj ((OpenNhds.inclusion p₀).op ⋙ skyscraperPresheaf p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X)))
              j ⟶
            colimit ((OpenNhds.inclusion p₀).op ⋙ skyscraperPresheaf p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X))))
        (Iso.hom (skyscraperPresheafStalkOfSpecializes p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X)) ⋯) :
          Presheaf.stalk (skyscraperPresheaf p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X))) p₀ ⟶
            colimit ((OpenNhds.inclusion p₀).op ⋙ X))) =
    colimit.ι ((OpenNhds.inclusion p₀).op ⋙ X) j

Tactic:
simp only [skyscraperPresheafStalkOfSpecializes, colimit.isoColimitCocone_ι_hom,
        skyscraperPresheafCoconeOfSpecializes_pt, skyscraperPresheafCoconeOfSpecializes_ι_app,
        Functor.comp_obj, Functor.op_obj, skyscraperPresheaf_obj, Functor.const_obj_obj]

Premises used: CategoryTheory.Functor.comp_obj, skyscraperPresheaf_obj, skyscraperPresheafStalkOfSpecializes, skyscraperPresheafCoconeOfSpecializes_ι_app, CategoryTheory.Functor.const_obj_obj, skyscraperPresheafCoconeOfSpecializes_pt, CategoryTheory.Limits.colimit.isoColimitCocone_ι_hom, CategoryTheory.Functor.op_obj
-- Module: Mathlib.Topology.Sheaves.Skyscraper
Goal:
X_1 : TopCat
p₀ : (↑X_1 : Type u)
inst : (U : Opens (↑X_1 : Type u)) → Decidable (p₀ ∈ U)
C : Type v
inst_1 : Category.{u, v} C
A : C
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
X : Presheaf C X_1
j : (OpenNhds p₀)ᵒᵖ
h : p₀ ∉ (OpenNhds.inclusion p₀).obj (unop j)
neg :
  Eq (α :=
    X.obj (op ((OpenNhds.inclusion p₀).obj (unop j))) ⟶
      if p₀ ∈ (OpenNhds.inclusion p₀).obj (unop j) then colimit ((OpenNhds.inclusion p₀).op ⋙ X) else terminal.{u, v} C)
    (IsTerminal.from
      (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
        (if p₀ ∈ (OpenNhds.inclusion p₀).obj (unop j) then colimit ((OpenNhds.inclusion p₀).op ⋙ X)
        else terminal.{u, v} C)
        ⋯)
      (X.obj (op ((OpenNhds.inclusion p₀).obj (unop j)))))
    (colimit.ι ((OpenNhds.inclusion p₀).op ⋙ X) j ≫ eqToHom ⋯)
⊢ CategoryStruct.comp (Y :=
      if p₀ ∈ (OpenNhds.inclusion p₀).obj (unop j) then colimit ((OpenNhds.inclusion p₀).op ⋙ X) else terminal.{u, v} C)
      (IsTerminal.from
        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
          (if p₀ ∈ (OpenNhds.inclusion p₀).obj (unop j) then colimit ((OpenNhds.inclusion p₀).op ⋙ X)
          else terminal.{u, v} C)
          ⋯)
        (X.obj (op ((OpenNhds.inclusion p₀).obj (unop j)))))
      (eqToHom ⋯) =
    colimit.ι ((OpenNhds.inclusion p₀).op ⋙ X) j

Tactic:
rw [comp_eqToHom_iff]

Premises used: CategoryTheory.comp_eqToHom_iff
-- Module: Mathlib.Topology.Sheaves.Skyscraper
Goal:
X_1 : TopCat
p₀ : (↑X_1 : Type u)
inst : (U : Opens (↑X_1 : Type u)) → Decidable (p₀ ∈ U)
C : Type v
inst_1 : Category.{u, v} C
A : C
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
X : Presheaf C X_1
j : (OpenNhds p₀)ᵒᵖ
h : p₀ ∉ (OpenNhds.inclusion p₀).obj (unop j)
⊢ Eq (α :=
    X.obj (op ((OpenNhds.inclusion p₀).obj (unop j))) ⟶
      if p₀ ∈ (OpenNhds.inclusion p₀).obj (unop j) then colimit ((OpenNhds.inclusion p₀).op ⋙ X) else terminal.{u, v} C)
    (IsTerminal.from
      (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
        (if p₀ ∈ (OpenNhds.inclusion p₀).obj (unop j) then colimit ((OpenNhds.inclusion p₀).op ⋙ X)
        else terminal.{u, v} C)
        ⋯)
      (X.obj (op ((OpenNhds.inclusion p₀).obj (unop j)))))
    (colimit.ι ((OpenNhds.inclusion p₀).op ⋙ X) j ≫ eqToHom ⋯)

Tactic:
apply ((if_neg h).symm.ndrec terminalIsTerminal).hom_ext

Premises used: Eq.ndrec, CategoryTheory.Limits.IsTerminal.hom_ext, CategoryTheory.Limits.terminalIsTerminal, Eq.symm, if_neg