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
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
⊢ NatTrans.app (toSkyscraperPresheaf p₀ (fromStalk p₀ f)) = f.app
have app : ∀ (U : (Opens (↑X : Type u))ᵒᵖ), NatTrans.app (toSkyscraperPresheaf p₀ (fromStalk p₀ f)) U = f.app 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.{u, v} C
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U : (Opens (↑X : Type u))ᵒᵖ
⊢ NatTrans.app (toSkyscraperPresheaf p₀ (fromStalk p₀ f)) U = f.app U
have app : (if h : p₀ ∈ unop U then CategoryStruct.comp (Y := 𝓕.stalk p₀) (𝓕.germ (unop U) p₀ h) (fromStalk p₀ 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)) =
  f.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
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U : (Opens (↑X : Type u))ᵒᵖ
⊢ (if h : p₀ ∈ unop U then CategoryStruct.comp (Y := 𝓕.stalk p₀) (𝓕.germ (unop U) p₀ h) (fromStalk p₀ f ≫ eqToHom ⋯)
    else
      IsTerminal.from
        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
          (if p₀ ∈ unop U then c else terminal.{u, v} C) ⋯)
        (𝓕.obj U)) =
    f.app U
have pos : ∀ (h : p₀ ∈ unop U), CategoryStruct.comp (Y := 𝓕.stalk p₀) (𝓕.germ (unop U) p₀ h) (fromStalk p₀ f ≫ eqToHom sorry) = f.app 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
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U : (Opens (↑X : Type u))ᵒᵖ
pos :
  ∀ (h : p₀ ∈ unop U),
    CategoryStruct.comp (Y := 𝓕.stalk p₀) (𝓕.germ (unop U) p₀ h) (fromStalk p₀ f ≫ eqToHom ⋯) = f.app U
⊢ (if h : p₀ ∈ unop U then CategoryStruct.comp (Y := 𝓕.stalk p₀) (𝓕.germ (unop U) p₀ h) (fromStalk p₀ f ≫ eqToHom ⋯)
    else
      IsTerminal.from
        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
          (if p₀ ∈ unop U then c else terminal.{u, v} C) ⋯)
        (𝓕.obj U)) =
    f.app U
have neg : ∀ (h : p₀ ∉ unop U),
  IsTerminal.from
      (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
        (if p₀ ∈ unop U then c else terminal.{u, v} C) sorry)
      (𝓕.obj U) =
    f.app 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
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
𝓕 : Presheaf C X
c : C
f : 𝓕.stalk p₀ ⟶ c
⊢ fromStalk p₀ (toSkyscraperPresheaf p₀ f) = f
have refine : ∀ (U : Opens (↑X : Type u)) (hxU : p₀ ∈ U),
  CategoryStruct.comp (Y := 𝓕.stalk p₀) (𝓕.germ U p₀ hxU) (fromStalk p₀ (toSkyscraperPresheaf p₀ f)) =
    𝓕.germ U p₀ hxU ≫ f
Tactic: refine 𝓕.stalk_hom_ext fun U hxU ↦ ?_
-- 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 : 𝓕.stalk p₀ ⟶ c
U : Opens (↑X : Type u)
hxU : p₀ ∈ U
⊢ CategoryStruct.comp (Y := 𝓕.stalk p₀) (𝓕.germ U p₀ hxU) (fromStalk p₀ (toSkyscraperPresheaf p₀ f)) =
    𝓕.germ U p₀ hxU ≫ f
have rw : CategoryStruct.comp (Y := Functor.obj (skyscraperPresheaf p₀ c) (op U))
    (NatTrans.app (toSkyscraperPresheaf p₀ f) (op U)) (eqToHom sorry) =
  𝓕.germ U p₀ hxU ≫ f
Tactic: rw [germ_fromStalk, toSkyscraperPresheaf_app, dif_pos hxU, Category.assoc, Category.assoc,
    eqToHom_trans, eqToHom_refl, Category.comp_id, Presheaf.germ]
