awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Sheafify (goal)
Goal:
X : TopCat
F : Presheaf (Type v) X
x : (↑X : Type v)
U : Opens (↑X : Type v)
m : x ∈ U
s : ToType (FC := TypeCat.Fun) (F.obj (op U))
⊢ ∃ (f :
    (y : ↥(↑(Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) U m) : Opens (↑X : Type v))) →
      F.stalk (↑y : (↑X : Type v)))
    (_ :
    (Sheafify.isLocallyGerm F).toPrelocalPredicate (T := fun (x : (↑X : Type v)) ↦ F.stalk x).pred (T :=
      fun (x : (↑X : Type v)) ↦ F.stalk x) f),
    Eq.{v + 1} (α :=
      F.stalk
        (↑(Subtype.mk (p := fun (x_2 : (↑X : Type v)) ↦
              x_2 ∈ (↑(Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) U m) : Opens (↑X : Type v))) x ⋯) :
          (↑X : Type v)))
      (f
        (Subtype.mk (p := fun (x_2 : (↑X : Type v)) ↦
          x_2 ∈ (↑(Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) U m) : Opens (↑X : Type v))) x ⋯))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.germ U x m) : (a : F.obj (op U)) → F.stalk x) s)
have h : (y : ↥(↑(Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) U m) : Opens (↑X : Type v))) →
  F.stalk (↑y : (↑X : Type v))
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Sheafify (goal)
Goal:
X : TopCat
F : Presheaf (Type v) X
x : (↑X : Type v)
⊢ Function.Injective (α := (fun (X : Type v) ↦ X) (F.sheafify.presheaf.stalk x)) (β :=
    (fun (X : Type v) ↦ X) (F.stalk x))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.stalkToFiber x)) :
      (a : (fun (X : Type v) ↦ X) (F.sheafify.presheaf.stalk x)) → (fun (X : Type v) ↦ X) (F.stalk x))
have w : ∀ (U V : OpenNhds x) (fU : (y : ↥(↑U : Opens (↑X : Type v))) → F.stalk (↑y : (↑X : Type v))),
  (Sheafify.isLocallyGerm F).toPrelocalPredicate (T := fun (x : (↑X : Type v)) ↦ F.stalk x).pred (T :=
      fun (x : (↑X : Type v)) ↦ F.stalk x) fU →
    ∀ (fV : (y : ↥(↑V : Opens (↑X : Type v))) → F.stalk (↑y : (↑X : Type v))),
      (Sheafify.isLocallyGerm F).toPrelocalPredicate (T := fun (x : (↑X : Type v)) ↦ F.stalk x).pred (T :=
          fun (x : (↑X : Type v)) ↦ F.stalk x) fV →
        Eq.{v + 1} (α :=
            F.stalk
              (↑(Subtype.mk (p := fun (x_3 : (↑X : Type v)) ↦ x_3 ∈ (↑U : Opens (↑X : Type v))) x sorry) : (↑X : Type v)))
            (fU (Subtype.mk (p := fun (x_3 : (↑X : Type v)) ↦ x_3 ∈ (↑U : Opens (↑X : Type v))) x sorry))
            (fV (Subtype.mk (p := fun (x_3 : (↑X : Type v)) ↦ x_3 ∈ (↑V : Opens (↑X : Type v))) x sorry)) →
          ∃ (W : OpenNhds x) (iU : W ⟶ U) (iV : W ⟶ V),
            ∀ (w : ↥(↑W : Opens (↑X : Type v))),
              Eq.{v + 1} (α :=
                F.stalk (↑((iU : (a : ↥(↑W : Opens (↑X : Type v))) → ↥(↑U : Opens (↑X : Type v))) w) : (↑X : Type v)))
                (fU ((iU : (a : ↥(↑W : Opens (↑X : Type v))) → ↥(↑U : Opens (↑X : Type v))) w))
                (fV ((iV : (a : ↥(↑W : Opens (↑X : Type v))) → ↥(↑V : Opens (↑X : Type v))) w))
