-- 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
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 ⋯
        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)))
⊢ 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 : ∀ (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