-- 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)
U : (OpenNhds y)ᵒᵖ
⊢ Eq (α :=
    Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (op (unop U)) ⟶
      Functor.obj (Functor.obj (Functor.const (OpenNhds y)ᵒᵖ) c.pt) (op (unop U)))
    (CategoryStruct.comp (Y :=
        Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
          (op (h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u))) ⊓ unop U)))
        (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 Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (skyscraperPresheafCocone p₀ A y))
          (CategoryStruct.comp (Y :=
              Functor.obj
                (Functor.obj (Functor.const (OpenNhds y)ᵒᵖ)
                  (Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
                    (skyscraperPresheafCocone p₀ A y)))
                U)
              (NatTrans.app (Cocone.ι (skyscraperPresheafCocone p₀ A y)) U) (eqToHom ⋯) :
            Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) U ⟶
              if
                  p₀ ∈
                    (↑(h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u)))) :
                      Opens (↑X : Type u)) then
                A
              else
                Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (skyscraperPresheafCocone p₀ A y))
          (CategoryTheory.Functor.map ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
              (Quiver.Hom.op (homOfLE ⋯)) :
            Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
                (op (h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u))))) ⟶
              Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
                (op (h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u))) ⊓ unop U))))
        (c.ι.app (op (h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u))) ⊓ unop U))) :
      Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) U ⟶ c.pt)
    (CategoryStruct.comp (Y :=
        Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
          (op (h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u))) ⊓ unop U)))
        (CategoryTheory.Functor.map ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (Quiver.Hom.op (homOfLE ⋯)))
        (c.ι.app (op (h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u))) ⊓ unop U))) :
      Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (op (unop U)) ⟶ c.pt)
have e_a : Eq (α :=
  Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) U ⟶
    Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
      (op (h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u))) ⊓ unop U)))
  (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 Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (skyscraperPresheafCocone p₀ A y))
    (CategoryStruct.comp (Y :=
        Functor.obj
          (Functor.obj (Functor.const (OpenNhds y)ᵒᵖ)
            (Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (skyscraperPresheafCocone p₀ A y)))
          U)
        (NatTrans.app (Cocone.ι (skyscraperPresheafCocone p₀ A y)) U) (eqToHom sorry) :
      Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) U ⟶
        if p₀ ∈ (↑(h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u)))) : Opens (↑X : Type u)) then
          A
        else Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (skyscraperPresheafCocone p₀ A y))
    (CategoryTheory.Functor.map ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (Quiver.Hom.op (homOfLE sorry)) :
      Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
          (op (h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u))))) ⟶
        Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
          (op (h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u))) ⊓ unop U))))
  (CategoryTheory.Functor.map ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (Quiver.Hom.op (homOfLE sorry)))
Tactic: congr 1