Module: Mathlib.CategoryTheory.Sites.LeftExact

Goal state before:
pp: C : Type u
inst✝¹² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹¹ : Category.{t, w} D
inst✝¹⁰ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝⁹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁸ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁷ : ConcreteCategory D FD
inst✝⁶ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁵ : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
K : Type s
inst✝⁴ : SmallCategory K
inst✝³ : FinCategory K
inst✝² : HasLimitsOfShape K D
inst✝¹ : PreservesLimitsOfShape K (forget D)
inst✝ : ReflectsLimitsOfShape K (forget D)
F : K ⥤ Cᵒᵖ ⥤ D
X : C
S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))
F' : K ⥤ (J.Cover X)ᵒᵖ ⥤ D := F ⋙ J.diagramFunctor D X
e : colimit (limit (F ⋙ J.diagramFunctor D X)) ≅ limit (colimit (F ⋙ J.diagramFunctor D X).flip) :=
  colimitLimitIso (F ⋙ J.diagramFunctor D X)
t : J.diagram (limit F) X ≅ limit (F ⋙ J.diagramFunctor D X) :=
  (isLimitOfPreserves (J.diagramFunctor D X) (limit.isLimit F)).conePointUniqueUpToIso
    (limit.isLimit (F ⋙ J.diagramFunctor D X))
p : (J.plusObj (limit F)).obj (op X) ≅ colimit (limit (F ⋙ J.diagramFunctor D X)) := HasColimit.isoOfNatIso t
i j : K
f : i ⟶ j
w : (J.Cover (unop (op X)))ᵒᵖ
⊢ colimit.ι (J.diagram (F.obj i) X) w ≫
      (colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip i).inv ≫
        (colimit (F ⋙ J.diagramFunctor D X).flip).map f =
    colimit.ι (J.diagram (F.obj i) X) w ≫
      ((J.plusFunctor D).map (F.map f)).app (op X) ≫
        (colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip j).inv

Tactic:
erw [colimit.ι_map_assoc,
          colimitObjIsoColimitCompEvaluation_ι_inv (F ⋙ J.diagramFunctor D X).flip w j,
          colimitObjIsoColimitCompEvaluation_ι_inv_assoc (F ⋙ J.diagramFunctor D X).flip w i]

Goal state after:
C : Type u
inst✝¹² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹¹ : Category.{t, w} D
inst✝¹⁰ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝⁹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁸ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁷ : ConcreteCategory D FD
inst✝⁶ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁵ : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
K : Type s
inst✝⁴ : SmallCategory K
inst✝³ : FinCategory K
inst✝² : HasLimitsOfShape K D
inst✝¹ : PreservesLimitsOfShape K (forget D)
inst✝ : ReflectsLimitsOfShape K (forget D)
F : K ⥤ Cᵒᵖ ⥤ D
X : C
S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))
F' : K ⥤ (J.Cover X)ᵒᵖ ⥤ D := F ⋙ J.diagramFunctor D X
e : colimit (limit (F ⋙ J.diagramFunctor D X)) ≅ limit (colimit (F ⋙ J.diagramFunctor D X).flip) :=
  colimitLimitIso (F ⋙ J.diagramFunctor D X)
t : J.diagram (limit F) X ≅ limit (F ⋙ J.diagramFunctor D X) :=
  (isLimitOfPreserves (J.diagramFunctor D X) (limit.isLimit F)).conePointUniqueUpToIso
    (limit.isLimit (F ⋙ J.diagramFunctor D X))
p : (J.plusObj (limit F)).obj (op X) ≅ colimit (limit (F ⋙ J.diagramFunctor D X)) := HasColimit.isoOfNatIso t
i j : K
f : i ⟶ j
w : (J.Cover (unop (op X)))ᵒᵖ
⊢ (colimit.ι (F ⋙ J.diagramFunctor D X).flip w).app i ≫ (colimit (F ⋙ J.diagramFunctor D X).flip).map f =
    (J.diagramNatTrans (F.map f) (unop (op X))).app w ≫ (colimit.ι (F ⋙ J.diagramFunctor D X).flip w).app j