-- Lean 4 proof step from Mathlib.Topology.Sheaves.Skyscraper (goal)
Goal:
X : TopCat
p₀ : (↑X : Type u)
inst : (U : Opens (↑X : Type u)) → Decidable (p₀ ∈ U)
C : Type v
inst_1 : Category.{u, v} C
A : C
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
Y : C
U : Opens (↑X : Type u)
pos :
  ∀ (h : p₀ ∈ U),
    Eq (α := (if p₀ ∈ U then Y else terminal.{u, v} C) ⟶ if p₀ ∈ U then Y else terminal.{u, v} C)
      (CategoryStruct.comp (Y := if p₀ ∈ U then Presheaf.stalk (skyscraperPresheaf p₀ Y) p₀ else terminal.{u, v} C)
          (Presheaf.germ (skyscraperPresheaf p₀ Y) U p₀ ⋯ ≫ eqToHom ⋯)
          (eqToHom ⋯ ≫
            CategoryStruct.comp (Y := Y)
              (Iso.hom
                  (colimit.isoColimitCocone
                    { cocone := skyscraperPresheafCoconeOfSpecializes p₀ Y ⋯,
                      isColimit := skyscraperPresheafCoconeIsColimitOfSpecializes p₀ Y ⋯ }) :
                Presheaf.stalk (skyscraperPresheaf p₀ Y) p₀ ⟶ Y)
              (eqToHom ⋯)) :
        (if p₀ ∈ U then Y else terminal.{u, v} C) ⟶ if p₀ ∈ U then Y else terminal.{u, v} C)
      (NatTrans.app (𝟙 (skyscraperPresheaf p₀ Y)) (op U) :
        Functor.obj (skyscraperPresheaf p₀ Y) (op U) ⟶ Functor.obj (skyscraperPresheaf p₀ Y) (op U))
⊢ Eq (α := (if p₀ ∈ U then Y else terminal.{u, v} C) ⟶ if p₀ ∈ U then Y else terminal.{u, v} C)
    (CategoryStruct.comp (Y := if p₀ ∈ U then Presheaf.stalk (skyscraperPresheaf p₀ Y) p₀ else terminal.{u, v} C)
        (if h : p₀ ∈ U then Presheaf.germ (skyscraperPresheaf p₀ Y) U p₀ ⋯ ≫ eqToHom ⋯
        else
          IsTerminal.from
            (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
              (if p₀ ∈ U then Presheaf.stalk (skyscraperPresheaf p₀ Y) p₀ else terminal.{u, v} C) ⋯)
            (if p₀ ∈ U then Y else terminal.{u, v} C))
        (if h : p₀ ∈ U then
          eqToHom ⋯ ≫
            CategoryStruct.comp (Y := Y)
              (Iso.hom
                  (colimit.isoColimitCocone
                    { cocone := skyscraperPresheafCoconeOfSpecializes p₀ Y ⋯,
                      isColimit := skyscraperPresheafCoconeIsColimitOfSpecializes p₀ Y ⋯ }) :
                Presheaf.stalk (skyscraperPresheaf p₀ Y) p₀ ⟶ Y)
              (eqToHom ⋯)
        else
          IsTerminal.from
            (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
              (if p₀ ∈ U then Y else terminal.{u, v} C) ⋯)
            (if p₀ ∈ U then Presheaf.stalk (skyscraperPresheaf p₀ Y) p₀ else terminal.{u, v} C)) :
      (if p₀ ∈ U then Y else terminal.{u, v} C) ⟶ if p₀ ∈ U then Y else terminal.{u, v} C)
    (NatTrans.app (𝟙 (skyscraperPresheaf p₀ Y)) (op U) :
      Functor.obj (skyscraperPresheaf p₀ Y) (op U) ⟶ Functor.obj (skyscraperPresheaf p₀ Y) (op U))
have neg : ∀ (h : p₀ ∉ U),
  Eq.{u + 1} (α := (if p₀ ∈ U then Y else terminal.{u, v} C) ⟶ if p₀ ∈ U then Y else terminal.{u, v} C)
    (IsTerminal.from
        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
          (if p₀ ∈ U then Presheaf.stalk (skyscraperPresheaf p₀ Y) p₀ else terminal.{u, v} C) sorry)
        (if p₀ ∈ U then Y else terminal.{u, v} C) ≫
      IsTerminal.from
        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
          (if p₀ ∈ U then Y else terminal.{u, v} C) sorry)
        (if p₀ ∈ U then Presheaf.stalk (skyscraperPresheaf p₀ Y) p₀ else terminal.{u, v} C))
    (NatTrans.app (𝟙 (skyscraperPresheaf p₀ Y)) (op U))
Tactic: split_ifs with h