-- Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean
theorem desc_fac (F : J ⥤ PresheafedSpace.{_, _, v} C) (s : Cocone F) (j : J) :
    (colimitCocone F).ι.app j ≫ desc F s = s.ι.app j

Proof state:
case h.w
J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
s : Cocone F
j : J
U : Opens ↑↑s.pt
⊢ (((colimitCocone F).ι.app j ≫ desc F s).c ≫ whiskerRight (eqToHom ⋯) (F.obj j).presheaf).app (op U) =
    (s.ι.app j).c.app (op U)

Tactic:
rw [NatTrans.comp_app, PresheafedSpace.comp_c_app, whiskerRight_app]

Result:
case h.w
J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
s : Cocone F
j : J
U : Opens ↑↑s.pt
⊢ ((desc F s).c.app (op U) ≫ ((colimitCocone F).ι.app j).c.app (op ((Opens.map (desc F s).base).obj (unop (op U))))) ≫
      (F.obj j).presheaf.map ((eqToHom ⋯).app (op U)) =
    (s.ι.app j).c.app (op U)

Proof state:
case h.w
J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
s : Cocone F
j : J
U : Opens ↑↑s.pt
⊢ ((limit.lift
            ((pushforwardDiagramToColimit F).leftOp ⋙
              (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj
                (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj U)))
            { pt := s.pt.presheaf.obj (op U),
              π :=
                { app := fun j => (s.ι.app (unop j)).c.app (op U) ≫ (F.obj (unop j)).presheaf.map (eqToHom ⋯),
                  naturality := ⋯ } } ≫
          (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp
              (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj U))).inv) ≫
        (limit.π (pushforwardDiagramToColimit F).leftOp (op j)).app
          (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj U))) ≫
      (F.obj j).presheaf.map ((eqToHom ⋯).app (op U)) =
    (s.ι.app j).c.app (op U)

Tactic:
simp only [eqToHom_app, op_obj, Opens.map_comp_obj, eqToHom_map, Functor.leftOp, assoc]

Result:
case h.w
J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
s : Cocone F
j : J
U : Opens ↑↑s.pt
⊢ limit.lift
        ({ obj := fun X => unop ((pushforwardDiagramToColimit F).obj (unop X)),
            map := fun {X Y} f => ((pushforwardDiagramToColimit F).map f.unop).unop, map_id := ⋯, map_comp := ⋯ } ⋙
          (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj
            (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj U)))
        { pt := s.pt.presheaf.obj (op U),
          π :=
            { app := fun j => (s.ι.app (unop j)).c.app (op U) ≫ (F.obj (unop j)).presheaf.map (eqToHom ⋯),
              naturality := ⋯ } } ≫
      (limitObjIsoLimitCompEvaluation
            { obj := fun X => unop ((pushforwardDiagramToColimit F).obj (unop X)),
              map := fun {X Y} f => ((pushforwardDiagramToColimit F).map f.unop).unop, map_id := ⋯, map_comp := ⋯ }
            (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj U))).inv ≫
        (limit.π
                { obj := fun X => unop ((pushforwardDiagramToColimit F).obj (unop X)),
                  map := fun {X Y} f => ((pushforwardDiagramToColimit F).map f.unop).unop, map_id := ⋯, map_comp := ⋯ }
                (op j)).app
            (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj U)) ≫
          eqToHom ⋯ =
    (s.ι.app j).c.app (op U)