-- 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)ᵒᵖ
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 ⋯) :
        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))))
    (CategoryTheory.Functor.map ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (Quiver.Hom.op (homOfLE ⋯)))
⊢ 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)

Tactic:
congr 1