awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Skyscraper (goal)
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 ⋯))
⊢ 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)))
have 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) sorry)
        (𝓖.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) sorry)
        (𝓕.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) sorry)
        (if p₀ ∈ U then 𝓕.stalk p₀ else terminal.{u, v} C))
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Skyscraper (goal)
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
⊢ 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)
have 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 sorry
              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) sorry)
                  (X.obj U),
            naturality := sorry }) :
      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)) sorry) :
      Presheaf.stalk (skyscraperPresheaf p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X))) p₀ ⟶
        colimit ((OpenNhds.inclusion p₀).op ⋙ X)) =
  𝟙 (colimit ((OpenNhds.inclusion p₀).op ⋙ X))
Tactic: dsimp [Presheaf.stalkFunctor, toSkyscraperPresheaf]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Skyscraper (goal)
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
⊢ 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))
have 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 sorry
                  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) sorry)
                      (X.obj U),
                naturality := sorry : 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)) sorry) :
          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))
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Skyscraper (goal)
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₀)ᵒᵖ
⊢ CategoryStruct.comp (Y :=
      if p₀ ∈ (OpenNhds.inclusion p₀).obj (unop j) then colimit ((OpenNhds.inclusion p₀).op ⋙ X) else terminal.{u, v} C)
      (if h : p₀ ∈ (OpenNhds.inclusion p₀).obj (unop j) then
        X.germ ((OpenNhds.inclusion p₀).obj (unop j)) p₀ ⋯ ≫ 𝟙 (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₀ ∈ (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
have pos : ∀ (h : p₀ ∈ (OpenNhds.inclusion p₀).obj (unop 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₀ sorry ≫ 𝟙 (X.stalk p₀) ≫ eqToHom sorry)
      (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)) sorry) :
          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: split_ifs with h
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Skyscraper (goal)
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)
⊢ 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
have 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₀ sorry : X.obj (op ((OpenNhds.inclusion p₀).obj (unop j))) ⟶ X.stalk p₀)
  (colimit.ι ((OpenNhds.inclusion p₀).op ⋙ X) j)
Tactic: simp [skyscraperPresheafStalkOfSpecializes]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Skyscraper (goal)
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)
⊢ 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
have 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)
        sorry)
      (X.obj (op ((OpenNhds.inclusion p₀).obj (unop j)))))
    (eqToHom sorry) =
  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]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Skyscraper (goal)
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)
⊢ 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
have 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)
      sorry)
    (X.obj (op ((OpenNhds.inclusion p₀).obj (unop j)))))
  (colimit.ι ((OpenNhds.inclusion p₀).op ⋙ X) j ≫ eqToHom sorry)
Tactic: rw [comp_eqToHom_iff]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Skyscraper (goal)
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 : C
⊢ Eq (α :=
    Quiver.Hom (V := Presheaf C X) (Functor.obj (skyscraperPresheafFunctor p₀) Y)
      (Functor.obj (skyscraperPresheafFunctor p₀) Y))
    (CategoryStruct.comp (Y :=
      Functor.obj (skyscraperPresheafFunctor p₀)
        (Functor.obj (C := Presheaf C X) (Presheaf.stalkFunctor C p₀) (Functor.obj (skyscraperPresheafFunctor p₀) Y)))
      (NatTrans.app (StalkSkyscraperPresheafAdjunctionAuxs.unit p₀) (Functor.obj (skyscraperPresheafFunctor p₀) Y))
      (CategoryTheory.Functor.map (skyscraperPresheafFunctor p₀)
        (NatTrans.app (StalkSkyscraperPresheafAdjunctionAuxs.counit p₀) Y)))
    (𝟙 (Functor.obj (skyscraperPresheafFunctor p₀) Y))
