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
y : (↑X : Type u)
h : p₀ ⤳ y
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
U : (OpenNhds y)ᵒᵖ
⊢ eqToHom ⋯ ≫ eqToHom ⋯ ≫ eqToHom ⋯ ≫ c.ι.app (op (unop U)) = c.ι.app U

Tactic:
simp only [eqToHom_trans_assoc,
        eqToHom_refl, Category.id_comp, op_unop]

Premises used: Opposite.op_unop, CategoryTheory.eqToHom_refl, CategoryTheory.eqToHom_trans_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
y : (↑X : Type u)
h : p₀ ⤳ y
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
U : (OpenNhds y)ᵒᵖ
⊢ p₀ ∈ unop ((OpenNhds.inclusion y).op.obj (op (unop U)))

Tactic:
h.mem_open U.unop.1.2 U.unop.2

Premises used: Specializes.mem_open, TopologicalSpace.Opens.is_open', Subtype.val, Opposite.unop, Subtype.property
-- 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
y : (↑X : Type u)
h : p₀ ⤳ y
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
U : (OpenNhds y)ᵒᵖ
⊢ p₀ ∈ unop ((OpenNhds.inclusion y).op.obj (op (unop U)))

Tactic:
exact h.mem_open U.unop.1.2 U.unop.2

Premises used: Specializes.mem_open, TopologicalSpace.Opens.is_open', Subtype.val, Opposite.unop, Subtype.property
-- 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
y : (↑X : Type u)
h_1 : p₀ ⤳ y
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
f :
  Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
      (skyscraperPresheafCoconeOfSpecializes p₀ A h_1) ⟶
    c.pt
h : ∀ (j : (OpenNhds y)ᵒᵖ), NatTrans.app (Cocone.ι (skyscraperPresheafCoconeOfSpecializes p₀ A h_1)) j ≫ f = c.ι.app j
dsimp : f = CategoryStruct.comp (Y := if True then A else terminal.{u, v} C) (eqToHom ⋯) (c.ι.app (op ⊤))
⊢ f =
    CategoryStruct.comp (Y :=
      if True then
        Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
          (skyscraperPresheafCoconeOfSpecializes p₀ A h_1)
      else terminal.{u, v} C)
      (eqToHom ⋯) (c.ι.app (op ⊤))

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
y : (↑X : Type u)
h_1 : p₀ ⤳ y
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
f :
  Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
      (skyscraperPresheafCoconeOfSpecializes p₀ A h_1) ⟶
    c.pt
h : ∀ (j : (OpenNhds y)ᵒᵖ), NatTrans.app (Cocone.ι (skyscraperPresheafCoconeOfSpecializes p₀ A h_1)) j ≫ f = c.ι.app j
rw :
  f =
    CategoryStruct.comp (Y := if True then A else terminal.{u, v} C) (eqToHom ⋯)
      (NatTrans.app (Cocone.ι (skyscraperPresheafCoconeOfSpecializes p₀ A h_1)) (op ⊤) ≫ f)
rw₁ : f = CategoryStruct.comp (Y := if True then A else terminal.{u, v} C) (eqToHom ⋯) (eqToHom ⋯ ≫ f)
rw₂ : f = eqToHom ⋯ ≫ f
rw₃ : f = 𝟙 A ≫ f
rw₄ rw₅ : f = f
⊢ f = CategoryStruct.comp (Y := if True then A else terminal.{u, v} C) (eqToHom ⋯) (c.ι.app (op ⊤))

Tactic:
rw [← h, skyscraperPresheafCoconeOfSpecializes_ι_app, eqToHom_trans_assoc, eqToHom_refl,
      Category.id_comp]

