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.{w, v} C
inst_2 : HasTerminal.{w, v} C
a : C
U : Opens (↑X : Type u)
pos :
  ∀ (h : p₀ ∈ U),
    Eq.{w + 1} (α :=
      Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) (op U) ⟶
        Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) (op U))
      (eqToHom ⋯ ≫ 𝟙 a ≫ eqToHom ⋯) (NatTrans.app (𝟙 (skyscraperPresheaf p₀ a)) (op U))
⊢ Eq.{w + 1} (α :=
    Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) (op U) ⟶
      Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) (op U))
    (if h : p₀ ∈ U then eqToHom ⋯ ≫ 𝟙 a ≫ eqToHom ⋯
    else
      IsTerminal.from
        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{w, v} C = x) ↦ IsTerminal.{w, v} x) terminalIsTerminal
          (if p₀ ∈ U then a else terminal.{w, v} C) ⋯)
        (Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) (op U)))
    (NatTrans.app (𝟙 (skyscraperPresheaf p₀ a)) (op U))
have neg : ∀ (h : p₀ ∉ U),
  IsTerminal.from
      (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{w, v} C = x) ↦ IsTerminal.{w, v} x) terminalIsTerminal
        (if p₀ ∈ U then a else terminal.{w, v} C) sorry)
      (Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) (op U)) =
    NatTrans.app (𝟙 (skyscraperPresheaf p₀ a)) (op U)
Tactic: split_ifs
-- 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.{w, v} C
inst_2 : HasTerminal.{w, v} C
a b c : C
f : a ⟶ b
g : b ⟶ c
⊢ Eq (α := Quiver.Hom (V := Presheaf.{u, w, v} C X) (skyscraperPresheaf p₀ a) (skyscraperPresheaf p₀ c))
    (map' p₀ (f ≫ g)) (map' p₀ f ≫ map' p₀ g)
have w : ∀ (U : Opens (↑X : Type u)),
  Eq (α :=
    Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) (op U) ⟶
      Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ c) (op U))
    (NatTrans.app (map' p₀ (f ≫ g)) (op U)) (NatTrans.app (map' p₀ f ≫ map' p₀ g) (op U))
Tactic: ext U
-- 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.{w, v} C
inst_2 : HasTerminal.{w, v} C
a b c : C
f : a ⟶ b
g : b ⟶ c
U : Opens (↑X : Type u)
⊢ Eq (α :=
    Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) (op U) ⟶
      Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ c) (op U))
    (NatTrans.app (map' p₀ (f ≫ g)) (op U)) (NatTrans.app (map' p₀ f ≫ map' p₀ g) (op U))
have w : Eq (α :=
  Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) (op U) ⟶ Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ c) (op U))
  (if h : p₀ ∈ U then eqToHom sorry ≫ (f ≫ g) ≫ eqToHom sorry
  else
    IsTerminal.from
      (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{w, v} C = x) ↦ IsTerminal.{w, v} x) terminalIsTerminal
        (if p₀ ∈ U then c else terminal.{w, v} C) sorry)
      (Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) (op U)))
  (NatTrans.app (map' p₀ f ≫ map' p₀ g) (op U))
Tactic: simp only [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.{w, v} C
inst_2 : HasTerminal.{w, v} C
a b c : C
f : a ⟶ b
g : b ⟶ c
U : Opens (↑X : Type u)
⊢ Eq (α :=
    Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) (op U) ⟶
      Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ c) (op U))
    (if h : p₀ ∈ U then eqToHom ⋯ ≫ (f ≫ g) ≫ eqToHom ⋯
    else
      IsTerminal.from
        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{w, v} C = x) ↦ IsTerminal.{w, v} x) terminalIsTerminal
          (if p₀ ∈ U then c else terminal.{w, v} C) ⋯)
        (Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) (op U)))
    (NatTrans.app (map' p₀ f ≫ map' p₀ g) (op U))
have pos : ∀ (h : p₀ ∈ U),
  Eq (α :=
    Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) (op U) ⟶
      Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ c) (op U))
    (eqToHom sorry ≫ (f ≫ g) ≫ eqToHom sorry) (NatTrans.app (map' p₀ f ≫ map' p₀ g) (op U))
Tactic: split_ifs with h
-- 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.{w, v} C
inst_2 : HasTerminal.{w, v} C
a b c : C
f : a ⟶ b
g : b ⟶ c
U : Opens (↑X : Type u)
pos :
  ∀ (h : p₀ ∈ U),
    Eq (α :=
      Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) (op U) ⟶
        Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ c) (op U))
      (eqToHom ⋯ ≫ (f ≫ g) ≫ eqToHom ⋯) (NatTrans.app (map' p₀ f ≫ map' p₀ g) (op U))