Tactic: apply TopCat.stalkToFiber_injective
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Sheafify (goal)
Goal:
X : TopCat
F : Presheaf (Type v) X
x : (↑X : Type v)
U V : OpenNhds x
fU : (y : ↥(↑U : Opens (↑X : Type v))) → F.stalk (↑y : (↑X : Type v))
hU :
  (Sheafify.isLocallyGerm F).toPrelocalPredicate (T := fun (x : (↑X : Type v)) ↦ F.stalk x).pred (T :=
    fun (x : (↑X : Type v)) ↦ F.stalk x) fU
fV : (y : ↥(↑V : Opens (↑X : Type v))) → F.stalk (↑y : (↑X : Type v))
hV :
  (Sheafify.isLocallyGerm F).toPrelocalPredicate (T := fun (x : (↑X : Type v)) ↦ F.stalk x).pred (T :=
    fun (x : (↑X : Type v)) ↦ F.stalk x) fV
e :
  Eq (α :=
    F.stalk (↑(Subtype.mk (p := fun (x_1 : (↑X : Type v)) ↦ x_1 ∈ (↑U : Opens (↑X : Type v))) x ⋯) : (↑X : Type v)))
    (fU (Subtype.mk (p := fun (x_1 : (↑X : Type v)) ↦ x_1 ∈ (↑U : Opens (↑X : Type v))) x ⋯))
    (fV (Subtype.mk (p := fun (x_1 : (↑X : Type v)) ↦ x_1 ∈ (↑V : Opens (↑X : Type v))) x ⋯))
⊢ ∃ (W : OpenNhds x) (iU : W ⟶ U) (iV : W ⟶ V),
    ∀ (w : ↥(↑W : Opens (↑X : Type v))),
      Eq (α := F.stalk (↑((iU : (a : ↥(↑W : Opens (↑X : Type v))) → ↥(↑U : Opens (↑X : Type v))) w) : (↑X : Type v)))
        (fU ((iU : (a : ↥(↑W : Opens (↑X : Type v))) → ↥(↑U : Opens (↑X : Type v))) w))
        (fV ((iV : (a : ↥(↑W : Opens (↑X : Type v))) → ↥(↑V : Opens (↑X : Type v))) w))
