-- 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 t
inst_8 : SmallCategory K
inst_9 : FinCategory K
inst_10 : HasLimitsOfShape 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) X)
m :
  S.pt ⟶
    Cone.pt (F := F ⋙ J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) X)
      (Functor.mapCone (J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) X) (limit.cone F))
hm :
  ∀ (j : K),
    m ≫ NatTrans.app (Cone.π (Functor.mapCone (J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) X) (limit.cone F))) j =
      S.π.app j
k_1 : K
k : (J.Cover (unop X))ᵒᵖ
preservesLimit :
  Eq (α :=
    multiequalizer ((unop k).index (limit F)) ⟶ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (F.obj k_1) (unop X)))
    (CategoryStruct.comp (Y :=
        Cocone.pt (J := (J.Cover (unop X))ᵒᵖ) (F := J.diagram (limit F) (unop X))
          (Functor.obj (C := Cocone (J := (J.Cover (unop X))ᵒᵖ) (limit (F ⋙ J.diagramFunctor D (unop X))))
              (Cocone.precompose
                (Iso.hom
                  (IsLimit.conePointUniqueUpToIso (isLimitOfPreserves (J.diagramFunctor D (unop X)) (limit.isLimit F))
                    (limit.isLimit (F ⋙ J.diagramFunctor D (unop X))))))
              (colimit.cocone (limit (F ⋙ J.diagramFunctor D (unop X)))) :
            Cocone (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (limit F) (unop X))))
        (NatTrans.app
          (Cocone.ι
            (Functor.obj (C := Cocone (J := (J.Cover (unop X))ᵒᵖ) (limit (F ⋙ J.diagramFunctor D (unop X))))
              (Cocone.precompose
                (Iso.hom
                  (IsLimit.conePointUniqueUpToIso (isLimitOfPreserves (J.diagramFunctor D (unop X)) (limit.isLimit F))
                    (limit.isLimit (F ⋙ J.diagramFunctor D (unop X))))))
              (colimit.cocone (limit (F ⋙ J.diagramFunctor D (unop X))))))
          k)
        (CategoryStruct.comp (Y :=
          limit (colimit (J := (J.Cover (unop X))ᵒᵖ) (Functor.flip (F ⋙ J.diagramFunctor D (unop X)))))
          (Iso.hom (colimitLimitIso (F ⋙ J.diagramFunctor D (unop X))) :
            colimit (J := (J.Cover (unop X))ᵒᵖ) (limit (F ⋙ J.diagramFunctor D (unop X))) ⟶
              limit (colimit (J := (J.Cover (unop X))ᵒᵖ) (Functor.flip (F ⋙ J.diagramFunctor D (unop X)))))
          (NatTrans.app
              (Cone.π
                (Functor.obj
                  (Cone.postcompose
                    (Iso.inv
                      (Iso.symm
                        (NatIso.ofComponents
                          (fun (k : K) ↦
                            colimitObjIsoColimitCompEvaluation (Functor.flip (F ⋙ J.diagramFunctor D (unop X))) k)
                          ⋯))))
                  (limit.cone (colimit (J := (J.Cover (unop X))ᵒᵖ) (Functor.flip (F ⋙ J.diagramFunctor D (unop X)))))))
              k_1 :
            Functor.obj
                (Functor.obj (Functor.const K)
                  (Cone.pt (F := F ⋙ J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) X)
                    (Functor.obj
                      (Cone.postcompose
                        (Iso.inv
                          (Iso.symm
                            (NatIso.ofComponents
                              (fun (k : K) ↦
                                colimitObjIsoColimitCompEvaluation (Functor.flip (F ⋙ J.diagramFunctor D (unop X))) k)
                              ⋯))))
                      (limit.cone
                        (colimit (J := (J.Cover (unop X))ᵒᵖ) (Functor.flip (F ⋙ J.diagramFunctor D (unop X))))))))
                k_1 ⟶
              (F ⋙ J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) X).obj k_1)) :
      Functor.obj (J.diagram (limit F) (unop X)) k ⟶
        colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (F.obj k_1) (unop X)))
    (NatTrans.app (J.diagramNatTrans (limit.π F k_1) (unop X)) k ≫ colimit.ι (J.diagram (F.obj k_1) (unop X)) k :
      Functor.obj (J.diagram (limit F) (unop X)) k ⟶
        colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (F.obj k_1) (unop X)))
⊢ Eq (α :=
    multiequalizer ((unop k).index (limit F)) ⟶ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (F.obj k_1) (unop X)))
    (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (limit F) (unop X)))
        (colimit.ι (J.diagram (limit F) (unop X)) k :
          Functor.obj (J.diagram (limit F) (unop X)) k ⟶
            colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (limit F) (unop X)))
        (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop X))ᵒᵖ) (limit (F ⋙ J.diagramFunctor D (unop X))))
            (Iso.hom
                (HasColimit.isoOfNatIso
                  (IsLimit.conePointUniqueUpToIso (isLimitOfPreserves (J.diagramFunctor D (unop X)) (limit.isLimit F))
                    (limit.isLimit (F ⋙ J.diagramFunctor D (unop X))))) :
              colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (limit F) (unop X)) ⟶
                colimit (J := (J.Cover (unop X))ᵒᵖ) (limit (F ⋙ J.diagramFunctor D (unop X))))
            (CategoryStruct.comp (Y :=
                limit (colimit (J := (J.Cover (unop X))ᵒᵖ) (Functor.flip (F ⋙ J.diagramFunctor D (unop X)))))
                (Iso.hom (colimitLimitIso (F ⋙ J.diagramFunctor D (unop X))) :
                  colimit (J := (J.Cover (unop X))ᵒᵖ) (limit (F ⋙ J.diagramFunctor D (unop X))) ⟶
                    limit (colimit (J := (J.Cover (unop X))ᵒᵖ) (Functor.flip (F ⋙ J.diagramFunctor D (unop X)))))
                (CategoryStruct.comp (Y := limit (F ⋙ J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) X))
                    (Iso.inv
                      (HasLimit.isoOfNatIso
                        (Iso.symm
                          (NatIso.ofComponents
                            (fun (k : K) ↦
                              colimitObjIsoColimitCompEvaluation (Functor.flip (F ⋙ J.diagramFunctor D (unop X))) k)
                            ⋯))))
                    (limit.π (F ⋙ J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) X) k_1) :
                  limit (colimit (J := (J.Cover (unop X))ᵒᵖ) (Functor.flip (F ⋙ J.diagramFunctor D (unop X)))) ⟶
                    colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (F.obj k_1) (unop X))) :
              colimit (J := (J.Cover (unop X))ᵒᵖ) (limit (F ⋙ J.diagramFunctor D (unop X))) ⟶
                colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (F.obj k_1) (unop X))) :
          colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (limit F) (unop X)) ⟶
            colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (F.obj k_1) (unop X))) :
      multiequalizer ((unop k).index (limit F)) ⟶ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (F.obj k_1) (unop X)))
    (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (limit F) (unop X)))
        (colimit.ι (J.diagram (limit F) (unop X)) k) (colimMap (J.diagramNatTrans (limit.π F k_1) (unop X))) :
      multiequalizer ((unop k).index (limit F)) ⟶ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (F.obj k_1) (unop X)))

Tactic:
erw [colimit.ι_map, colimit.ι_desc_assoc, limit.lift_π]

Premises used: CategoryTheory.Limits.colimit.ι_map, CategoryTheory.Limits.colimit.ι_desc_assoc, CategoryTheory.Limits.limit.lift_π