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
c : C
f : 𝓕.stalk p₀ ⟶ c
U V : (Opens (↑X : Type u))ᵒᵖ
inc : U ⟶ V
dsimp :
  Eq (α := 𝓕.obj U ⟶ if p₀ ∈ unop V then c else terminal.{u, v} C)
    (𝓕.map inc ≫
      if h : p₀ ∈ unop V then 𝓕.germ (unop V) p₀ h ≫ f ≫ eqToHom ⋯
      else
        IsTerminal.from
          (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
            (if p₀ ∈ unop V then c else terminal.{u, v} C) ⋯)
          (𝓕.obj V))
    (CategoryStruct.comp (Y := if p₀ ∈ unop U then c else terminal.{u, v} C)
      (if h : p₀ ∈ unop U then 𝓕.germ (unop U) p₀ h ≫ f ≫ 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 c else terminal.{u, v} C) ⋯)
          (𝓕.obj U))
      (if h : p₀ ∈ unop V then eqToHom ⋯
      else
        IsTerminal.from
          (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
            (if p₀ ∈ unop V then c else terminal.{u, v} C) ⋯)
          (if p₀ ∈ unop U then c else terminal.{u, v} C)))
⊢ Eq (α := 𝓕.obj U ⟶ Functor.obj (skyscraperPresheaf p₀ c) V)
    (𝓕.map inc ≫
      if h : p₀ ∈ unop V then 𝓕.germ (unop V) p₀ h ≫ f ≫ eqToHom ⋯
      else IsTerminal.from (Eq.ndrec (motive := IsTerminal.{u, v}) terminalIsTerminal ⋯) (𝓕.obj V))
    ((if h : p₀ ∈ unop U then 𝓕.germ (unop U) p₀ h ≫ f ≫ eqToHom ⋯
      else IsTerminal.from (Eq.ndrec (motive := IsTerminal.{u, v}) terminalIsTerminal ⋯) (𝓕.obj U)) ≫
      CategoryTheory.Functor.map (skyscraperPresheaf p₀ c) inc)

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
c : C
f : 𝓕.stalk p₀ ⟶ c
U V : (Opens (↑X : Type u))ᵒᵖ
inc : U ⟶ V
hV : p₀ ∈ unop V
⊢ p₀ ∈ unop U

Tactic:
have hU : p₀ ∈ U.unop := leOfHom inc.unop hV
-- 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
c : C
f : 𝓕.stalk p₀ ⟶ c
U V : (Opens (↑X : Type u))ᵒᵖ
inc : U ⟶ V
hV : p₀ ∈ unop V
hU : p₀ ∈ unop U
pos :
  Eq (α := 𝓕.obj U ⟶ if p₀ ∈ unop V then c else terminal.{u, v} C) (𝓕.map inc ≫ 𝓕.germ (unop V) p₀ hV ≫ f ≫ eqToHom ⋯)
    ((𝓕.germ (unop U) p₀ hU ≫ f ≫ eqToHom ⋯) ≫ eqToHom ⋯)
⊢ Eq (α := 𝓕.obj U ⟶ if p₀ ∈ unop V then c else terminal.{u, v} C)
    (𝓕.map inc ≫
      if h : p₀ ∈ unop V then 𝓕.germ (unop V) p₀ h ≫ f ≫ eqToHom ⋯
      else
        IsTerminal.from
          (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
            (if p₀ ∈ unop V then c else terminal.{u, v} C) ⋯)
          (𝓕.obj V))
    (CategoryStruct.comp (Y := if p₀ ∈ unop U then c else terminal.{u, v} C)
      (if h : p₀ ∈ unop U then 𝓕.germ (unop U) p₀ h ≫ f ≫ 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 c else terminal.{u, v} C) ⋯)
          (𝓕.obj U))
      (if h : p₀ ∈ unop V then eqToHom ⋯
      else
        IsTerminal.from
          (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
            (if p₀ ∈ unop V then c else terminal.{u, v} C) ⋯)
          (if p₀ ∈ unop U then c else terminal.{u, v} C)))

