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
y : (↑X : Type u)
h : ¬p₀ ⤳ y
h1 : ∃ (U : OpenNhds y), p₀ ∉ (↑U : Opens (↑X : Type u)) := ⋯
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
f : Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (skyscraperPresheafCocone p₀ A y) ⟶ c.pt
H : ∀ (j : (OpenNhds y)ᵒᵖ), NatTrans.app (Cocone.ι (skyscraperPresheafCocone p₀ A y)) j ≫ f = c.ι.app j
⊢ f =
    CategoryStruct.comp (Y :=
      if p₀ ∈ (↑(h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u)))) : Opens (↑X : Type u)) then A
      else terminal.{u, v} C)
      (eqToHom ⋯) (c.ι.app (op (h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u))))))
have rw : 𝟙 (Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (skyscraperPresheafCocone p₀ A y)) ≫ f =
  CategoryStruct.comp (Y :=
      if p₀ ∈ (↑(h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u)))) : Opens (↑X : Type u)) then A
      else terminal.{u, v} C)
      (eqToHom sorry)
      (NatTrans.app (Cocone.ι (skyscraperPresheafCocone p₀ A y))
        (op (h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u)))))) ≫
    f
Tactic: rw [← Category.id_comp f, ← H, ← Category.assoc]
-- 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)
f : Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (skyscraperPresheafCocone p₀ A y) ⟶ c.pt
H : ∀ (j : (OpenNhds y)ᵒᵖ), NatTrans.app (Cocone.ι (skyscraperPresheafCocone p₀ A y)) j ≫ f = c.ι.app j
⊢ 𝟙 (Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (skyscraperPresheafCocone p₀ A y)) ≫ f =
    CategoryStruct.comp (Y :=
        if p₀ ∈ (↑(h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u)))) : Opens (↑X : Type u)) then
          A
        else terminal.{u, v} C)
        (eqToHom ⋯)
        (NatTrans.app (Cocone.ι (skyscraperPresheafCocone p₀ A y))
          (op (h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u)))))) ≫
      f
have e_a : Eq.{u + 1} (α :=
  Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (skyscraperPresheafCocone p₀ A y) ⟶
    Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (skyscraperPresheafCocone p₀ A y))
  (𝟙 (Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (skyscraperPresheafCocone p₀ A y)))
  (CategoryStruct.comp (Y :=
    if p₀ ∈ (↑(h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u)))) : Opens (↑X : Type u)) then A
    else terminal.{u, v} C)
    (eqToHom sorry)
    (NatTrans.app (Cocone.ι (skyscraperPresheafCocone p₀ A y))
      (op (h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u)))))))
Tactic: congr 1
-- 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
⊢ IsTerminal.{u, v}
    (Functor.obj.{u, u, u, v} (C := (Opens (↑(of PUnit.{u + 1}) : Type u))ᵒᵖ) (skyscraperPresheaf PUnit.unit A) (op ⊥))
have dsimp : IsTerminal.{u, v} (if Membership.mem (γ := Opens PUnit.{u + 1}) ⊥ PUnit.unit then A else terminal.{u, v} C)
Tactic: dsimp [skyscraperPresheaf]
-- 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
⊢ IsTerminal.{u, v} (if Membership.mem (γ := Opens PUnit.{u + 1}) ⊥ PUnit.unit then A else terminal.{u, v} C)
have rw : IsTerminal.{u, v} (terminal.{u, v} C)
Tactic: rw [if_neg]
-- 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
rw : IsTerminal.{u, v} (terminal.{u, v} C)
⊢ IsTerminal.{u, v} (if Membership.mem (γ := Opens PUnit.{u + 1}) ⊥ PUnit.unit then A else terminal.{u, v} C)
have hnc : PUnit.unit ∉ ⊥
Tactic: rw [if_neg]
-- 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
c : C
f : 𝓕.stalk p₀ ⟶ c
U V : (Opens (↑X : Type u))ᵒᵖ
inc : U ⟶ V
⊢ 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)
have 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 sorry
    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) sorry)
        (𝓕.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 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 c else terminal.{u, v} C) sorry)
        (𝓕.obj U))
    (if h : p₀ ∈ unop V then 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 V then c else terminal.{u, v} C) sorry)
        (if p₀ ∈ unop U then c else terminal.{u, v} C)))
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
inst_3 : HasColimits.{u, v} C
𝓕 : Presheaf C X
c : C
f : 𝓕.stalk p₀ ⟶ c
U V : (Opens (↑X : Type u))ᵒᵖ
inc : U ⟶ V
⊢ 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)))
have pos : ∀ (hV : p₀ ∈ unop V),
  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 sorry
      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) sorry)
          (𝓕.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 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 c else terminal.{u, v} C) sorry)
          (𝓕.obj U))
      (if h : p₀ ∈ unop V then 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 V then c else terminal.{u, v} C) sorry)
          (if p₀ ∈ unop U then c else terminal.{u, v} C)))
Tactic: by_cases hV : p₀ ∈ V.unop
-- 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.{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 ≫
      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)))
