-- Module: Mathlib.CategoryTheory.Sites.LeftExact
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{t, w} D
inst_2 : ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst_4 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
inst_5 : ConcreteCategory D FD (CC := CD)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_7 : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
K : Type s
inst_8 : SmallCategory K
inst_9 : FinCategory K
inst_10 : HasLimitsOfShape.{s, s, t, w} K D
inst_11 : PreservesLimitsOfShape K (forget D (FC := FD) (CC := CD))
inst_12 : ReflectsLimitsOfShape K (forget D (FC := FD) (CC := CD))
F : K ⥤ Functor.{v, t, u, w} Cᵒᵖ D
X : C
S : Cone (F ⋙ J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) (op X))
x : Type (max 0 u v) := (J.Cover 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) :=
  IsLimit.conePointUniqueUpToIso (isLimitOfPreserves (J.diagramFunctor D X) (limit.isLimit F))
    (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)))ᵒᵖ
dsimp :
  CategoryStruct.comp (Y := colimit (J.diagram (F.obj i) X))
      (colimit.ι (J.diagram (F.obj i) X) w : (J.diagram (F.obj i) X).obj w ⟶ colimit (J.diagram (F.obj i) X))
      (Iso.inv (colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip i) ≫
          (colimit (F ⋙ J.diagramFunctor D X).flip).map f :
        (J.plusObj (F.obj i)).obj (op X) ⟶ (colimit (F ⋙ J.diagramFunctor D X).flip).obj j) =
    CategoryStruct.comp (Y := colimit (J.diagram (F.obj i) X)) (colimit.ι (J.diagram (F.obj i) X) w)
      (CategoryStruct.comp (Y := (J.plusObj (F.obj j)).obj (op X))
        (colimMap (J.diagramNatTrans (F.map f) X) : colimit (J.diagram (F.obj i) X) ⟶ colimit (J.diagram (F.obj j) X))
        (Iso.inv (colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip j) :
          (J.plusObj (F.obj j)).obj (op X) ⟶ (colimit (F ⋙ J.diagramFunctor D X).flip).obj j))
⊢ CategoryStruct.comp (Y := colimit (J := (J.Cover (unop (op X)))ᵒᵖ) (J.diagram (F.obj i) (unop (op X))))
      (colimit.ι (J.diagram (F.obj i) (unop (op X))) w)
      (Iso.inv
          ((fun (k : K) ↦
              (colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k :
                (colimit (F ⋙ J.diagramFunctor D X).flip).obj k ≅
                  colimit ((F ⋙ J.diagramFunctor D X).flip ⋙ Functor.obj (evaluation K D) k)))
            i) ≫
        (colimit (F ⋙ J.diagramFunctor D X).flip).map f) =
    colimit.ι (J.diagram (F.obj i) (unop (op X))) w ≫
      (F ⋙ J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) (op X)).map f ≫
        Iso.inv
          ((fun (k : K) ↦
              (colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k :
                (colimit (F ⋙ J.diagramFunctor D X).flip).obj k ≅
                  colimit ((F ⋙ J.diagramFunctor D X).flip ⋙ Functor.obj (evaluation K D) k)))
            j)

Tactic:
dsimp [plusMap]

Premises used: CategoryTheory.GrothendieckTopology.plusMap