Tactic:
split_ifs
-- 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
c : C
f : 𝓕.stalk p₀ ⟶ c
U V : (Opens (↑X : Type u))ᵒᵖ
inc : U ⟶ V
hV : p₀ ∈ unop V
hU : p₀ ∈ unop U
pos :
  Eq (α := 𝓕.obj U ⟶ if p₀ ∈ unop V then c else terminal.{u, v} C) ((𝓕.map inc ≫ 𝓕.germ (unop V) p₀ hV) ≫ f ≫ eqToHom ⋯)
    ((𝓕.germ (unop U) p₀ hU ≫ f ≫ eqToHom ⋯) ≫ eqToHom ⋯)
pos₁ :
  Eq (α := 𝓕.obj U ⟶ if p₀ ∈ unop V then c else terminal.{u, v} C) (𝓕.germ (unop U) p₀ ⋯ ≫ f ≫ eqToHom ⋯)
    ((𝓕.germ (unop U) p₀ hU ≫ f ≫ eqToHom ⋯) ≫ eqToHom ⋯)
pos₂ :
  Eq (α := 𝓕.obj U ⟶ if p₀ ∈ unop V then c else terminal.{u, v} C) (𝓕.germ (unop U) p₀ ⋯ ≫ f ≫ eqToHom ⋯)
    (𝓕.germ (unop U) p₀ hU ≫ (f ≫ eqToHom ⋯) ≫ eqToHom ⋯)
pos₃ :
  Eq (α := 𝓕.obj U ⟶ if p₀ ∈ unop V then c else terminal.{u, v} C) (𝓕.germ (unop U) p₀ ⋯ ≫ f ≫ eqToHom ⋯)
    (𝓕.germ (unop U) p₀ hU ≫ f ≫ eqToHom ⋯ ≫ eqToHom ⋯)
pos₄ pos₅ :
  Eq (α := 𝓕.obj U ⟶ if p₀ ∈ unop V then c else terminal.{u, v} C) (𝓕.germ (unop U) p₀ ⋯ ≫ f ≫ eqToHom ⋯)
    (𝓕.germ (unop U) p₀ hU ≫ f ≫ eqToHom ⋯)
⊢ Eq (α := 𝓕.obj U ⟶ if p₀ ∈ unop V then c else terminal.{u, v} C) (𝓕.map inc ≫ 𝓕.germ (unop V) p₀ hV ≫ f ≫ eqToHom ⋯)
    ((𝓕.germ (unop U) p₀ hU ≫ f ≫ eqToHom ⋯) ≫ eqToHom ⋯)

Tactic:
rw [← Category.assoc, 𝓕.germ_res' inc, Category.assoc, Category.assoc, eqToHom_trans]

Premises used: CategoryTheory.Category.assoc, TopCat.Presheaf.germ_res', CategoryTheory.eqToHom_trans
-- 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
c : C
f : 𝓕.stalk p₀ ⟶ c
U V : (Opens (↑X : Type u))ᵒᵖ
inc : U ⟶ V
hV : p₀ ∉ unop V
neg :
  Eq (α := 𝓕.obj U ⟶ if p₀ ∈ unop V then c else terminal.{u, v} C)
    (𝓕.map inc ≫
      IsTerminal.from
        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
          (if p₀ ∈ unop V then c else terminal.{u, v} C) ⋯)
        (𝓕.obj V))
    ((if h : p₀ ∈ unop U then 𝓕.germ (unop U) p₀ h ≫ f ≫ 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 c else terminal.{u, v} C) ⋯)
          (𝓕.obj U)) ≫
      IsTerminal.from
        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
          (if p₀ ∈ unop V then c else terminal.{u, v} C) ⋯)
        (if p₀ ∈ unop U then c else terminal.{u, v} C))