-- 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 : 𝓕.stalk p₀ ⟶ c
U : Opens (↑X : Type u)
hxU : p₀ ∈ U
rw :
  CategoryStruct.comp (Y := Functor.obj (skyscraperPresheaf p₀ c) (op U))
      (NatTrans.app (toSkyscraperPresheaf p₀ f) (op U)) (eqToHom ⋯) =
    𝓕.germ U p₀ hxU ≫ f
⊢ CategoryStruct.comp (Y := 𝓕.stalk p₀) (𝓕.germ U p₀ hxU) (fromStalk p₀ (toSkyscraperPresheaf p₀ f)) =
    𝓕.germ U p₀ hxU ≫ f
have rw₁ : CategoryStruct.comp (Y := Functor.obj (skyscraperPresheaf p₀ c) (op U))
    (if h : p₀ ∈ unop (op U) then 𝓕.germ (unop (op U)) p₀ h ≫ f ≫ eqToHom sorry
    else IsTerminal.from (Eq.ndrec (motive := IsTerminal.{u, v}) terminalIsTerminal sorry) (𝓕.obj (op U)))
    (eqToHom sorry) =
  𝓕.germ U p₀ hxU ≫ f
Tactic: rw [germ_fromStalk, toSkyscraperPresheaf_app, dif_pos hxU, Category.assoc, Category.assoc,
    eqToHom_trans, eqToHom_refl, Category.comp_id, Presheaf.germ]
-- 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 : 𝓕.stalk p₀ ⟶ c
U : Opens (↑X : Type u)
hxU : p₀ ∈ U
rw :
  CategoryStruct.comp (Y := Functor.obj (skyscraperPresheaf p₀ c) (op U))
      (NatTrans.app (toSkyscraperPresheaf p₀ f) (op U)) (eqToHom ⋯) =
    𝓕.germ U p₀ hxU ≫ f
rw₁ :
  CategoryStruct.comp (Y := Functor.obj (skyscraperPresheaf p₀ c) (op U))
      (if h : p₀ ∈ unop (op U) then 𝓕.germ (unop (op U)) p₀ h ≫ f ≫ eqToHom ⋯
      else IsTerminal.from (Eq.ndrec (motive := IsTerminal.{u, v}) terminalIsTerminal ⋯) (𝓕.obj (op U)))
      (eqToHom ⋯) =
    𝓕.germ U p₀ hxU ≫ f
⊢ CategoryStruct.comp (Y := 𝓕.stalk p₀) (𝓕.germ U p₀ hxU) (fromStalk p₀ (toSkyscraperPresheaf p₀ f)) =
    𝓕.germ U p₀ hxU ≫ f
have rw₂ : CategoryStruct.comp (Y := Functor.obj (skyscraperPresheaf p₀ c) (op U)) (𝓕.germ (unop (op U)) p₀ hxU ≫ f ≫ eqToHom sorry)
    (eqToHom sorry) =
  𝓕.germ U p₀ hxU ≫ f
Tactic: rw [germ_fromStalk, toSkyscraperPresheaf_app, dif_pos hxU, Category.assoc, Category.assoc,
    eqToHom_trans, eqToHom_refl, Category.comp_id, Presheaf.germ]
-- 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 : 𝓕.stalk p₀ ⟶ c
U : Opens (↑X : Type u)
hxU : p₀ ∈ U
rw :
  CategoryStruct.comp (Y := Functor.obj (skyscraperPresheaf p₀ c) (op U))
      (NatTrans.app (toSkyscraperPresheaf p₀ f) (op U)) (eqToHom ⋯) =
    𝓕.germ U p₀ hxU ≫ f
rw₁ :
  CategoryStruct.comp (Y := Functor.obj (skyscraperPresheaf p₀ c) (op U))
      (if h : p₀ ∈ unop (op U) then 𝓕.germ (unop (op U)) p₀ h ≫ f ≫ eqToHom ⋯
      else IsTerminal.from (Eq.ndrec (motive := IsTerminal.{u, v}) terminalIsTerminal ⋯) (𝓕.obj (op U)))
      (eqToHom ⋯) =
    𝓕.germ U p₀ hxU ≫ f