Premises used: CategoryTheory.eqToHom_refl, skyscraperPresheafCoconeOfSpecializes_ι_app, CategoryTheory.eqToHom_trans_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
y : (↑X : Type u)
h : p₀ ⤳ y
U : Opens (↑X : Type u)
hU : y ∈ U
⊢ Eq (α := Functor.obj (skyscraperPresheaf p₀ A) (op U) ⟶ A)
    (CategoryStruct.comp (Y := Presheaf.stalk (skyscraperPresheaf p₀ A) y)
      (Presheaf.germ (skyscraperPresheaf p₀ A) U y hU) (Iso.hom (skyscraperPresheafStalkOfSpecializes p₀ A h)))
    (eqToHom ⋯)

Tactic:
colimit.isoColimitCocone_ι_hom _ _

Premises used: Eq.mpr, Set.Mem, CategoryTheory.eqToHom, CategoryTheory.Functor.comp, TopCat.Presheaf, TopCat.Presheaf.stalk, CategoryTheory.Limits.colimit, TopCat.Presheaf.germ, TopologicalSpace.OpenNhds, CategoryTheory.Limits.colimit.isoColimitCocone_ι_hom, ite
-- 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
y : (↑X : Type u)
h : ¬p₀ ⤳ y
h1 : ∃ (U : OpenNhds y), p₀ ∉ (↑U : Opens (↑X : Type u)) := ⋯
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
U : (OpenNhds y)ᵒᵖ
change :
  CategoryStruct.comp (Y :=
      Functor.obj
        (Functor.obj (Functor.const (OpenNhds y)ᵒᵖ)
          (Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (skyscraperPresheafCocone p₀ A y)))
        U)
      (NatTrans.app (Cocone.ι (skyscraperPresheafCocone p₀ A y)) U)
      (CategoryStruct.comp (Y :=
        if p₀ ∈ (↑(h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u)))) : Opens (↑X : Type u)) then
          A
        else Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (skyscraperPresheafCocone p₀ A y))
        (eqToHom ⋯) (c.ι.app (op (h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u))))))) =
    c.ι.app (op (unop U))
⊢ CategoryStruct.comp (Y :=
      Functor.obj
        (Functor.obj (Functor.const (OpenNhds y)ᵒᵖ)
          (Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (skyscraperPresheafCocone p₀ A y)))
        U)
      (NatTrans.app (Cocone.ι (skyscraperPresheafCocone p₀ A y)) U)
      (CategoryStruct.comp (Y :=
        if p₀ ∈ (↑(h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u)))) : Opens (↑X : Type u)) then
          A
        else Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (skyscraperPresheafCocone p₀ A y))
        (eqToHom ⋯) (c.ι.app (op (h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u))))))) =
    c.ι.app U

Tactic:
change _ = c.ι.app (op U.unop)

Premises used: CategoryTheory.Limits.Cocone.ι, Opposite.op, Opposite.unop, CategoryTheory.NatTrans.app
-- 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
y : (↑X : Type u)
h : ¬p₀ ⤳ y
h1 : ∃ (U : OpenNhds y), p₀ ∉ (↑U : Opens (↑X : Type u)) := ⋯
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
U : (OpenNhds y)ᵒᵖ
⊢ Eq (α :=
    Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) U ⟶
      Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
        (op (h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u))) ⊓ unop U)))
    (CategoryStruct.comp (Y :=
      if p₀ ∈ (↑(h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u)))) : Opens (↑X : Type u)) then A
      else Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (skyscraperPresheafCocone p₀ A y))
      (CategoryStruct.comp (Y :=
          Functor.obj
            (Functor.obj (Functor.const (OpenNhds y)ᵒᵖ)
              (Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (skyscraperPresheafCocone p₀ A y)))
            U)
          (NatTrans.app (Cocone.ι (skyscraperPresheafCocone p₀ A y)) U) (eqToHom ⋯) :
        Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) U ⟶
          if
              p₀ ∈
                (↑(h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u)))) : Opens (↑X : Type u)) then
            A
          else Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (skyscraperPresheafCocone p₀ A y))
      (CategoryTheory.Functor.map ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (Quiver.Hom.op (homOfLE ⋯)) :
        Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
            (op (h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u))))) ⟶
          Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
            (op (h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u))) ⊓ unop U))))
    (CategoryTheory.Functor.map ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (Quiver.Hom.op (homOfLE ⋯)))

