Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits

Goal state before:
pp: case refine_2
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
U : (Opens ↑↑s.pt)ᵒᵖ
j j' : Jᵒᵖ
f : j ⟶ j'
w :
  op
      ((Opens.map (colimit.ι (F ⋙ forget C) (unop j))).obj
        ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U))) =
    op ((Opens.map (((forget C).mapCocone s).ι.app (unop j))).obj (unop U))
w' :
  (F.map f.unop).c.app
      (op
        ((Opens.map (colimit.ι (F ⋙ forget C) (unop j))).obj
          ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U)))) =
    (F.obj (unop j)).presheaf.map (eqToHom w) ≫
      (F.map f.unop).c.app (op ((Opens.map (((forget C).mapCocone s).ι.app (unop j))).obj (unop U))) ≫
        ((pushforward C (F.map f.unop).base).obj (F.obj (unop j')).presheaf).map (eqToHom ⋯)
⊢ 𝟙 (s.pt.presheaf.obj U) ≫
      ((F.map f.unop ≫ s.ι.app (unop j)).c.app U ≫ (F.obj (unop j')).presheaf.map (eqToHom ⋯)) ≫
        (F.obj (unop j')).presheaf.map (eqToHom ⋯) =
    ((s.ι.app (unop j)).c.app U ≫ (F.obj (unop j)).presheaf.map (eqToHom ⋯)) ≫
      (F.map f.unop).c.app
          (op
            ((Opens.map (colimit.ι (F ⋙ forget C) (unop j))).obj
              ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U)))) ≫
        𝟙
            ((F.obj (unop j')).presheaf.obj
              (op
                ((Opens.map (F.map f.unop).base).obj
                  ((Opens.map (colimit.ι (F ⋙ forget C) (unop j))).obj
                    ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U)))))) ≫
          (pushforwardEq ⋯ (F.obj (unop j')).presheaf).hom.app
            (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U)))

Tactic:
rw [w']

Goal state after:
case refine_2
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
U : (Opens ↑↑s.pt)ᵒᵖ
j j' : Jᵒᵖ
f : j ⟶ j'
w :
  op
      ((Opens.map (colimit.ι (F ⋙ forget C) (unop j))).obj
        ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U))) =
    op ((Opens.map (((forget C).mapCocone s).ι.app (unop j))).obj (unop U))
w' :
  (F.map f.unop).c.app
      (op
        ((Opens.map (colimit.ι (F ⋙ forget C) (unop j))).obj
          ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U)))) =
    (F.obj (unop j)).presheaf.map (eqToHom w) ≫
      (F.map f.unop).c.app (op ((Opens.map (((forget C).mapCocone s).ι.app (unop j))).obj (unop U))) ≫
        ((pushforward C (F.map f.unop).base).obj (F.obj (unop j')).presheaf).map (eqToHom ⋯)
⊢ 𝟙 (s.pt.presheaf.obj U) ≫
      ((F.map f.unop ≫ s.ι.app (unop j)).c.app U ≫ (F.obj (unop j')).presheaf.map (eqToHom ⋯)) ≫
        (F.obj (unop j')).presheaf.map (eqToHom ⋯) =
    ((s.ι.app (unop j)).c.app U ≫ (F.obj (unop j)).presheaf.map (eqToHom ⋯)) ≫
      ((F.obj (unop j)).presheaf.map (eqToHom w) ≫
          (F.map f.unop).c.app (op ((Opens.map (((forget C).mapCocone s).ι.app (unop j))).obj (unop U))) ≫
            ((pushforward C (F.map f.unop).base).obj (F.obj (unop j')).presheaf).map (eqToHom ⋯)) ≫
        𝟙
            ((F.obj (unop j')).presheaf.obj
              (op
                ((Opens.map (F.map f.unop).base).obj
                  ((Opens.map (colimit.ι (F ⋙ forget C) (unop j))).obj
                    ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U)))))) ≫
          (pushforwardEq ⋯ (F.obj (unop j')).presheaf).hom.app
            (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U)))