⊢ Eq (α := 𝓕.obj U ⟶ if p₀ ∈ unop V then c else terminal.{u, v} C)
    (𝓕.map inc ≫
      if h : p₀ ∈ unop V then 𝓕.germ (unop V) p₀ h ≫ f ≫ eqToHom ⋯
      else
        IsTerminal.from
          (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
            (if p₀ ∈ unop V then c else terminal.{u, v} C) ⋯)
          (𝓕.obj V))
    (CategoryStruct.comp (Y := if p₀ ∈ unop U then c else terminal.{u, v} C)
      (if h : p₀ ∈ unop U then 𝓕.germ (unop U) p₀ h ≫ f ≫ 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 c else terminal.{u, v} C) ⋯)
          (𝓕.obj U))
      (if h : p₀ ∈ unop V then eqToHom ⋯
      else
        IsTerminal.from
          (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
            (if p₀ ∈ unop V then c else terminal.{u, v} C) ⋯)
          (if p₀ ∈ unop U then c else terminal.{u, v} C)))

Tactic:
split_ifs
-- 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
c : C
f : 𝓕.stalk p₀ ⟶ c
U V : (Opens (↑X : Type u))ᵒᵖ
inc : U ⟶ V
hV : p₀ ∉ unop V
⊢ Eq (α := 𝓕.obj U ⟶ if p₀ ∈ unop V then c else terminal.{u, v} C)
    (𝓕.map inc ≫
      IsTerminal.from
        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
          (if p₀ ∈ unop V then c else terminal.{u, v} C) ⋯)
        (𝓕.obj V))
    ((if h : p₀ ∈ unop U then 𝓕.germ (unop U) p₀ h ≫ f ≫ 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 c else terminal.{u, v} C) ⋯)
          (𝓕.obj U)) ≫
      IsTerminal.from
        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
          (if p₀ ∈ unop V then c else terminal.{u, v} C) ⋯)
        (if p₀ ∈ unop U then c else terminal.{u, v} C))

Tactic:
((if_neg hV).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
𝓕 : Presheaf C X
c : C
f : 𝓕.stalk p₀ ⟶ c
U V : (Opens (↑X : Type u))ᵒᵖ
inc : U ⟶ V
hV : p₀ ∉ unop V
⊢ Eq (α := 𝓕.obj U ⟶ if p₀ ∈ unop V then c else terminal.{u, v} C)
    (𝓕.map inc ≫
      IsTerminal.from
        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
          (if p₀ ∈ unop V then c else terminal.{u, v} C) ⋯)
        (𝓕.obj V))
    ((if h : p₀ ∈ unop U then 𝓕.germ (unop U) p₀ h ≫ f ≫ 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 c else terminal.{u, v} C) ⋯)
          (𝓕.obj U)) ≫
      IsTerminal.from
        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
          (if p₀ ∈ unop V then c else terminal.{u, v} C) ⋯)
        (if p₀ ∈ unop U then c else terminal.{u, v} C))