have w : ∀ (U' : Opens (↑X : Type v))
  (mU : (↑(Subtype.mk (p := fun (x_1 : (↑X : Type v)) ↦ x_1 ∈ (↑U : Opens (↑X : Type v))) x sorry) : (↑X : Type v)) ∈ U')
  (iU : U' ⟶ (↑U : Opens (↑X : Type v))) (gU : F.obj (op U'))
  (wU :
    ∀ (x_1 : ↥U'),
      Eq (α := F.stalk (↑x_1 : (↑X : Type v)))
        ((fun (x_2 : ↥U') ↦
              (fU ((iU : (a : ↥U') → ↥(↑U : Opens (↑X : Type v))) x_2) :
                ?T (↑((iU : (a : ↥U') → ↥(↑U : Opens (↑X : Type v))) x_2) : (↑?X : Type ?u.5027))))
            x_1 :
          F.stalk (↑((iU : (a : ↥U') → ↥(↑U : Opens (↑X : Type v))) x_1) : (↑X : Type ?u.5027)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.germ U' (↑x_1 : (↑X : Type v)) sorry) :
              (a : (fun (X : Type v) ↦ X) (F.obj (op U'))) → (fun (X : Type v) ↦ X) (F.stalk (↑x_1 : (↑X : Type v))))
            gU :
          (fun (X : Type v) ↦ X) (F.stalk (↑x_1 : (↑X : Type v))))),
  ∃ (W : OpenNhds x) (iU : W ⟶ U) (iV : W ⟶ V),
    ∀ (w : ↥(↑W : Opens (↑X : Type v))),
      Eq (α := F.stalk (↑((iU : (a : ↥(↑W : Opens (↑X : Type v))) → ↥(↑U : Opens (↑X : Type v))) w) : (↑X : Type v)))
        (fU ((iU : (a : ↥(↑W : Opens (↑X : Type v))) → ↥(↑U : Opens (↑X : Type v))) w))
        (fV ((iV : (a : ↥(↑W : Opens (↑X : Type v))) → ↥(↑V : Opens (↑X : Type v))) w))
Tactic: rcases hU ⟨x, U.2⟩ with ⟨U', mU, iU, gU, wU⟩
-- 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 V : (Opens (↑X : Type u))ᵒᵖ
i : U ⟶ V
h : p₀ ∈ unop V
⊢ (if p₀ ∈ unop U then A else terminal.{w, v} C) = if p₀ ∈ unop V then A else terminal.{w, v} C
have rw : (if p₀ ∈ unop U then A else terminal.{w, v} C) = A
Tactic: rw [if_pos h, if_pos (by simpa using i.unop.le 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 : C
U V : (Opens (↑X : Type u))ᵒᵖ
i : U ⟶ V
h : p₀ ∈ unop V
rw : (if p₀ ∈ unop U then A else terminal.{w, v} C) = A
⊢ (if p₀ ∈ unop U then A else terminal.{w, v} C) = if p₀ ∈ unop V then A else terminal.{w, v} C
have rw₁ : A = A
Tactic: rw [if_pos h, if_pos (by simpa using i.unop.le 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 : C
U V W : (Opens (↑X : Type u))ᵒᵖ
iVU : U ⟶ V
iWV : V ⟶ W
⊢ Eq.{w + 1} (α := (if p₀ ∈ unop U then A else terminal.{w, v} C) ⟶ if p₀ ∈ unop W then A else terminal.{w, v} C)
    (if h : p₀ ∈ unop W then eqToHom ⋯
    else
      IsTerminal.from (Eq.ndrec (motive := IsTerminal.{w, v}) terminalIsTerminal ⋯)
        (if p₀ ∈ unop U then A else terminal.{w, v} C))
    (CategoryStruct.comp (Y := if p₀ ∈ unop V then A else terminal.{w, v} C)
      (if h : p₀ ∈ unop V then eqToHom ⋯
      else
        IsTerminal.from (Eq.ndrec (motive := IsTerminal.{w, v}) terminalIsTerminal ⋯)
          (if p₀ ∈ unop U then A else terminal.{w, v} C))
      (if h : p₀ ∈ unop W then eqToHom ⋯
      else
        IsTerminal.from (Eq.ndrec (motive := IsTerminal.{w, v}) terminalIsTerminal ⋯)
          (if p₀ ∈ unop V then A else terminal.{w, v} C)))
have pos : ∀ (hW : p₀ ∈ unop W),
  Eq.{w + 1} (α := (if p₀ ∈ unop U then A else terminal.{w, v} C) ⟶ if p₀ ∈ unop W then A else terminal.{w, v} C)
    (if h : p₀ ∈ unop W then eqToHom sorry
    else
      IsTerminal.from (Eq.ndrec (motive := IsTerminal.{w, v}) terminalIsTerminal sorry)
        (if p₀ ∈ unop U then A else terminal.{w, v} C))
    (CategoryStruct.comp (Y := if p₀ ∈ unop V then A else terminal.{w, v} C)
      (if h : p₀ ∈ unop V then eqToHom sorry
      else
        IsTerminal.from (Eq.ndrec (motive := IsTerminal.{w, v}) terminalIsTerminal sorry)
          (if p₀ ∈ unop U then A else terminal.{w, v} C))
      (if h : p₀ ∈ unop W then eqToHom sorry
      else
        IsTerminal.from (Eq.ndrec (motive := IsTerminal.{w, v}) terminalIsTerminal sorry)
          (if p₀ ∈ unop V then A else terminal.{w, v} C)))
Tactic: by_cases hW : p₀ ∈ unop W
-- 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 V W : (Opens (↑X : Type u))ᵒᵖ
iVU : U ⟶ V
iWV : V ⟶ W
pos :
  ∀ (hW : p₀ ∈ unop W),
    Eq.{w + 1} (α := (if p₀ ∈ unop U then A else terminal.{w, v} C) ⟶ if p₀ ∈ unop W then A else terminal.{w, v} C)
      (if h : p₀ ∈ unop W then eqToHom ⋯
      else
        IsTerminal.from (Eq.ndrec (motive := IsTerminal.{w, v}) terminalIsTerminal ⋯)
          (if p₀ ∈ unop U then A else terminal.{w, v} C))
      (CategoryStruct.comp (Y := if p₀ ∈ unop V then A else terminal.{w, v} C)
        (if h : p₀ ∈ unop V then eqToHom ⋯
        else
          IsTerminal.from (Eq.ndrec (motive := IsTerminal.{w, v}) terminalIsTerminal ⋯)
            (if p₀ ∈ unop U then A else terminal.{w, v} C))
        (if h : p₀ ∈ unop W then eqToHom ⋯
        else
          IsTerminal.from (Eq.ndrec (motive := IsTerminal.{w, v}) terminalIsTerminal ⋯)
            (if p₀ ∈ unop V then A else terminal.{w, v} C)))
⊢ Eq.{w + 1} (α := (if p₀ ∈ unop U then A else terminal.{w, v} C) ⟶ if p₀ ∈ unop W then A else terminal.{w, v} C)
    (if h : p₀ ∈ unop W then eqToHom ⋯
    else
      IsTerminal.from (Eq.ndrec (motive := IsTerminal.{w, v}) terminalIsTerminal ⋯)
        (if p₀ ∈ unop U then A else terminal.{w, v} C))
    (CategoryStruct.comp (Y := if p₀ ∈ unop V then A else terminal.{w, v} C)
      (if h : p₀ ∈ unop V then eqToHom ⋯
      else
        IsTerminal.from (Eq.ndrec (motive := IsTerminal.{w, v}) terminalIsTerminal ⋯)
          (if p₀ ∈ unop U then A else terminal.{w, v} C))
      (if h : p₀ ∈ unop W then eqToHom ⋯
      else
        IsTerminal.from (Eq.ndrec (motive := IsTerminal.{w, v}) terminalIsTerminal ⋯)
          (if p₀ ∈ unop V then A else terminal.{w, v} C)))
have neg : ∀ (hW : p₀ ∉ unop W),
  Eq.{w + 1} (α := (if p₀ ∈ unop U then A else terminal.{w, v} C) ⟶ if p₀ ∈ unop W then A else terminal.{w, v} C)
    (if h : p₀ ∈ unop W then eqToHom sorry
    else
      IsTerminal.from (Eq.ndrec (motive := IsTerminal.{w, v}) terminalIsTerminal sorry)
        (if p₀ ∈ unop U then A else terminal.{w, v} C))
    (CategoryStruct.comp (Y := if p₀ ∈ unop V then A else terminal.{w, v} C)
      (if h : p₀ ∈ unop V then eqToHom sorry
      else
        IsTerminal.from (Eq.ndrec (motive := IsTerminal.{w, v}) terminalIsTerminal sorry)
          (if p₀ ∈ unop U then A else terminal.{w, v} C))
      (if h : p₀ ∈ unop W then eqToHom sorry
      else
        IsTerminal.from (Eq.ndrec (motive := IsTerminal.{w, v}) terminalIsTerminal sorry)
          (if p₀ ∈ unop V then A else terminal.{w, v} C)))
Tactic: by_cases hW : p₀ ∈ unop W
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Skyscraper (hypothesis)
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 V W : (Opens (↑X : Type u))ᵒᵖ
iVU : U ⟶ V
iWV : V ⟶ W
hW : p₀ ∈ unop W
⊢ Eq.{w + 1} (α := (if p₀ ∈ unop U then A else terminal.{w, v} C) ⟶ if p₀ ∈ unop W then A else terminal.{w, v} C)
    (if h : p₀ ∈ unop W then eqToHom ⋯
    else
      IsTerminal.from (Eq.ndrec (motive := IsTerminal.{w, v}) terminalIsTerminal ⋯)
        (if p₀ ∈ unop U then A else terminal.{w, v} C))
    (CategoryStruct.comp (Y := if p₀ ∈ unop V then A else terminal.{w, v} C)
      (if h : p₀ ∈ unop V then eqToHom ⋯
      else
        IsTerminal.from (Eq.ndrec (motive := IsTerminal.{w, v}) terminalIsTerminal ⋯)
          (if p₀ ∈ unop U then A else terminal.{w, v} C))
      (if h : p₀ ∈ unop W then eqToHom ⋯
      else
        IsTerminal.from (Eq.ndrec (motive := IsTerminal.{w, v}) terminalIsTerminal ⋯)
          (if p₀ ∈ unop V then A else terminal.{w, v} C)))
have hV : p₀ ∈ unop V
Tactic: have hV : p₀ ∈ unop V := leOfHom iWV.unop hW
-- 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 V W : (Opens (↑X : Type u))ᵒᵖ
iVU : U ⟶ V
iWV : V ⟶ W
hW : p₀ ∉ unop W
⊢ Eq.{w + 1} (α := (if p₀ ∈ unop U then A else terminal.{w, v} C) ⟶ if p₀ ∈ unop W then A else terminal.{w, v} C)
    (if h : p₀ ∈ unop W then eqToHom ⋯
    else
      IsTerminal.from
        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{w, v} C = x) ↦ IsTerminal.{w, v} x) terminalIsTerminal
          (if p₀ ∈ unop W then A else terminal.{w, v} C) ⋯)
        (if p₀ ∈ unop U then A else terminal.{w, v} C))
    (CategoryStruct.comp (Y := if p₀ ∈ unop V then A else terminal.{w, v} C)
      (if h : p₀ ∈ unop V then eqToHom ⋯
      else
        IsTerminal.from
          (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{w, v} C = x) ↦ IsTerminal.{w, v} x) terminalIsTerminal
            (if p₀ ∈ unop V then A else terminal.{w, v} C) ⋯)
          (if p₀ ∈ unop U then A else terminal.{w, v} C))
      (if h : p₀ ∈ unop W then eqToHom ⋯
      else
        IsTerminal.from
          (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{w, v} C = x) ↦ IsTerminal.{w, v} x) terminalIsTerminal
            (if p₀ ∈ unop W then A else terminal.{w, v} C) ⋯)
          (if p₀ ∈ unop V then A else terminal.{w, v} C)))
have neg : Eq.{w + 1} (α := (if p₀ ∈ unop U then A else terminal.{w, v} C) ⟶ if p₀ ∈ unop W then A else terminal.{w, v} C)
  (IsTerminal.from
    (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{w, v} C = x) ↦ IsTerminal.{w, v} x) terminalIsTerminal
      (if p₀ ∈ unop W then A else terminal.{w, v} C) sorry)
    (if p₀ ∈ unop U then A else terminal.{w, v} C))
  (CategoryStruct.comp (Y := if p₀ ∈ unop V then A else terminal.{w, v} C)
    (if h : p₀ ∈ unop V then eqToHom sorry
    else
      IsTerminal.from
        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{w, v} C = x) ↦ IsTerminal.{w, v} x) terminalIsTerminal
          (if p₀ ∈ unop V then A else terminal.{w, v} C) sorry)
        (if p₀ ∈ unop U then A else terminal.{w, v} C))
    (if h : p₀ ∈ unop W then eqToHom sorry
    else
      IsTerminal.from
        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{w, v} C = x) ↦ IsTerminal.{w, v} x) terminalIsTerminal
          (if p₀ ∈ unop W then A else terminal.{w, v} C) sorry)
        (if p₀ ∈ unop V then A else terminal.{w, v} C)))
Tactic: rw [dif_neg hW]
-- 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
hd : (U : Opens (↑(of PUnit.{u + 1}) : Type u)) → Decidable (PUnit.unit ∈ U)
⊢ Eq (α := Presheaf.{u, w, v} C X) (skyscraperPresheaf p₀ A)
    (Functor.obj (C := Presheaf.{u, w, v} C (of (↑(of PUnit.{u + 1}) : Type u)))
      (Presheaf.pushforward C (ofHom (ContinuousMap.const (↑(of PUnit.{u + 1}) : Type u) p₀)))
      (skyscraperPresheaf PUnit.unit A))
have h : Eq (α := Presheaf.{u, w, v} C X) (skyscraperPresheaf p₀ A) (skyscraperPresheaf p₀ A)
Tactic: convert_to @skyscraperPresheaf X p₀ (fun U => hd <| (Opens.map <| ofHom <|
      ContinuousMap.const _ p₀).obj U)
    C _ _ A = _
-- 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
hd : (U : Opens (↑(of PUnit.{u + 1}) : Type u)) → Decidable (PUnit.unit ∈ U)
h : Eq (α := Presheaf.{u, w, v} C X) (skyscraperPresheaf p₀ A) (skyscraperPresheaf p₀ A)
⊢ Eq (α := Presheaf.{u, w, v} C X) (skyscraperPresheaf p₀ A)
    (Functor.obj (C := Presheaf.{u, w, v} C (of (↑(of PUnit.{u + 1}) : Type u)))
      (Presheaf.pushforward C (ofHom (ContinuousMap.const (↑(of PUnit.{u + 1}) : Type u) p₀)))
      (skyscraperPresheaf PUnit.unit A))
have convert_2 : Eq (α := Presheaf.{u, w, v} C X) (skyscraperPresheaf p₀ A)
  (Functor.obj (C := Presheaf.{u, w, v} C (of (↑(of PUnit.{u + 1}) : Type u)))
    (Presheaf.pushforward C (ofHom (ContinuousMap.const (↑(of PUnit.{u + 1}) : Type u) p₀)))
    (skyscraperPresheaf PUnit.unit A))
Tactic: convert_to @skyscraperPresheaf X p₀ (fun U => hd <| (Opens.map <| ofHom <|
      ContinuousMap.const _ p₀).obj U)
    C _ _ A = _
-- 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 a b : C
f : a ⟶ b
U V : (Opens (↑X : Type u))ᵒᵖ
i : U ⟶ V
⊢ Eq.{w + 1} (α :=
    Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) U ⟶ Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ b) V)
    (CategoryTheory.Functor.map (skyscraperPresheaf p₀ a) i ≫
      if h : p₀ ∈ unop V then eqToHom ⋯ ≫ f ≫ eqToHom ⋯
      else
        IsTerminal.from (Eq.ndrec (motive := IsTerminal.{w, v}) terminalIsTerminal ⋯)
          (Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) V))
    ((if h : p₀ ∈ unop U then eqToHom ⋯ ≫ f ≫ eqToHom ⋯
      else
        IsTerminal.from (Eq.ndrec (motive := IsTerminal.{w, v}) terminalIsTerminal ⋯)
          (Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) U)) ≫
      CategoryTheory.Functor.map (skyscraperPresheaf p₀ b) i)
have simp : Eq.{w + 1} (α :=
  Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) U ⟶ Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ b) V)
  (CategoryStruct.comp (Y := Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) V)
    (if h : p₀ ∈ unop V then eqToHom sorry
    else
      IsTerminal.from
        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{w, v} C = x) ↦ IsTerminal.{w, v} x) terminalIsTerminal
          (if p₀ ∈ unop V then a else terminal.{w, v} C) sorry)
        (if p₀ ∈ unop U then a else terminal.{w, v} C))
    (if h : p₀ ∈ unop V then eqToHom sorry ≫ f ≫ eqToHom sorry
    else
      IsTerminal.from
        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{w, v} C = x) ↦ IsTerminal.{w, v} x) terminalIsTerminal
          (if p₀ ∈ unop V then b else terminal.{w, v} C) sorry)
        (Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) V)))
  (CategoryStruct.comp (Y := Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ b) U)
    (if h : p₀ ∈ unop U then eqToHom sorry ≫ f ≫ eqToHom sorry
    else
      IsTerminal.from
        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{w, v} C = x) ↦ IsTerminal.{w, v} x) terminalIsTerminal
          (if p₀ ∈ unop U then b else terminal.{w, v} C) sorry)
        (Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) U))
    (if h : p₀ ∈ unop V then eqToHom sorry
    else
      IsTerminal.from
        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{w, v} C = x) ↦ IsTerminal.{w, v} x) terminalIsTerminal
          (if p₀ ∈ unop V then b else terminal.{w, v} C) sorry)
        (if p₀ ∈ unop U then b else terminal.{w, v} C)))