⊢ Eq (α :=
    Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) (op U) ⟶
      Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ c) (op U))
    (if h : p₀ ∈ U then eqToHom ⋯ ≫ (f ≫ g) ≫ eqToHom ⋯
    else
      IsTerminal.from
        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{w, v} C = x) ↦ IsTerminal.{w, v} x) terminalIsTerminal
          (if p₀ ∈ U then c else terminal.{w, v} C) ⋯)
        (Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) (op U)))
    (NatTrans.app (map' p₀ f ≫ map' p₀ g) (op U))
have neg : ∀ (h : p₀ ∉ U),
  IsTerminal.from
      (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{w, v} C = x) ↦ IsTerminal.{w, v} x) terminalIsTerminal
        (if p₀ ∈ U then c else terminal.{w, v} C) sorry)
      (Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) (op U)) =
    NatTrans.app (map' p₀ f ≫ map' p₀ g) (op U)
Tactic: split_ifs with h
-- 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
y : (↑X : Type u)
h : p₀ ⤳ y
U V : (OpenNhds y)ᵒᵖ
inc : U ⟶ V
⊢ Eq (α :=
    Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) U ⟶
      Functor.obj (Functor.obj (Functor.const (OpenNhds y)ᵒᵖ) A) V)
    (CategoryTheory.Functor.map ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) inc ≫ eqToHom ⋯)
    (eqToHom ⋯ ≫ CategoryTheory.Functor.map (Functor.obj (Functor.const (OpenNhds y)ᵒᵖ) A) inc)
have change : Eq (α :=
  Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) U ⟶
    Functor.obj (Functor.obj (Functor.const (OpenNhds y)ᵒᵖ) A) V)
  (CategoryStruct.comp (Y := Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) V)
      (if h : p₀ ∈ unop ((OpenNhds.inclusion y).op.obj V) then eqToHom sorry
      else
        IsTerminal.from (Eq.ndrec (motive := IsTerminal.{u, v}) terminalIsTerminal sorry)
          (if p₀ ∈ unop ((OpenNhds.inclusion y).op.obj U) then A else terminal.{u, v} C))
      (eqToHom sorry) :
    Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) U ⟶
      Functor.obj (Functor.obj (Functor.const (OpenNhds y)ᵒᵖ) A) V)
  (eqToHom sorry ≫ CategoryTheory.Functor.map (Functor.obj (Functor.const (OpenNhds y)ᵒᵖ) A) inc :
    Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) U ⟶
      Functor.obj (Functor.obj (Functor.const (OpenNhds y)ᵒᵖ) A) V)
Tactic: change dite _ _ _ ≫ _ = _
-- 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
y : (↑X : Type u)
h : p₀ ⤳ y
U V : (OpenNhds y)ᵒᵖ
inc : U ⟶ V
⊢ Eq (α :=
    Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) U ⟶
      Functor.obj (Functor.obj (Functor.const (OpenNhds y)ᵒᵖ) A) V)
    (CategoryStruct.comp (Y := Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) V)
        (if h : p₀ ∈ unop ((OpenNhds.inclusion y).op.obj V) then eqToHom ⋯
        else
          IsTerminal.from (Eq.ndrec (motive := IsTerminal.{u, v}) terminalIsTerminal ⋯)
            (if p₀ ∈ unop ((OpenNhds.inclusion y).op.obj U) then A else terminal.{u, v} C))
        (eqToHom ⋯) :
      Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) U ⟶
        Functor.obj (Functor.obj (Functor.const (OpenNhds y)ᵒᵖ) A) V)
    (eqToHom ⋯ ≫ CategoryTheory.Functor.map (Functor.obj (Functor.const (OpenNhds y)ᵒᵖ) A) inc :
      Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) U ⟶
        Functor.obj (Functor.obj (Functor.const (OpenNhds y)ᵒᵖ) A) V)
have rw : Eq.{u + 1} (α :=
  Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) U ⟶
    Functor.obj (Functor.obj (Functor.const (OpenNhds y)ᵒᵖ) A) V)
  (eqToHom sorry ≫ eqToHom sorry) (eqToHom sorry ≫ CategoryTheory.Functor.map (Functor.obj (Functor.const (OpenNhds y)ᵒᵖ) A) inc)