Tactic:
exact ((if_neg hV).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
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U V : (OpenNhds p₀)ᵒᵖ
inc : U ⟶ V
dsimp :
  𝓕.map ((OpenNhds.inclusion p₀).op.map inc) ≫ f.app (op ((OpenNhds.inclusion p₀).obj (unop V))) ≫ eqToHom ⋯ =
    (f.app (op ((OpenNhds.inclusion p₀).obj (unop U))) ≫ eqToHom ⋯) ≫ 𝟙 c
⊢ Eq (α := ((OpenNhds.inclusion p₀).op ⋙ 𝓕).obj U ⟶ Functor.obj (Functor.obj (Functor.const (OpenNhds p₀)ᵒᵖ) c) V)
    (((OpenNhds.inclusion p₀).op ⋙ 𝓕).map inc ≫ f.app ((OpenNhds.inclusion p₀).op.obj V) ≫ eqToHom ⋯)
    ((f.app ((OpenNhds.inclusion p₀).op.obj U) ≫ eqToHom ⋯) ≫
      CategoryTheory.Functor.map (Functor.obj (Functor.const (OpenNhds p₀)ᵒᵖ) c) inc)

Tactic:
dsimp only [Functor.const_obj_map, Functor.const_obj_obj, Functor.comp_map,
            Functor.comp_obj, Functor.op_obj, skyscraperPresheaf_obj]

Premises used: CategoryTheory.Functor.comp_obj, skyscraperPresheaf_obj, CategoryTheory.Functor.const_obj_obj, CategoryTheory.Functor.const_obj_map, CategoryTheory.Functor.comp_map, CategoryTheory.Functor.op_obj
-- 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
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U V : (OpenNhds p₀)ᵒᵖ
inc : U ⟶ V
rw :
  Eq (α :=
    𝓕.obj (op ((OpenNhds.inclusion p₀).obj (unop U))) ⟶
      if p₀ ∈ (OpenNhds.inclusion p₀).obj (unop V) then c else terminal.{u, v} C)
    (f.app (op ((OpenNhds.inclusion p₀).obj (unop U))) ≫
      if h : p₀ ∈ unop (op ((OpenNhds.inclusion p₀).obj (unop V))) then eqToHom ⋯
      else
        IsTerminal.from (Eq.ndrec (motive := IsTerminal.{u, v}) terminalIsTerminal ⋯)
          (if p₀ ∈ unop (op ((OpenNhds.inclusion p₀).obj (unop U))) then c else terminal.{u, v} C))
    (f.app (op ((OpenNhds.inclusion p₀).obj (unop U))) ≫ eqToHom ⋯)
⊢ 𝓕.map ((OpenNhds.inclusion p₀).op.map inc) ≫ f.app (op ((OpenNhds.inclusion p₀).obj (unop V))) ≫ eqToHom ⋯ =
    (f.app (op ((OpenNhds.inclusion p₀).obj (unop U))) ≫ eqToHom ⋯) ≫ 𝟙 c

Tactic:
rw [Category.comp_id, ← Category.assoc, comp_eqToHom_iff, Category.assoc,
            eqToHom_trans, f.naturality, skyscraperPresheaf_map]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.NatTrans.naturality, CategoryTheory.comp_eqToHom_iff, CategoryTheory.eqToHom_trans, skyscraperPresheaf_map
-- 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
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U V : (OpenNhds p₀)ᵒᵖ
inc : U ⟶ V
⊢ p₀ ∈ (OpenNhds.inclusion p₀).obj (unop V)

Tactic:
have hV : p₀ ∈ (OpenNhds.inclusion p₀).obj V.unop := V.unop.2
-- 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
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U V : (OpenNhds p₀)ᵒᵖ
inc : U ⟶ V
hV : p₀ ∈ (OpenNhds.inclusion p₀).obj (unop V)
⊢ Eq (α :=
    𝓕.obj (op ((OpenNhds.inclusion p₀).obj (unop U))) ⟶
      if p₀ ∈ (OpenNhds.inclusion p₀).obj (unop V) then c else terminal.{u, v} C)
    (f.app (op ((OpenNhds.inclusion p₀).obj (unop U))) ≫
      if h : p₀ ∈ unop (op ((OpenNhds.inclusion p₀).obj (unop V))) then eqToHom ⋯
      else
        IsTerminal.from (Eq.ndrec (motive := IsTerminal.{u, v}) terminalIsTerminal ⋯)
          (if p₀ ∈ unop (op ((OpenNhds.inclusion p₀).obj (unop U))) then c else terminal.{u, v} C))
    (f.app (op ((OpenNhds.inclusion p₀).obj (unop U))) ≫ eqToHom ⋯)

Tactic:
simp only [dif_pos hV]

Premises used: dif_pos
-- 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
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U : Opens (↑X : Type u)
hU : p₀ ∈ U
⊢ CategoryStruct.comp (Y := 𝓕.stalk p₀) (𝓕.germ U p₀ hU) (fromStalk p₀ f) = f.app (op U) ≫ eqToHom ⋯

Tactic:
colimit.ι_desc _ _

Premises used: Set.Mem, CategoryTheory.Functor.comp, TopCat.Presheaf.stalk, CategoryTheory.Limits.colimit, TopCat.Presheaf.germ, StalkSkyscraperPresheafAdjunctionAuxs.fromStalk, CategoryTheory.Limits.colimit.ι_desc
-- 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
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
app : NatTrans.app (toSkyscraperPresheaf p₀ (fromStalk p₀ f)) = f.app
⊢ toSkyscraperPresheaf p₀ (fromStalk p₀ f) = f

Tactic:
apply NatTrans.ext

Premises used: CategoryTheory.NatTrans.ext
-- 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
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
app : ∀ (U : (Opens (↑X : Type u))ᵒᵖ), NatTrans.app (toSkyscraperPresheaf p₀ (fromStalk p₀ f)) U = f.app U
⊢ NatTrans.app (toSkyscraperPresheaf p₀ (fromStalk p₀ f)) = f.app

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
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U : (Opens (↑X : Type u))ᵒᵖ
app :
  (if h : p₀ ∈ unop U then CategoryStruct.comp (Y := 𝓕.stalk p₀) (𝓕.germ (unop U) p₀ h) (fromStalk 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₀ ∈ unop U then c else terminal.{u, v} C) ⋯)
        (𝓕.obj U)) =
    f.app U