Tactic: simp only [skyscraperPresheaf_map]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Skyscraper (hypothesis)
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 a b : C
f : a ⟶ b
U V : (Opens (↑X : Type u))ᵒᵖ
i : U ⟶ V
hV : p₀ ∈ unop V
⊢ Eq.{w + 1} (α :=
    Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) U ⟶ Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ b) V)
    (CategoryStruct.comp (Y := Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) V)
      (if h : p₀ ∈ unop V then eqToHom ⋯
      else
        IsTerminal.from
          (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{w, v} C = x) ↦ IsTerminal.{w, v} x) terminalIsTerminal
            (if p₀ ∈ unop V then a else terminal.{w, v} C) ⋯)
          (if p₀ ∈ unop U then a else terminal.{w, v} C))
      (if h : p₀ ∈ unop V then eqToHom ⋯ ≫ f ≫ eqToHom ⋯
      else
        IsTerminal.from
          (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{w, v} C = x) ↦ IsTerminal.{w, v} x) terminalIsTerminal
            (if p₀ ∈ unop V then b else terminal.{w, v} C) ⋯)
          (Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) V)))
    (CategoryStruct.comp (Y := Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ b) U)
      (if h : p₀ ∈ unop U then eqToHom ⋯ ≫ f ≫ eqToHom ⋯
      else
        IsTerminal.from
          (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{w, v} C = x) ↦ IsTerminal.{w, v} x) terminalIsTerminal
            (if p₀ ∈ unop U then b else terminal.{w, v} C) ⋯)
          (Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) U))
      (if h : p₀ ∈ unop V then eqToHom ⋯
      else
        IsTerminal.from
          (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{w, v} C = x) ↦ IsTerminal.{w, v} x) terminalIsTerminal
            (if p₀ ∈ unop V then b else terminal.{w, v} C) ⋯)
          (if p₀ ∈ unop U then b else terminal.{w, v} C)))
have hU : p₀ ∈ unop U
Tactic: have hU : p₀ ∈ U.unop := leOfHom i.unop hV
-- 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
⊢ Eq (α := Quiver.Hom (V := Presheaf.{u, w, v} C X) (skyscraperPresheaf p₀ a) (skyscraperPresheaf p₀ a)) (map' p₀ (𝟙 a))
    (𝟙 (skyscraperPresheaf p₀ a))
have w : ∀ (U : Opens (↑X : Type 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))
    (NatTrans.app (map' p₀ (𝟙 a)) (op U)) (NatTrans.app (𝟙 (skyscraperPresheaf p₀ a)) (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 : C
U : Opens (↑X : Type 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))
    (NatTrans.app (map' p₀ (𝟙 a)) (op U)) (NatTrans.app (𝟙 (skyscraperPresheaf p₀ a)) (op U))
have w : 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 sorry ≫ 𝟙 a ≫ 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 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: 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 : C
U : Opens (↑X : Type 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 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 sorry ≫ 𝟙 a ≫ eqToHom sorry) (NatTrans.app (𝟙 (skyscraperPresheaf p₀ a)) (op U))
Tactic: split_ifs