have w : ∀ (U : Opens (↑X : Type u)),
  Eq (α :=
    Functor.obj (Functor.obj (skyscraperPresheafFunctor p₀) Y) (op U) ⟶
      Functor.obj (Functor.obj (skyscraperPresheafFunctor p₀) Y) (op U))
    (NatTrans.app
      (CategoryStruct.comp (Y :=
        Functor.obj (skyscraperPresheafFunctor p₀)
          (Functor.obj (C := Presheaf C X) (Presheaf.stalkFunctor C p₀) (Functor.obj (skyscraperPresheafFunctor p₀) Y)))
        (NatTrans.app (StalkSkyscraperPresheafAdjunctionAuxs.unit p₀) (Functor.obj (skyscraperPresheafFunctor p₀) Y))
        (CategoryTheory.Functor.map (skyscraperPresheafFunctor p₀)
          (NatTrans.app (StalkSkyscraperPresheafAdjunctionAuxs.counit p₀) Y)))
      (op U))
    (NatTrans.app (𝟙 (Functor.obj (skyscraperPresheafFunctor p₀) Y)) (op U))
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Skyscraper (goal)
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 : C
U : Opens (↑X : Type u)
⊢ Eq (α :=
    Functor.obj (Functor.obj (skyscraperPresheafFunctor p₀) Y) (op U) ⟶
      Functor.obj (Functor.obj (skyscraperPresheafFunctor p₀) Y) (op U))
    (NatTrans.app
      (CategoryStruct.comp (Y :=
        Functor.obj (skyscraperPresheafFunctor p₀)
          (Functor.obj (C := Presheaf C X) (Presheaf.stalkFunctor C p₀) (Functor.obj (skyscraperPresheafFunctor p₀) Y)))
        (NatTrans.app (StalkSkyscraperPresheafAdjunctionAuxs.unit p₀) (Functor.obj (skyscraperPresheafFunctor p₀) Y))
        (CategoryTheory.Functor.map (skyscraperPresheafFunctor p₀)
          (NatTrans.app (StalkSkyscraperPresheafAdjunctionAuxs.counit p₀) Y)))
      (op U))
    (NatTrans.app (𝟙 (Functor.obj (skyscraperPresheafFunctor p₀) Y)) (op U))
have w : Eq (α := (if p₀ ∈ U then Y else terminal.{u, v} C) ⟶ if p₀ ∈ U then Y else terminal.{u, v} C)
  (CategoryStruct.comp (Y := if p₀ ∈ U then Presheaf.stalk (skyscraperPresheaf p₀ Y) p₀ else terminal.{u, v} C)
      (if h : p₀ ∈ U then Presheaf.germ (skyscraperPresheaf p₀ Y) U p₀ sorry ≫ eqToHom sorry
      else
        IsTerminal.from
          (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
            (if p₀ ∈ U then Presheaf.stalk (skyscraperPresheaf p₀ Y) p₀ else terminal.{u, v} C) sorry)
          (if p₀ ∈ U then Y else terminal.{u, v} C))
      (if h : p₀ ∈ U then
        eqToHom sorry ≫
          CategoryStruct.comp (Y := Y)
            (Iso.hom
                (colimit.isoColimitCocone
                  { cocone := skyscraperPresheafCoconeOfSpecializes p₀ Y sorry,
                    isColimit := skyscraperPresheafCoconeIsColimitOfSpecializes p₀ Y sorry }) :
              Presheaf.stalk (skyscraperPresheaf p₀ Y) p₀ ⟶ Y)
            (eqToHom sorry)
      else
        IsTerminal.from
          (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
            (if p₀ ∈ U then Y else terminal.{u, v} C) sorry)
          (if p₀ ∈ U then Presheaf.stalk (skyscraperPresheaf p₀ Y) p₀ else terminal.{u, v} C)) :
    (if p₀ ∈ U then Y else terminal.{u, v} C) ⟶ if p₀ ∈ U then Y else terminal.{u, v} C)
  (NatTrans.app (𝟙 (skyscraperPresheaf p₀ Y)) (op U) :
    Functor.obj (skyscraperPresheaf p₀ Y) (op U) ⟶ Functor.obj (skyscraperPresheaf p₀ Y) (op U))