rw₂ :
  CategoryStruct.comp (Y := Functor.obj (skyscraperPresheaf p₀ c) (op U)) (𝓕.germ (unop (op U)) p₀ hxU ≫ f ≫ eqToHom ⋯)
      (eqToHom ⋯) =
    𝓕.germ U p₀ hxU ≫ f
⊢ CategoryStruct.comp (Y := 𝓕.stalk p₀) (𝓕.germ U p₀ hxU) (fromStalk p₀ (toSkyscraperPresheaf p₀ f)) =
    𝓕.germ U p₀ hxU ≫ f
have rw₃ : 𝓕.germ (unop (op U)) p₀ hxU ≫
    CategoryStruct.comp (Y := Functor.obj (skyscraperPresheaf p₀ c) (op U)) (f ≫ eqToHom sorry) (eqToHom sorry) =
  𝓕.germ U p₀ hxU ≫ f
Tactic: rw [germ_fromStalk, toSkyscraperPresheaf_app, dif_pos hxU, Category.assoc, Category.assoc,
    eqToHom_trans, eqToHom_refl, Category.comp_id, Presheaf.germ]
-- 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 : 𝓕.stalk p₀ ⟶ c
U : Opens (↑X : Type u)
hxU : p₀ ∈ U
rw :
  CategoryStruct.comp (Y := Functor.obj (skyscraperPresheaf p₀ c) (op U))
      (NatTrans.app (toSkyscraperPresheaf p₀ f) (op U)) (eqToHom ⋯) =
    𝓕.germ U p₀ hxU ≫ f
rw₁ :
  CategoryStruct.comp (Y := Functor.obj (skyscraperPresheaf p₀ c) (op U))
      (if h : p₀ ∈ unop (op U) then 𝓕.germ (unop (op U)) p₀ h ≫ f ≫ eqToHom ⋯
      else IsTerminal.from (Eq.ndrec (motive := IsTerminal.{u, v}) terminalIsTerminal ⋯) (𝓕.obj (op U)))
      (eqToHom ⋯) =
    𝓕.germ U p₀ hxU ≫ f
rw₂ :
  CategoryStruct.comp (Y := Functor.obj (skyscraperPresheaf p₀ c) (op U)) (𝓕.germ (unop (op U)) p₀ hxU ≫ f ≫ eqToHom ⋯)
      (eqToHom ⋯) =
    𝓕.germ U p₀ hxU ≫ f
rw₃ :
  𝓕.germ (unop (op U)) p₀ hxU ≫
      CategoryStruct.comp (Y := Functor.obj (skyscraperPresheaf p₀ c) (op U)) (f ≫ eqToHom ⋯) (eqToHom ⋯) =
    𝓕.germ U p₀ hxU ≫ f
⊢ CategoryStruct.comp (Y := 𝓕.stalk p₀) (𝓕.germ U p₀ hxU) (fromStalk p₀ (toSkyscraperPresheaf p₀ f)) =
    𝓕.germ U p₀ hxU ≫ f
have rw₄ : 𝓕.germ (unop (op U)) p₀ hxU ≫
    f ≫ CategoryStruct.comp (Y := Functor.obj (skyscraperPresheaf p₀ c) (op U)) (eqToHom sorry) (eqToHom sorry) =
  𝓕.germ U p₀ hxU ≫ f
Tactic: rw [germ_fromStalk, toSkyscraperPresheaf_app, dif_pos hxU, Category.assoc, Category.assoc,
    eqToHom_trans, eqToHom_refl, Category.comp_id, Presheaf.germ]
-- 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 : 𝓕.stalk p₀ ⟶ c
U : Opens (↑X : Type u)
hxU : p₀ ∈ U
rw :
  CategoryStruct.comp (Y := Functor.obj (skyscraperPresheaf p₀ c) (op U))
      (NatTrans.app (toSkyscraperPresheaf p₀ f) (op U)) (eqToHom ⋯) =
    𝓕.germ U p₀ hxU ≫ f