have hU : p₀ ∈ unop U
Tactic: have hU : p₀ ∈ U.unop := leOfHom inc.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.{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
⊢ 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)))
have pos : Eq (α := 𝓕.obj U ⟶ if p₀ ∈ unop V then c else terminal.{u, v} C) (𝓕.map inc ≫ 𝓕.germ (unop V) p₀ hV ≫ f ≫ eqToHom sorry)
  ((𝓕.germ (unop U) p₀ hU ≫ f ≫ eqToHom sorry) ≫ eqToHom sorry)
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.{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
⊢ 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 ⋯)
have pos : Eq (α := 𝓕.obj U ⟶ if p₀ ∈ unop V then c else terminal.{u, v} C) ((𝓕.map inc ≫ 𝓕.germ (unop V) p₀ hV) ≫ f ≫ eqToHom sorry)
  ((𝓕.germ (unop U) p₀ hU ≫ f ≫ eqToHom sorry) ≫ eqToHom sorry)
Tactic: rw [← Category.assoc, 𝓕.germ_res' inc, Category.assoc, Category.assoc, eqToHom_trans]
-- 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
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 ≫ 𝓕.germ (unop V) p₀ hV ≫ f ≫ eqToHom ⋯)
    ((𝓕.germ (unop U) p₀ hU ≫ f ≫ eqToHom ⋯) ≫ eqToHom ⋯)
have pos₁ : Eq (α := 𝓕.obj U ⟶ if p₀ ∈ unop V then c else terminal.{u, v} C) (𝓕.germ (unop U) p₀ sorry ≫ f ≫ eqToHom sorry)
  ((𝓕.germ (unop U) p₀ hU ≫ f ≫ eqToHom sorry) ≫ eqToHom sorry)
Tactic: rw [← Category.assoc, 𝓕.germ_res' inc, Category.assoc, Category.assoc, eqToHom_trans]
-- 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
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 ⋯)
⊢ 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 ⋯)
have pos₂ : Eq (α := 𝓕.obj U ⟶ if p₀ ∈ unop V then c else terminal.{u, v} C) (𝓕.germ (unop U) p₀ sorry ≫ f ≫ eqToHom sorry)
  (𝓕.germ (unop U) p₀ hU ≫ (f ≫ eqToHom sorry) ≫ eqToHom sorry)
Tactic: rw [← Category.assoc, 𝓕.germ_res' inc, Category.assoc, Category.assoc, eqToHom_trans]
-- 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
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 ⋯)
⊢ 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 ⋯)
have pos₃ : Eq (α := 𝓕.obj U ⟶ if p₀ ∈ unop V then c else terminal.{u, v} C) (𝓕.germ (unop U) p₀ sorry ≫ f ≫ eqToHom sorry)
  (𝓕.germ (unop U) p₀ hU ≫ f ≫ eqToHom sorry ≫ eqToHom sorry)
Tactic: rw [← Category.assoc, 𝓕.germ_res' inc, Category.assoc, Category.assoc, eqToHom_trans]
-- 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
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 ⋯)
⊢ 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 ⋯)
have pos₄ : Eq (α := 𝓕.obj U ⟶ if p₀ ∈ unop V then c else terminal.{u, v} C) (𝓕.germ (unop U) p₀ sorry ≫ f ≫ eqToHom sorry)
  (𝓕.germ (unop U) p₀ hU ≫ f ≫ eqToHom sorry)
Tactic: rw [← Category.assoc, 𝓕.germ_res' inc, Category.assoc, Category.assoc, eqToHom_trans]
-- 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
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 ≫
      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)))
have 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) sorry)
      (𝓕.obj V))
  ((if h : p₀ ∈ unop U then 𝓕.germ (unop U) p₀ h ≫ f ≫ 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 c else terminal.{u, v} C) sorry)
        (𝓕.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) sorry)
      (if p₀ ∈ unop U then c else terminal.{u, v} C))
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.{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
⊢ 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)
have dsimp : 𝓕.map ((OpenNhds.inclusion p₀).op.map inc) ≫ f.app (op ((OpenNhds.inclusion p₀).obj (unop V))) ≫ eqToHom sorry =
  (f.app (op ((OpenNhds.inclusion p₀).obj (unop U))) ≫ eqToHom sorry) ≫ 𝟙 c
Tactic: dsimp only [Functor.const_obj_map, Functor.const_obj_obj, Functor.comp_map,
            Functor.comp_obj, Functor.op_obj, skyscraperPresheaf_obj]
-- 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
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U V : (OpenNhds p₀)ᵒᵖ
inc : U ⟶ V
⊢ 𝓕.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
have 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 sorry
    else
      IsTerminal.from (Eq.ndrec (motive := IsTerminal.{u, v}) terminalIsTerminal sorry)
        (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 sorry)
Tactic: rw [Category.comp_id, ← Category.assoc, comp_eqToHom_iff, Category.assoc,
            eqToHom_trans, f.naturality, 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.{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
⊢ 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 ⋯)
have hV : p₀ ∈ (OpenNhds.inclusion p₀).obj (unop V)
Tactic: have hV : p₀ ∈ (OpenNhds.inclusion p₀).obj V.unop := V.unop.2
-- 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
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
⊢ toSkyscraperPresheaf p₀ (fromStalk p₀ f) = f
have app : NatTrans.app (toSkyscraperPresheaf p₀ (fromStalk p₀ f)) = f.app
Tactic: apply NatTrans.ext