-- 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
inst_3 : HasColimits.{u, v} C
Y : C
U : Opens (↑X : Type u)
w :
  Eq (α := (if p₀ ∈ U then Y else terminal.{u, v} C) ⟶ if p₀ ∈ U then Y else terminal.{u, v} C)
    (CategoryStruct.comp (Y := if p₀ ∈ U then Presheaf.stalk (skyscraperPresheaf p₀ Y) p₀ else terminal.{u, v} C)
        (if h : p₀ ∈ U then Presheaf.germ (skyscraperPresheaf p₀ Y) U p₀ ⋯ ≫ eqToHom ⋯
        else
          IsTerminal.from
            (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
              (if p₀ ∈ U then Presheaf.stalk (skyscraperPresheaf p₀ Y) p₀ else terminal.{u, v} C) ⋯)
            (if p₀ ∈ U then Y else terminal.{u, v} C))
        (if h : p₀ ∈ U then
          eqToHom ⋯ ≫
            CategoryStruct.comp (Y := Y)
              (Iso.hom
                  (colimit.isoColimitCocone
                    { cocone := skyscraperPresheafCoconeOfSpecializes p₀ Y ⋯,
                      isColimit := skyscraperPresheafCoconeIsColimitOfSpecializes p₀ Y ⋯ }) :
                Presheaf.stalk (skyscraperPresheaf p₀ Y) p₀ ⟶ Y)
              (eqToHom ⋯)
        else
          IsTerminal.from
            (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
              (if p₀ ∈ U then Y else terminal.{u, v} C) ⋯)
            (if p₀ ∈ U then Presheaf.stalk (skyscraperPresheaf p₀ Y) p₀ else terminal.{u, v} C)) :
      (if p₀ ∈ U then Y else terminal.{u, v} C) ⟶ if p₀ ∈ U then Y else terminal.{u, v} C)
    (NatTrans.app (𝟙 (skyscraperPresheaf p₀ Y)) (op U) :
      Functor.obj (skyscraperPresheaf p₀ Y) (op U) ⟶ Functor.obj (skyscraperPresheaf p₀ Y) (op U))
⊢ Eq (α :=
    Functor.obj (Functor.obj (skyscraperPresheafFunctor p₀) Y) (op U) ⟶
      Functor.obj (Functor.obj (skyscraperPresheafFunctor p₀) Y) (op U))
    (NatTrans.app
      (CategoryStruct.comp (Y :=
        Functor.obj (skyscraperPresheafFunctor p₀)
          (Functor.obj (C := Presheaf C X) (Presheaf.stalkFunctor C p₀) (Functor.obj (skyscraperPresheafFunctor p₀) Y)))
        (NatTrans.app (StalkSkyscraperPresheafAdjunctionAuxs.unit p₀) (Functor.obj (skyscraperPresheafFunctor p₀) Y))
        (CategoryTheory.Functor.map (skyscraperPresheafFunctor p₀)
          (NatTrans.app (StalkSkyscraperPresheafAdjunctionAuxs.counit p₀) Y)))
      (op U))
    (NatTrans.app (𝟙 (Functor.obj (skyscraperPresheafFunctor p₀) Y)) (op U))

Tactic:
simp only [skyscraperPresheafFunctor_obj, Functor.id_obj, skyscraperPresheaf_obj,
      Presheaf.stalkFunctor_obj, unit_app, counit_app,
      skyscraperPresheafStalkOfSpecializes, skyscraperPresheafFunctor_map, Presheaf.comp_app,
      toSkyscraperPresheaf_app, Category.id_comp, SkyscraperPresheafFunctor.map'_app]

Premises used: skyscraperPresheaf_obj, StalkSkyscraperPresheafAdjunctionAuxs.counit_app, TopCat.Presheaf.comp_app, TopCat.Presheaf.stalkFunctor_obj, skyscraperPresheafStalkOfSpecializes, skyscraperPresheafFunctor_obj, StalkSkyscraperPresheafAdjunctionAuxs.unit_app, CategoryTheory.Functor.id_obj, SkyscraperPresheafFunctor.map'_app, skyscraperPresheafFunctor_map, CategoryTheory.Category.id_comp, StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf_app