rw₁ :
  CategoryStruct.comp (Y := Functor.obj (skyscraperPresheaf p₀ c) (op U))
      (if h : p₀ ∈ unop (op U) then 𝓕.germ (unop (op U)) p₀ h ≫ f ≫ eqToHom ⋯
      else IsTerminal.from (Eq.ndrec (motive := IsTerminal.{u, v}) terminalIsTerminal ⋯) (𝓕.obj (op U)))
      (eqToHom ⋯) =
    𝓕.germ U p₀ hxU ≫ f
rw₂ :
  CategoryStruct.comp (Y := Functor.obj (skyscraperPresheaf p₀ c) (op U)) (𝓕.germ (unop (op U)) p₀ hxU ≫ f ≫ eqToHom ⋯)
      (eqToHom ⋯) =
    𝓕.germ U p₀ hxU ≫ f
rw₃ :
  𝓕.germ (unop (op U)) p₀ hxU ≫
      CategoryStruct.comp (Y := Functor.obj (skyscraperPresheaf p₀ c) (op U)) (f ≫ eqToHom ⋯) (eqToHom ⋯) =
    𝓕.germ U p₀ hxU ≫ f
rw₄ :
  𝓕.germ (unop (op U)) p₀ hxU ≫
      f ≫ CategoryStruct.comp (Y := Functor.obj (skyscraperPresheaf p₀ c) (op U)) (eqToHom ⋯) (eqToHom ⋯) =
    𝓕.germ U p₀ hxU ≫ f
⊢ CategoryStruct.comp (Y := 𝓕.stalk p₀) (𝓕.germ U p₀ hxU) (fromStalk p₀ (toSkyscraperPresheaf p₀ f)) =
    𝓕.germ U p₀ hxU ≫ f
have rw₅ : 𝓕.germ (unop (op U)) p₀ hxU ≫ f ≫ eqToHom sorry = 𝓕.germ U p₀ hxU ≫ f
Tactic: rw [germ_fromStalk, toSkyscraperPresheaf_app, dif_pos hxU, Category.assoc, Category.assoc,
    eqToHom_trans, eqToHom_refl, Category.comp_id, Presheaf.germ]
-- 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 : 𝓕.stalk p₀ ⟶ c
U : Opens (↑X : Type u)
hxU : p₀ ∈ U
rw :
  CategoryStruct.comp (Y := Functor.obj (skyscraperPresheaf p₀ c) (op U))
      (NatTrans.app (toSkyscraperPresheaf p₀ f) (op U)) (eqToHom ⋯) =
    𝓕.germ U p₀ hxU ≫ f
rw₁ :
  CategoryStruct.comp (Y := Functor.obj (skyscraperPresheaf p₀ c) (op U))
      (if h : p₀ ∈ unop (op U) then 𝓕.germ (unop (op U)) p₀ h ≫ f ≫ eqToHom ⋯
      else IsTerminal.from (Eq.ndrec (motive := IsTerminal.{u, v}) terminalIsTerminal ⋯) (𝓕.obj (op U)))
      (eqToHom ⋯) =
    𝓕.germ U p₀ hxU ≫ f
rw₂ :
  CategoryStruct.comp (Y := Functor.obj (skyscraperPresheaf p₀ c) (op U)) (𝓕.germ (unop (op U)) p₀ hxU ≫ f ≫ eqToHom ⋯)
      (eqToHom ⋯) =
    𝓕.germ U p₀ hxU ≫ f
rw₃ :
  𝓕.germ (unop (op U)) p₀ hxU ≫
      CategoryStruct.comp (Y := Functor.obj (skyscraperPresheaf p₀ c) (op U)) (f ≫ eqToHom ⋯) (eqToHom ⋯) =
    𝓕.germ U p₀ hxU ≫ f