⊢ NatTrans.app (toSkyscraperPresheaf p₀ (fromStalk p₀ f)) U = f.app 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
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U : (Opens (↑X : Type u))ᵒᵖ
pos :
  ∀ (h : p₀ ∈ unop U),
    CategoryStruct.comp (Y := 𝓕.stalk p₀) (𝓕.germ (unop U) p₀ h) (fromStalk p₀ f ≫ eqToHom ⋯) = f.app U
neg :
  ∀ (h : p₀ ∉ unop U),
    IsTerminal.from
        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
          (if p₀ ∈ unop U then c else terminal.{u, v} C) ⋯)
        (𝓕.obj U) =
      f.app U
⊢ (if h : p₀ ∈ unop U then CategoryStruct.comp (Y := 𝓕.stalk p₀) (𝓕.germ (unop U) p₀ h) (fromStalk 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₀ ∈ unop U then c else terminal.{u, v} C) ⋯)
        (𝓕.obj U)) =
    f.app U

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
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U : (Opens (↑X : Type u))ᵒᵖ
h : p₀ ∈ unop U
⊢ CategoryStruct.comp (Y := 𝓕.stalk p₀) (𝓕.germ (unop U) p₀ h) (fromStalk p₀ f ≫ eqToHom ⋯) = f.app U

Tactic:
simp
-- 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
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U : (Opens (↑X : Type u))ᵒᵖ
h : p₀ ∉ unop U
⊢ IsTerminal.from
      (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
        (if p₀ ∈ unop U then c else terminal.{u, v} C) ⋯)
      (𝓕.obj U) =
    f.app U

