-- 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 = 𝟙 ((componentwiseDiagram F U).obj (op j))

Tactic:
erw [← (F.obj j).presheaf.map_id]

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 ⋯)
⊢ f = (F.obj j).presheaf.map (𝟙 (op ((Opens.map (colimit.ι F (unop (op j))).base).obj 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
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 = (F.obj j).presheaf.map (𝟙 (op ((Opens.map (colimit.ι F (unop (op j))).base).obj U)))

Tactic:
change (F.obj j).presheaf.map _ ≫ _ = _

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

Tactic:
dsimp

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
⊢ ((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) ≫
        ((colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom.c.app
              (op
                ((Opens.map
                      (colimit.isoColimitCocone
                            { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj
                  U)) ≫
            (Limits.colimit F).presheaf.map
              (𝟙
                (op
                  ((Opens.map
                        (colimit.isoColimitCocone
                              { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom.base).obj
                    ((Opens.map
                          (colimit.isoColimitCocone
                                { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj
                      U))))) ≫
          (Limits.colimit F).presheaf.map (eqToHom ⋯)) ≫
      (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 : (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)

Tactic:
suffices f_eq : f = 𝟙 _ by rw [f_eq, comp_id]

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 ⋯)
⊢ f = 𝟙 ((componentwiseDiagram F U).obj (op j))