-- 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
pos :
  ∀ (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)))
⊢ 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 neg : ∀ (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 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: by_cases hV : p₀ ∈ V.unop