rw₄ :
  𝓕.germ (unop (op U)) p₀ hxU ≫
      f ≫ CategoryStruct.comp (Y := Functor.obj (skyscraperPresheaf p₀ c) (op U)) (eqToHom ⋯) (eqToHom ⋯) =
    𝓕.germ U p₀ hxU ≫ f
rw₅ : 𝓕.germ (unop (op U)) p₀ hxU ≫ f ≫ eqToHom ⋯ = 𝓕.germ U p₀ hxU ≫ f
⊢ CategoryStruct.comp (Y := 𝓕.stalk p₀) (𝓕.germ U p₀ hxU) (fromStalk p₀ (toSkyscraperPresheaf p₀ f)) =
    𝓕.germ U p₀ hxU ≫ f
have rw₆ : 𝓕.germ (unop (op U)) p₀ hxU ≫ f ≫ 𝟙 c = 𝓕.germ U p₀ hxU ≫ f
Tactic: rw [germ_fromStalk, toSkyscraperPresheaf_app, dif_pos hxU, Category.assoc, Category.assoc,
    eqToHom_trans, eqToHom_refl, Category.comp_id, Presheaf.germ]
-- 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 : 𝓕.stalk p₀ ⟶ c
U : Opens (↑X : Type u)
hxU : p₀ ∈ U
rw :
  CategoryStruct.comp (Y := Functor.obj (skyscraperPresheaf p₀ c) (op U))
      (NatTrans.app (toSkyscraperPresheaf p₀ f) (op U)) (eqToHom ⋯) =
    𝓕.germ U p₀ hxU ≫ f
rw₁ :
  CategoryStruct.comp (Y := Functor.obj (skyscraperPresheaf p₀ c) (op U))
      (if h : p₀ ∈ unop (op U) then 𝓕.germ (unop (op U)) p₀ h ≫ f ≫ eqToHom ⋯
      else IsTerminal.from (Eq.ndrec (motive := IsTerminal.{u, v}) terminalIsTerminal ⋯) (𝓕.obj (op U)))
      (eqToHom ⋯) =
    𝓕.germ U p₀ hxU ≫ f
rw₂ :
  CategoryStruct.comp (Y := Functor.obj (skyscraperPresheaf p₀ c) (op U)) (𝓕.germ (unop (op U)) p₀ hxU ≫ f ≫ eqToHom ⋯)
      (eqToHom ⋯) =
    𝓕.germ U p₀ hxU ≫ f
rw₃ :
  𝓕.germ (unop (op U)) p₀ hxU ≫
      CategoryStruct.comp (Y := Functor.obj (skyscraperPresheaf p₀ c) (op U)) (f ≫ eqToHom ⋯) (eqToHom ⋯) =
    𝓕.germ U p₀ hxU ≫ f
rw₄ :
  𝓕.germ (unop (op U)) p₀ hxU ≫
      f ≫ CategoryStruct.comp (Y := Functor.obj (skyscraperPresheaf p₀ c) (op U)) (eqToHom ⋯) (eqToHom ⋯) =
    𝓕.germ U p₀ hxU ≫ f
rw₅ : 𝓕.germ (unop (op U)) p₀ hxU ≫ f ≫ eqToHom ⋯ = 𝓕.germ U p₀ hxU ≫ f
rw₆ : 𝓕.germ (unop (op U)) p₀ hxU ≫ f ≫ 𝟙 c = 𝓕.germ U p₀ hxU ≫ f
⊢ CategoryStruct.comp (Y := 𝓕.stalk p₀) (𝓕.germ U p₀ hxU) (fromStalk p₀ (toSkyscraperPresheaf p₀ f)) =
    𝓕.germ U p₀ hxU ≫ f
have rw₇ : 𝓕.germ (unop (op U)) p₀ hxU ≫ f = 𝓕.germ U p₀ hxU ≫ f
Tactic: rw [germ_fromStalk, toSkyscraperPresheaf_app, dif_pos hxU, Category.assoc, Category.assoc,
    eqToHom_trans, eqToHom_refl, Category.comp_id, Presheaf.germ]