Tactic:
((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
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U : (Opens (↑X : Type u))ᵒᵖ
h : p₀ ∉ unop U
⊢ IsTerminal.from
      (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
        (if p₀ ∈ unop U then c else terminal.{u, v} C) ⋯)
      (𝓕.obj U) =
    f.app U

Tactic:
exact ((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
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
𝓕 : Presheaf C X
c : C
f : 𝓕.stalk p₀ ⟶ c
⊢ fromStalk p₀ (toSkyscraperPresheaf p₀ f) = f

Tactic:
𝓕.stalk_hom_ext fun U hxU ↦ ?_

Premises used: TopCat.Presheaf.stalk_hom_ext
-- 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
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
𝓕 : Presheaf C X
c : C
f : 𝓕.stalk p₀ ⟶ c
refine :
  ∀ (U : Opens (↑X : Type u)) (hxU : p₀ ∈ U),
    CategoryStruct.comp (Y := 𝓕.stalk p₀) (𝓕.germ U p₀ hxU) (fromStalk p₀ (toSkyscraperPresheaf p₀ f)) =
      𝓕.germ U p₀ hxU ≫ f
⊢ fromStalk p₀ (toSkyscraperPresheaf p₀ f) = f

Tactic:
refine 𝓕.stalk_hom_ext fun U hxU ↦ ?_

Premises used: TopCat.Presheaf.stalk_hom_ext
-- 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
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
𝓕 : Presheaf C X
c : C
f : 𝓕.stalk p₀ ⟶ c
U : Opens (↑X : Type u)
hxU : p₀ ∈ U
rw :
  CategoryStruct.comp (Y := Functor.obj (skyscraperPresheaf p₀ c) (op U))
      (NatTrans.app (toSkyscraperPresheaf p₀ f) (op U)) (eqToHom ⋯) =
    𝓕.germ U p₀ hxU ≫ f
rw₁ :
  CategoryStruct.comp (Y := Functor.obj (skyscraperPresheaf p₀ c) (op U))
      (if h : p₀ ∈ unop (op U) then 𝓕.germ (unop (op U)) p₀ h ≫ f ≫ eqToHom ⋯
      else IsTerminal.from (Eq.ndrec (motive := IsTerminal.{u, v}) terminalIsTerminal ⋯) (𝓕.obj (op U)))
      (eqToHom ⋯) =
    𝓕.germ U p₀ hxU ≫ f
rw₂ :
  CategoryStruct.comp (Y := Functor.obj (skyscraperPresheaf p₀ c) (op U)) (𝓕.germ (unop (op U)) p₀ hxU ≫ f ≫ eqToHom ⋯)
      (eqToHom ⋯) =
    𝓕.germ U p₀ hxU ≫ f
rw₃ :
  𝓕.germ (unop (op U)) p₀ hxU ≫
      CategoryStruct.comp (Y := Functor.obj (skyscraperPresheaf p₀ c) (op U)) (f ≫ eqToHom ⋯) (eqToHom ⋯) =
    𝓕.germ U p₀ hxU ≫ f
rw₄ :
  𝓕.germ (unop (op U)) p₀ hxU ≫
      f ≫ CategoryStruct.comp (Y := Functor.obj (skyscraperPresheaf p₀ c) (op U)) (eqToHom ⋯) (eqToHom ⋯) =
    𝓕.germ U p₀ hxU ≫ f
rw₅ : 𝓕.germ (unop (op U)) p₀ hxU ≫ f ≫ eqToHom ⋯ = 𝓕.germ U p₀ hxU ≫ f
rw₆ : 𝓕.germ (unop (op U)) p₀ hxU ≫ f ≫ 𝟙 c = 𝓕.germ U p₀ hxU ≫ f
rw₇ : 𝓕.germ (unop (op U)) p₀ hxU ≫ f = 𝓕.germ U p₀ hxU ≫ f
rw₈ rw₉ :
  Eq (α := 𝓕.obj (op U) ⟶ c)
    (colimit.ι ((OpenNhds.inclusion p₀).op ⋙ 𝓕)
          (op (Subtype.mk (p := fun (U : Opens (↑X : Type u)) ↦ p₀ ∈ U) (unop (op U)) hxU)) ≫
        f :
      𝓕.obj (op U) ⟶ c)
    (colimit.ι ((OpenNhds.inclusion p₀).op ⋙ 𝓕)
          (op (Subtype.mk (p := fun (U : Opens (↑X : Type u)) ↦ p₀ ∈ U) (unop (op U)) hxU)) ≫
        f :
      𝓕.obj (op U) ⟶ c)
⊢ CategoryStruct.comp (Y := 𝓕.stalk p₀) (𝓕.germ U p₀ hxU) (fromStalk p₀ (toSkyscraperPresheaf p₀ f)) =
    𝓕.germ U p₀ hxU ≫ f

Tactic:
rw [germ_fromStalk, toSkyscraperPresheaf_app, dif_pos hxU, Category.assoc, Category.assoc,
    eqToHom_trans, eqToHom_refl, Category.comp_id, Presheaf.germ]

Premises used: CategoryTheory.Category.assoc, StalkSkyscraperPresheafAdjunctionAuxs.germ_fromStalk, dif_pos, CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, TopCat.Presheaf.germ, CategoryTheory.eqToHom_trans, StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf_app