Tactic:
((if_neg ?_).symm.ndrec terminalIsTerminal).hom_ext _ _

Premises used: Eq.ndrec, CategoryTheory.Limits.IsTerminal.hom_ext, CategoryTheory.Limits.terminalIsTerminal, Eq.symm, if_neg, ite
-- 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
y : (↑X : Type u)
h : ¬p₀ ⤳ y
h1 : ∃ (U : OpenNhds y), p₀ ∉ (↑U : Opens (↑X : Type u)) := ⋯
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
U : (OpenNhds y)ᵒᵖ
e_a :
  p₀ ∉
    unop
      ((OpenNhds.inclusion y).op.obj
        (op (h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u))) ⊓ unop U)))
⊢ Eq (α :=
    Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) U ⟶
      Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
        (op (h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u))) ⊓ unop U)))
    (CategoryStruct.comp (Y :=
      if p₀ ∈ (↑(h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u)))) : Opens (↑X : Type u)) then A
      else Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (skyscraperPresheafCocone p₀ A y))
      (CategoryStruct.comp (Y :=
          Functor.obj
            (Functor.obj (Functor.const (OpenNhds y)ᵒᵖ)
              (Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (skyscraperPresheafCocone p₀ A y)))
            U)
          (NatTrans.app (Cocone.ι (skyscraperPresheafCocone p₀ A y)) U) (eqToHom ⋯) :
        Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) U ⟶
          if
              p₀ ∈
                (↑(h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u)))) : Opens (↑X : Type u)) then
            A
          else Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (skyscraperPresheafCocone p₀ A y))
      (CategoryTheory.Functor.map ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (Quiver.Hom.op (homOfLE ⋯)) :
        Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
            (op (h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u))))) ⟶
          Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
            (op (h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u))) ⊓ unop U))))
    (CategoryTheory.Functor.map ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (Quiver.Hom.op (homOfLE ⋯)))

Tactic:
refine ((if_neg ?_).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
y : (↑X : Type u)
h : ¬p₀ ⤳ y
h1 : ∃ (U : OpenNhds y), p₀ ∉ (↑U : Opens (↑X : Type u)) := ⋯
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
U : (OpenNhds y)ᵒᵖ
⊢ p₀ ∉
    unop
      ((OpenNhds.inclusion y).op.obj
        (op (h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u))) ⊓ unop U)))

Tactic:
fun h => h1.choose_spec h.1

Premises used: Exists.choose_spec, And.left, Not
-- 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
y : (↑X : Type u)
h : ¬p₀ ⤳ y
h1 : ∃ (U : OpenNhds y), p₀ ∉ (↑U : Opens (↑X : Type u)) := ⋯
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
U : (OpenNhds y)ᵒᵖ
⊢ p₀ ∉
    unop
      ((OpenNhds.inclusion y).op.obj
        (op (h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u))) ⊓ unop U)))

Tactic:
exact fun h => h1.choose_spec h.1

Premises used: Exists.choose_spec
-- 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
y : (↑X : Type u)
h : ¬p₀ ⤳ y
h1 : ∃ (U : OpenNhds y), p₀ ∉ (↑U : Opens (↑X : Type u)) := ⋯
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
f : Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (skyscraperPresheafCocone p₀ A y) ⟶ c.pt
H : ∀ (j : (OpenNhds y)ᵒᵖ), NatTrans.app (Cocone.ι (skyscraperPresheafCocone p₀ A y)) j ≫ f = c.ι.app j
dsimp :
  f =
    CategoryStruct.comp (Y :=
      if p₀ ∈ (↑(h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u)))) : Opens (↑X : Type u)) then A
      else terminal.{u, v} C)
      (eqToHom ⋯) (c.ι.app (op (h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u))))))