Tactic: simp only [skyscraperPresheafFunctor_obj, Functor.id_obj, skyscraperPresheaf_obj,
      Presheaf.stalkFunctor_obj, unit_app, counit_app,
      skyscraperPresheafStalkOfSpecializes, skyscraperPresheafFunctor_map, Presheaf.comp_app,
      toSkyscraperPresheaf_app, Category.id_comp, SkyscraperPresheafFunctor.map'_app]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Skyscraper (goal)
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 : C
U : Opens (↑X : Type u)
⊢ Eq (α := (if p₀ ∈ U then Y else terminal.{u, v} C) ⟶ if p₀ ∈ U then Y else terminal.{u, v} C)
    (CategoryStruct.comp (Y := if p₀ ∈ U then Presheaf.stalk (skyscraperPresheaf p₀ Y) p₀ else terminal.{u, v} C)
        (if h : p₀ ∈ U then Presheaf.germ (skyscraperPresheaf p₀ Y) U 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 Presheaf.stalk (skyscraperPresheaf p₀ Y) p₀ else terminal.{u, v} C) ⋯)
            (if p₀ ∈ U then Y else terminal.{u, v} C))
        (if h : p₀ ∈ U then
          eqToHom ⋯ ≫
            CategoryStruct.comp (Y := Y)
              (Iso.hom
                  (colimit.isoColimitCocone
                    { cocone := skyscraperPresheafCoconeOfSpecializes p₀ Y ⋯,
                      isColimit := skyscraperPresheafCoconeIsColimitOfSpecializes p₀ Y ⋯ }) :
                Presheaf.stalk (skyscraperPresheaf p₀ Y) p₀ ⟶ Y)
              (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 Y else terminal.{u, v} C) ⋯)
            (if p₀ ∈ U then Presheaf.stalk (skyscraperPresheaf p₀ Y) p₀ else terminal.{u, v} C)) :
      (if p₀ ∈ U then Y else terminal.{u, v} C) ⟶ if p₀ ∈ U then Y else terminal.{u, v} C)
    (NatTrans.app (𝟙 (skyscraperPresheaf p₀ Y)) (op U) :
      Functor.obj (skyscraperPresheaf p₀ Y) (op U) ⟶ Functor.obj (skyscraperPresheaf p₀ Y) (op U))
have pos : ∀ (h : p₀ ∈ U),
  Eq (α := (if p₀ ∈ U then Y else terminal.{u, v} C) ⟶ if p₀ ∈ U then Y else terminal.{u, v} C)
    (CategoryStruct.comp (Y := if p₀ ∈ U then Presheaf.stalk (skyscraperPresheaf p₀ Y) p₀ else terminal.{u, v} C)
        (Presheaf.germ (skyscraperPresheaf p₀ Y) U p₀ sorry ≫ eqToHom sorry)
        (eqToHom sorry ≫
          CategoryStruct.comp (Y := Y)
            (Iso.hom
                (colimit.isoColimitCocone
                  { cocone := skyscraperPresheafCoconeOfSpecializes p₀ Y sorry,
                    isColimit := skyscraperPresheafCoconeIsColimitOfSpecializes p₀ Y sorry }) :
              Presheaf.stalk (skyscraperPresheaf p₀ Y) p₀ ⟶ Y)
            (eqToHom sorry)) :
      (if p₀ ∈ U then Y else terminal.{u, v} C) ⟶ if p₀ ∈ U then Y else terminal.{u, v} C)
    (NatTrans.app (𝟙 (skyscraperPresheaf p₀ Y)) (op U) :
      Functor.obj (skyscraperPresheaf p₀ Y) (op U) ⟶ Functor.obj (skyscraperPresheaf p₀ Y) (op U))
Tactic: split_ifs with h