Tactic: rw [dif_pos]
-- 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
y : (↑X : Type u)
h : p₀ ⤳ y
U V : (OpenNhds y)ᵒᵖ
inc : U ⟶ V
rw :
  Eq.{u + 1} (α :=
    Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) U ⟶
      Functor.obj (Functor.obj (Functor.const (OpenNhds y)ᵒᵖ) A) V)
    (eqToHom ⋯ ≫ eqToHom ⋯) (eqToHom ⋯ ≫ CategoryTheory.Functor.map (Functor.obj (Functor.const (OpenNhds y)ᵒᵖ) A) inc)
⊢ Eq (α :=
    Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) U ⟶
      Functor.obj (Functor.obj (Functor.const (OpenNhds y)ᵒᵖ) A) V)
    (CategoryStruct.comp (Y := Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) V)
        (if h : p₀ ∈ unop ((OpenNhds.inclusion y).op.obj V) then eqToHom ⋯
        else
          IsTerminal.from (Eq.ndrec (motive := IsTerminal.{u, v}) terminalIsTerminal ⋯)
            (if p₀ ∈ unop ((OpenNhds.inclusion y).op.obj U) then A else terminal.{u, v} C))
        (eqToHom ⋯) :
      Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) U ⟶
        Functor.obj (Functor.obj (Functor.const (OpenNhds y)ᵒᵖ) A) V)
    (eqToHom ⋯ ≫ CategoryTheory.Functor.map (Functor.obj (Functor.const (OpenNhds y)ᵒᵖ) A) inc :
      Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) U ⟶
        Functor.obj (Functor.obj (Functor.const (OpenNhds y)ᵒᵖ) A) V)
have hc : p₀ ∈ unop ((OpenNhds.inclusion y).op.obj V)
Tactic: rw [dif_pos]
-- 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
y : (↑X : Type u)
h : p₀ ⤳ y
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
U : (OpenNhds y)ᵒᵖ
⊢ CategoryStruct.comp (Y :=
      Functor.obj
        (Functor.obj (Functor.const (OpenNhds y)ᵒᵖ)
          (Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
            (skyscraperPresheafCoconeOfSpecializes p₀ A h)))
        U)
      (NatTrans.app (Cocone.ι (skyscraperPresheafCoconeOfSpecializes p₀ A h)) U)
      (CategoryStruct.comp (Y :=
        if True then
          Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
            (skyscraperPresheafCoconeOfSpecializes p₀ A h)
        else terminal.{u, v} C)
        (eqToHom ⋯) (c.ι.app (op ⊤))) =
    c.ι.app U
have dsimp : eqToHom sorry ≫ CategoryStruct.comp (Y := if True then A else terminal.{u, v} C) (eqToHom sorry) (c.ι.app (op ⊤)) = c.ι.app U
Tactic: dsimp
-- 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
y : (↑X : Type u)
h : p₀ ⤳ y
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
U : (OpenNhds y)ᵒᵖ
⊢ eqToHom ⋯ ≫ CategoryStruct.comp (Y := if True then A else terminal.{u, v} C) (eqToHom ⋯) (c.ι.app (op ⊤)) = c.ι.app U
have rw : eqToHom sorry ≫
    eqToHom sorry ≫
      CategoryStruct.comp (Y := Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (op (unop U)))
        (CategoryTheory.Functor.map ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (Quiver.Hom.op (homOfLE sorry)))
        (c.ι.app (op (unop U))) =
  c.ι.app U
Tactic: rw [← c.w (homOfLE <| (le_top : unop U ≤ _)).op]
-- 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
y : (↑X : Type u)
h : p₀ ⤳ y
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
U : (OpenNhds y)ᵒᵖ
⊢ eqToHom ⋯ ≫
      eqToHom ⋯ ≫
        CategoryStruct.comp (Y := Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (op (unop U)))
          (CategoryTheory.Functor.map ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (Quiver.Hom.op (homOfLE ⋯)))
          (c.ι.app (op (unop U))) =
    c.ι.app U
have change : eqToHom sorry ≫
    CategoryStruct.comp (Y := if True then A else terminal.{u, v} C) (eqToHom sorry)
      (CategoryStruct.comp (Y := Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (op (unop U)))
        (if h : p₀ ∈ unop ((OpenNhds.inclusion y).op.obj (op (unop U))) then eqToHom sorry
        else
          IsTerminal.from (Eq.ndrec (motive := IsTerminal.{u, v}) terminalIsTerminal sorry)
            (if p₀ ∈ unop ((OpenNhds.inclusion y).op.obj (op ⊤)) then A else terminal.{u, v} C))
        (c.ι.app (op (unop U)))) =
  c.ι.app U