-- 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 : 𝓕.stalk p₀ ⟶ c
U : Opens (↑X : Type u)
hxU : p₀ ∈ U
rw :
  CategoryStruct.comp (Y := Functor.obj (skyscraperPresheaf p₀ c) (op U))
      (NatTrans.app (toSkyscraperPresheaf p₀ f) (op U)) (eqToHom ⋯) =
    𝓕.germ U p₀ hxU ≫ f
rw₁ :
  CategoryStruct.comp (Y := Functor.obj (skyscraperPresheaf p₀ c) (op U))
      (if h : p₀ ∈ unop (op U) then 𝓕.germ (unop (op U)) p₀ h ≫ f ≫ eqToHom ⋯
      else IsTerminal.from (Eq.ndrec (motive := IsTerminal.{u, v}) terminalIsTerminal ⋯) (𝓕.obj (op U)))
      (eqToHom ⋯) =
    𝓕.germ U p₀ hxU ≫ f
rw₂ :
  CategoryStruct.comp (Y := Functor.obj (skyscraperPresheaf p₀ c) (op U)) (𝓕.germ (unop (op U)) p₀ hxU ≫ f ≫ eqToHom ⋯)
      (eqToHom ⋯) =
    𝓕.germ U p₀ hxU ≫ f
rw₃ :
  𝓕.germ (unop (op U)) p₀ hxU ≫
      CategoryStruct.comp (Y := Functor.obj (skyscraperPresheaf p₀ c) (op U)) (f ≫ eqToHom ⋯) (eqToHom ⋯) =
    𝓕.germ U p₀ hxU ≫ f
rw₄ :
  𝓕.germ (unop (op U)) p₀ hxU ≫
      f ≫ CategoryStruct.comp (Y := Functor.obj (skyscraperPresheaf p₀ c) (op U)) (eqToHom ⋯) (eqToHom ⋯) =
    𝓕.germ U p₀ hxU ≫ f
rw₅ : 𝓕.germ (unop (op U)) p₀ hxU ≫ f ≫ eqToHom ⋯ = 𝓕.germ U p₀ hxU ≫ f
rw₆ : 𝓕.germ (unop (op U)) p₀ hxU ≫ f ≫ 𝟙 c = 𝓕.germ U p₀ hxU ≫ f
rw₇ : 𝓕.germ (unop (op U)) p₀ hxU ≫ f = 𝓕.germ U p₀ hxU ≫ f
⊢ CategoryStruct.comp (Y := 𝓕.stalk p₀) (𝓕.germ U p₀ hxU) (fromStalk p₀ (toSkyscraperPresheaf p₀ f)) =
    𝓕.germ U p₀ hxU ≫ f
have rw₈ : Eq (α := 𝓕.obj (op U) ⟶ c)
  (colimit.ι ((OpenNhds.inclusion p₀).op ⋙ 𝓕)
        (op (Subtype.mk (p := fun (U : Opens (↑X : Type u)) ↦ p₀ ∈ U) (unop (op U)) hxU)) ≫
      f :
    𝓕.obj (op U) ⟶ c)
  (colimit.ι ((OpenNhds.inclusion p₀).op ⋙ 𝓕)
        (op (Subtype.mk (p := fun (U : Opens (↑X : Type u)) ↦ p₀ ∈ U) (unop (op U)) hxU)) ≫
      f :
    𝓕.obj (op U) ⟶ c)
Tactic: rw [germ_fromStalk, toSkyscraperPresheaf_app, dif_pos hxU, Category.assoc, Category.assoc,
    eqToHom_trans, eqToHom_refl, Category.comp_id, Presheaf.germ]