⊢ f =
    CategoryStruct.comp (Y :=
      if p₀ ∈ (↑(h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u)))) : Opens (↑X : Type u)) then A
      else Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (skyscraperPresheafCocone p₀ A y))
      (eqToHom ⋯) (c.ι.app (op (h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type 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
y : (↑X : Type u)
h : ¬p₀ ⤳ y
h1 : ∃ (U : OpenNhds y), p₀ ∉ (↑U : Opens (↑X : Type u)) := ⋯
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
f : Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (skyscraperPresheafCocone p₀ A y) ⟶ c.pt
H : ∀ (j : (OpenNhds y)ᵒᵖ), NatTrans.app (Cocone.ι (skyscraperPresheafCocone p₀ A y)) j ≫ f = c.ι.app j
rw :
  𝟙 (Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (skyscraperPresheafCocone p₀ A y)) ≫ f =
    CategoryStruct.comp (Y :=
        if p₀ ∈ (↑(h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u)))) : Opens (↑X : Type u)) then
          A
        else terminal.{u, v} C)
        (eqToHom ⋯)
        (NatTrans.app (Cocone.ι (skyscraperPresheafCocone p₀ A y))
          (op (h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u)))))) ≫
      f
⊢ f =
    CategoryStruct.comp (Y :=
      if p₀ ∈ (↑(h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u)))) : Opens (↑X : Type u)) then A
      else terminal.{u, v} C)
      (eqToHom ⋯) (c.ι.app (op (h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u))))))

Tactic:
rw [← Category.id_comp f, ← H, ← Category.assoc]

Premises used: CategoryTheory.Category.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
y : (↑X : Type u)
h : ¬p₀ ⤳ y
h1 : ∃ (U : OpenNhds y), p₀ ∉ (↑U : Opens (↑X : Type u)) := ⋯
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
f : Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (skyscraperPresheafCocone p₀ A y) ⟶ c.pt
H : ∀ (j : (OpenNhds y)ᵒᵖ), NatTrans.app (Cocone.ι (skyscraperPresheafCocone p₀ A y)) j ≫ f = c.ι.app j
e_a :
  Eq.{u + 1} (α :=
    Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (skyscraperPresheafCocone p₀ A y) ⟶
      Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (skyscraperPresheafCocone p₀ A y))
    (𝟙 (Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (skyscraperPresheafCocone p₀ A y)))
    (CategoryStruct.comp (Y :=
      if p₀ ∈ (↑(h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u)))) : Opens (↑X : Type u)) then A
      else terminal.{u, v} C)
      (eqToHom ⋯)
      (NatTrans.app (Cocone.ι (skyscraperPresheafCocone p₀ A y))
        (op (h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u)))))))
⊢ 𝟙 (Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (skyscraperPresheafCocone p₀ A y)) ≫ f =
    CategoryStruct.comp (Y :=
        if p₀ ∈ (↑(h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u)))) : Opens (↑X : Type u)) then
          A
        else terminal.{u, v} C)
        (eqToHom ⋯)
        (NatTrans.app (Cocone.ι (skyscraperPresheafCocone p₀ A y))
          (op (h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u)))))) ≫
      f

Tactic:
congr 1
-- 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
y : (↑X : Type u)
h : ¬p₀ ⤳ y
h1 : ∃ (U : OpenNhds y), p₀ ∉ (↑U : Opens (↑X : Type u)) := ⋯
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
f : Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (skyscraperPresheafCocone p₀ A y) ⟶ c.pt
H : ∀ (j : (OpenNhds y)ᵒᵖ), NatTrans.app (Cocone.ι (skyscraperPresheafCocone p₀ A y)) j ≫ f = c.ι.app j
⊢ Eq.{u + 1} (α :=
    Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (skyscraperPresheafCocone p₀ A y) ⟶
      Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (skyscraperPresheafCocone p₀ A y))
    (𝟙 (Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (skyscraperPresheafCocone p₀ A y)))
    (CategoryStruct.comp (Y :=
      if p₀ ∈ (↑(h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u)))) : Opens (↑X : Type u)) then A
      else terminal.{u, v} C)
      (eqToHom ⋯)
      (NatTrans.app (Cocone.ι (skyscraperPresheafCocone p₀ A y))
        (op (h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u)))))))

