-- Module: Mathlib.Topology.Sheaves.Skyscraper
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)ᵒᵖ
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 ⋯) :
            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)
⊢ 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))

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]

Premises used: CategoryTheory.Category.assoc, Quiver.Hom.op, inf_le_right, CategoryTheory.Limits.Cocone.w, CategoryTheory.homOfLE, inf_le_left