-- Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean
theorem colimitPresheafObjIsoComponentwiseLimit_inv_ι_app (F : J ⥤ PresheafedSpace.{_, _, v} C)
    (U : Opens (Limits.colimit F).carrier) (j : J) :
    (colimitPresheafObjIsoComponentwiseLimit F U).inv ≫ (colimit.ι F j).c.app (op U) =
      limit.π _ (op j)

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
U : Opens ↑↑(Limits.colimit F)
j : J
f : (componentwiseDiagram F U).obj (op j) ⟶ (F.obj j).presheaf.obj (op ((Opens.map (colimit.ι F j).base).obj U)) :=
  (NatIso.ofComponents (fun X => mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv.app (op j) ≫
    (F.obj j).presheaf.map (eqToHom ⋯) ≫ ((pushforward C (colimit.ι F j).base).obj (F.obj j).presheaf).map (eqToHom ⋯)
f_eq : f = 𝟙 ((componentwiseDiagram F U).obj (op j))
⊢ limit.π (componentwiseDiagram F U) (op j) ≫ f = limit.π (componentwiseDiagram F U) (op j)

Tactic:
rw [f_eq, comp_id]

Result:
no goals

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
U : Opens ↑↑(Limits.colimit F)
j : J
⊢ (colimitPresheafObjIsoComponentwiseLimit F U).inv ≫ (colimit.ι F j).c.app (op U) =
    limit.π (componentwiseDiagram F U) (op j)

Tactic:
delta colimitPresheafObjIsoComponentwiseLimit

Result:
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
U : Opens ↑↑(Limits.colimit F)
j : J
⊢ ((sheafIsoOfIso
                (colimit.isoColimitCocone
                    { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm).app
            (op U) ≪≫
          limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp
              ((Opens.map
                      (colimit.isoColimitCocone
                              { cocone := colimitCocone F,
                                isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj
                (op U)) ≪≫
            Limits.lim.mapIso (NatIso.ofComponents (fun X => mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯)).inv ≫
      (colimit.ι F j).c.app (op U) =
    limit.π (componentwiseDiagram F U) (op j)

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
U : Opens ↑↑(Limits.colimit F)
j : J
f : ?m.277584 := ?m.277585
⊢ limit.π (componentwiseDiagram F U) (op j) ≫
      (NatIso.ofComponents (fun X => mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv.app (op j) ≫
        (F.obj j).presheaf.map (eqToHom ⋯) ≫
          ((pushforward C (colimit.ι F j).base).obj (F.obj j).presheaf).map (eqToHom ⋯) =
    limit.π (componentwiseDiagram F U) (op j)

Tactic:
change _ ≫ f = _

Result:
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
U : Opens ↑↑(Limits.colimit F)
j : J
f : (componentwiseDiagram F U).obj (op j) ⟶ (F.obj j).presheaf.obj (op ((Opens.map (colimit.ι F j).base).obj U)) :=
  (NatIso.ofComponents (fun X => mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv.app (op j) ≫
    (F.obj j).presheaf.map (eqToHom ⋯) ≫ ((pushforward C (colimit.ι F j).base).obj (F.obj j).presheaf).map (eqToHom ⋯)
⊢ limit.π (componentwiseDiagram F U) (op j) ≫ f = limit.π (componentwiseDiagram F U) (op j)

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
U : Opens ↑↑(Limits.colimit F)
j : J
⊢ limMap (NatIso.ofComponents (fun X => mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv ≫
      (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp
            (op
              ((Opens.map
                    (colimit.isoColimitCocone
                          { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj
                U))).inv ≫
        ({ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.ι.app j).c.app
            (op
              ((Opens.map
                    (colimit.isoColimitCocone
                          { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj
                U)) ≫
          (F.obj j).presheaf.map (eqToHom ⋯) ≫
            ((pushforward C (colimit.ι F j).base).obj (F.obj j).presheaf).map (eqToHom ⋯) =
    limit.π (componentwiseDiagram F U) (op j)

Tactic:
erw [limitObjIsoLimitCompEvaluation_inv_π_app_assoc, limMap_π_assoc]

Result:
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
U : Opens ↑↑(Limits.colimit F)
j : J
⊢ limit.π (componentwiseDiagram F U) (op j) ≫
      (NatIso.ofComponents (fun X => mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv.app (op j) ≫
        (F.obj j).presheaf.map (eqToHom ⋯) ≫
          ((pushforward C (colimit.ι F j).base).obj (F.obj j).presheaf).map (eqToHom ⋯) =
    limit.π (componentwiseDiagram F U) (op j)