Tactic:
apply terminalIsTerminal.hom_ext

Premises used: CategoryTheory.Limits.IsTerminal.hom_ext, CategoryTheory.Limits.terminalIsTerminal
-- 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
dsimp : IsTerminal.{u, v} (if Membership.mem (γ := Opens PUnit.{u + 1}) ⊥ PUnit.unit then A else terminal.{u, v} C)
⊢ IsTerminal.{u, v}
    (Functor.obj.{u, u, u, v} (C := (Opens (↑(of PUnit.{u + 1}) : Type u))ᵒᵖ) (skyscraperPresheaf PUnit.unit A) (op ⊥))

Tactic:
dsimp [skyscraperPresheaf]

Premises used: skyscraperPresheaf
-- 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
rw : IsTerminal.{u, v} (terminal.{u, v} C)
hnc : PUnit.unit ∉ ⊥
⊢ IsTerminal.{u, v} (if Membership.mem (γ := Opens PUnit.{u + 1}) ⊥ PUnit.unit then A else terminal.{u, v} C)

Tactic:
rw [if_neg]

Premises used: 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
⊢ IsTerminal.{u, v} (terminal.{u, v} C)

Tactic:
exact terminalIsTerminal

Premises used: CategoryTheory.Limits.terminalIsTerminal
-- 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
⊢ PUnit.unit ∉ ⊥

Tactic:
Set.notMem_empty PUnit.unit.{u + 1}

Premises used: Set.Mem, Set.notMem_empty, PUnit.unit
-- 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
⊢ PUnit.unit ∉ ⊥

Tactic:
exact Set.notMem_empty PUnit.unit.{u + 1}
-- 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
⊢ TopCat.Presheaf.IsSheaf (skyscraperPresheaf p₀ A)

Tactic:
exact
    (Presheaf.isSheaf_iso_iff (eqToIso <| skyscraperPresheaf_eq_pushforward p₀ A)).mpr <|
      (Sheaf.pushforward_sheaf_of_sheaf _
        (Presheaf.isSheaf_on_punit_of_isTerminal _ (by
          dsimp [skyscraperPresheaf]
          rw [if_neg]
          · exact terminalIsTerminal
          · #adaptation_note /-- 2024-03-24
            Previously the universe annotation was not needed here. -/
            exact Set.notMem_empty PUnit.unit.{u + 1})))

Premises used: Iff.mpr, TopCat.Sheaf.pushforward_sheaf_of_sheaf, CategoryTheory.eqToIso, TopCat.Presheaf.isSheaf_on_punit_of_isTerminal, skyscraperPresheaf_eq_pushforward, TopCat.Presheaf.isSheaf_iso_iff
-- 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
⊢ TopCat.Presheaf.IsSheaf (skyscraperPresheaf p₀ A)

Tactic:
classical exact
    (Presheaf.isSheaf_iso_iff (eqToIso <| skyscraperPresheaf_eq_pushforward p₀ A)).mpr <|
      (Sheaf.pushforward_sheaf_of_sheaf _
        (Presheaf.isSheaf_on_punit_of_isTerminal _ (by
          dsimp [skyscraperPresheaf]
          rw [if_neg]
          · exact terminalIsTerminal
          · #adaptation_note /-- 2024-03-24
            Previously the universe annotation was not needed here. -/
            exact Set.notMem_empty PUnit.unit.{u + 1})))

Premises used: TopCat.Sheaf.pushforward_sheaf_of_sheaf, TopCat.Presheaf.isSheaf_on_punit_of_isTerminal