-- 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 : 𝓕 ⟶ 𝓖
⊢ Eq (α := Functor.obj (𝟭 (Presheaf C X)) 𝓕 ⟶ Functor.obj (Presheaf.stalkFunctor C p₀ ⋙ skyscraperPresheafFunctor p₀) 𝓖)
    (CategoryTheory.Functor.map (𝟭 (Presheaf C X)) f ≫
      toSkyscraperPresheaf p₀ (𝟙 ((Functor.obj (𝟭 (Presheaf C X)) 𝓖).stalk p₀)))
    (CategoryStruct.comp (Y := Functor.obj (Presheaf.stalkFunctor C p₀ ⋙ skyscraperPresheafFunctor p₀) 𝓕)
      (toSkyscraperPresheaf p₀ (𝟙 ((Functor.obj (𝟭 (Presheaf C X)) 𝓕).stalk p₀)))
      (CategoryTheory.Functor.map (Presheaf.stalkFunctor C p₀ ⋙ skyscraperPresheafFunctor p₀) f))
have w : ∀ (U : Opens (↑X : Type u)),
  Eq (α :=
    (Functor.obj (𝟭 (Presheaf C X)) 𝓕).obj (op U) ⟶
      (Functor.obj (Presheaf.stalkFunctor C p₀ ⋙ skyscraperPresheafFunctor p₀) 𝓖).obj (op U))
    (NatTrans.app
      (CategoryTheory.Functor.map (𝟭 (Presheaf C X)) f ≫
        toSkyscraperPresheaf p₀ (𝟙 ((Functor.obj (𝟭 (Presheaf C X)) 𝓖).stalk p₀)))
      (op U))
    (NatTrans.app
      (CategoryStruct.comp (Y := Functor.obj (Presheaf.stalkFunctor C p₀ ⋙ skyscraperPresheafFunctor p₀) 𝓕)
        (toSkyscraperPresheaf p₀ (𝟙 ((Functor.obj (𝟭 (Presheaf C X)) 𝓕).stalk p₀)))
        (CategoryTheory.Functor.map (Presheaf.stalkFunctor C p₀ ⋙ skyscraperPresheafFunctor p₀) f))
      (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.{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)
⊢ Eq (α :=
    (Functor.obj (𝟭 (Presheaf C X)) 𝓕).obj (op U) ⟶
      (Functor.obj (Presheaf.stalkFunctor C p₀ ⋙ skyscraperPresheafFunctor p₀) 𝓖).obj (op U))
    (NatTrans.app
      (CategoryTheory.Functor.map (𝟭 (Presheaf C X)) f ≫
        toSkyscraperPresheaf p₀ (𝟙 ((Functor.obj (𝟭 (Presheaf C X)) 𝓖).stalk p₀)))
      (op U))
    (NatTrans.app
      (CategoryStruct.comp (Y := Functor.obj (Presheaf.stalkFunctor C p₀ ⋙ skyscraperPresheafFunctor p₀) 𝓕)
        (toSkyscraperPresheaf p₀ (𝟙 ((Functor.obj (𝟭 (Presheaf C X)) 𝓕).stalk p₀)))
        (CategoryTheory.Functor.map (Presheaf.stalkFunctor C p₀ ⋙ skyscraperPresheafFunctor p₀) f))
      (op U))
have w : 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 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 𝓖.stalk p₀ else terminal.{u, v} C) sorry)
        (𝓖.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 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 𝓕.stalk p₀ else terminal.{u, v} C) sorry)
        (𝓕.obj (op U)))
    (if h : p₀ ∈ U then eqToHom sorry ≫ CategoryTheory.Functor.map (Presheaf.stalkFunctor C p₀) 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₀ ∈ U then 𝓖.stalk p₀ else terminal.{u, v} C) sorry)
        (if p₀ ∈ U then 𝓕.stalk p₀ 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
f : 𝓕 ⟶ 𝓖
U : Opens (↑X : Type u)
⊢ 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 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 sorry)
    (CategoryStruct.comp (Y := if p₀ ∈ U then 𝓕.stalk p₀ else terminal.{u, v} C)
      (𝓕.germ U p₀ h ≫ 𝟙 (𝓕.stalk p₀) ≫ eqToHom sorry)
      (eqToHom sorry ≫ CategoryTheory.Functor.map (Presheaf.stalkFunctor C p₀) f ≫ eqToHom sorry))
Tactic: split_ifs with h