Tactic: change _ ≫ _ ≫ dite _ _ _ ≫ _ = _
-- 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
y : (↑X : Type u)
h : p₀ ⤳ y
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
U : (OpenNhds y)ᵒᵖ
⊢ eqToHom ⋯ ≫
      CategoryStruct.comp (Y := if True then A else terminal.{u, v} C) (eqToHom ⋯)
        (CategoryStruct.comp (Y := Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (op (unop U)))
          (if h : p₀ ∈ unop ((OpenNhds.inclusion y).op.obj (op (unop U))) then eqToHom ⋯
          else
            IsTerminal.from (Eq.ndrec (motive := IsTerminal.{u, v}) terminalIsTerminal ⋯)
              (if p₀ ∈ unop ((OpenNhds.inclusion y).op.obj (op ⊤)) then A else terminal.{u, v} C))
          (c.ι.app (op (unop U)))) =
    c.ι.app U
have rw : eqToHom sorry ≫ eqToHom sorry ≫ eqToHom sorry ≫ c.ι.app (op (unop U)) = c.ι.app U
Tactic: rw [dif_pos]
-- 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
y : (↑X : Type u)
h : p₀ ⤳ y
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
U : (OpenNhds y)ᵒᵖ
rw : eqToHom ⋯ ≫ eqToHom ⋯ ≫ eqToHom ⋯ ≫ c.ι.app (op (unop U)) = c.ι.app U
⊢ eqToHom ⋯ ≫
      CategoryStruct.comp (Y := if True then A else terminal.{u, v} C) (eqToHom ⋯)
        (CategoryStruct.comp (Y := Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (op (unop U)))
          (if h : p₀ ∈ unop ((OpenNhds.inclusion y).op.obj (op (unop U))) then eqToHom ⋯
          else
            IsTerminal.from (Eq.ndrec (motive := IsTerminal.{u, v}) terminalIsTerminal ⋯)
              (if p₀ ∈ unop ((OpenNhds.inclusion y).op.obj (op ⊤)) then A else terminal.{u, v} C))
          (c.ι.app (op (unop U)))) =
    c.ι.app U
have hc : p₀ ∈ unop ((OpenNhds.inclusion y).op.obj (op (unop U)))
Tactic: rw [dif_pos]
-- 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
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
⊢ f = CategoryStruct.comp (Y := if True then A else terminal.{u, v} C) (eqToHom ⋯) (c.ι.app (op ⊤))
have rw : f =
  CategoryStruct.comp (Y := if True then A else terminal.{u, v} C) (eqToHom sorry)
    (NatTrans.app (Cocone.ι (skyscraperPresheafCoconeOfSpecializes p₀ A h_1)) (op ⊤) ≫ f)
Tactic: rw [← h, skyscraperPresheafCoconeOfSpecializes_ι_app, eqToHom_trans_assoc, eqToHom_refl,
      Category.id_comp]
-- 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
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)
⊢ f = CategoryStruct.comp (Y := if True then A else terminal.{u, v} C) (eqToHom ⋯) (c.ι.app (op ⊤))
have rw₁ : f = CategoryStruct.comp (Y := if True then A else terminal.{u, v} C) (eqToHom sorry) (eqToHom sorry ≫ f)
Tactic: rw [← h, skyscraperPresheafCoconeOfSpecializes_ι_app, eqToHom_trans_assoc, eqToHom_refl,
      Category.id_comp]
-- 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
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)
⊢ f = CategoryStruct.comp (Y := if True then A else terminal.{u, v} C) (eqToHom ⋯) (c.ι.app (op ⊤))
have rw₂ : f = eqToHom sorry ≫ f
Tactic: rw [← h, skyscraperPresheafCoconeOfSpecializes_ι_app, eqToHom_trans_assoc, eqToHom_refl,
      Category.id_comp]
-- 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
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
⊢ f = CategoryStruct.comp (Y := if True then A else terminal.{u, v} C) (eqToHom ⋯) (c.ι.app (op ⊤))
have rw₃ : f = 𝟙 A ≫ f
Tactic: rw [← h, skyscraperPresheafCoconeOfSpecializes_ι_app, eqToHom_trans_assoc, eqToHom_refl,
      Category.id_comp]
-- 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
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
⊢ f = CategoryStruct.comp (Y := if True then A else terminal.{u, v} C) (eqToHom ⋯) (c.ι.app (op ⊤))
have rw₄ : f = f
Tactic: rw [← h, skyscraperPresheafCoconeOfSpecializes_ι_app, eqToHom_trans_assoc, eqToHom_refl,
      Category.id_comp]
-- 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
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 ⋯)))
have 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)))
Tactic: refine ((if_neg ?_).symm.ndrec terminalIsTerminal).hom_ext _ _