-- 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)ᵒᵖ
⊢ 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)
      (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))
        (eqToHom ⋯) (c.ι.app (op (h1.choose (p := fun (U : OpenNhds y) ↦ p₀ ∉ (↑U : Opens (↑X : Type u))))))) =
    c.ι.app (op (unop U))
have simp : 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 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))))
      (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 sorry)))
      (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)
Tactic: simp only [← c.w (homOfLE <| @inf_le_left _ _ h1.choose U.unop).op, ←
        c.w (homOfLE <| @inf_le_right _ _ h1.choose U.unop).op, ← Category.assoc]