-- 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
⊢ 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 := ⋯ } } ≫
      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 := ⋯ } ⋙
            (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj
              (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj U)))
          (op j) ≫
        eqToHom ⋯ =
    (s.ι.app j).c.app (op U)

Tactic:
simp

Result:
no goals

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
⊢ ((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)

Tactic:
dsimp [desc, descCApp]

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
            ((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)

Proof state:
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
⊢ (colimitCocone F).ι.app j ≫ desc F s = s.ι.app j

Tactic:
ext U

Result:
case w.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 : ↑↑(F.obj j)
⊢ (ConcreteCategory.hom ((colimitCocone F).ι.app j ≫ desc F s).base) U = (ConcreteCategory.hom (s.ι.app j).base) U

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)

Proof state:
case w.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 : ↑↑(F.obj j)
⊢ (ConcreteCategory.hom ((colimitCocone F).ι.app j ≫ desc F s).base) U = (ConcreteCategory.hom (s.ι.app j).base) U

Tactic:
simp [desc]

Result:
no goals

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
        ({ 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)

Tactic:
rw [limitObjIsoLimitCompEvaluation_inv_π_app_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 := ⋯ } } ≫
      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 := ⋯ } ⋙
            (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj
              (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj U)))
          (op j) ≫
        eqToHom ⋯ =
    (s.ι.app j).c.app (op U)