-- Module: Mathlib.CategoryTheory.Sites.CompatiblePlus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
F : Functor.{v_1, v_2, u_1, u_2} D E
inst_3 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst_4 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst_5 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D), PreservesLimit (W.index P).multicospan F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ D
inst_6 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_7 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst_8 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (J.Cover (unop X))ᵒᵖ
slice_lhs :
  Eq (α := F.obj (multiequalizer ((unop W).index P)) ⟶ colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram (P ⋙ F) (unop Y)))
    (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram P (unop Y) ⋙ F))
        (CategoryStruct.comp (Y := F.obj (colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram P (unop Y))))
            (CategoryStruct.comp (Y := F.obj (multiequalizer (((unop W).pullback f.unop).index P)))
              (F.map
                (Multiequalizer.lift (((unop W).pullback f.unop).index P) (multiequalizer ((unop W).index P))
                  (fun (I : ((unop W).pullback f.unop).Arrow) ↦ Multiequalizer.ι ((unop W).index P) I.base) ⋯))
              (F.map (colimit.ι (J.diagram P (unop Y)) (op ((unop W).pullback f.unop)))))
            (Iso.hom
              (IsColimit.coconePointUniqueUpToIso (isColimitOfPreserves F (colimit.isColimit (J.diagram P (unop Y))))
                (colimit.isColimit (J.diagram P (unop Y) ⋙ F)))) :
          F.obj (multiequalizer ((unop W).index P)) ⟶ colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram P (unop Y) ⋙ F))
        (Iso.hom (HasColimit.isoOfNatIso (J.diagramCompIso F P (unop Y))) :
          colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram P (unop Y) ⋙ F) ⟶
            colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram (P ⋙ F) (unop Y))) :
      F.obj (multiequalizer ((unop W).index P)) ⟶ colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram (P ⋙ F) (unop Y)))
    (CategoryStruct.comp (Y := colimit ((J.pullback f.unop).op ⋙ J.diagram (P ⋙ F) (unop Y)))
        (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (P ⋙ F) (unop X)))
            (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X) ⋙ F))
                (NatTrans.app (Cocone.ι (colimit.cocone (J.diagram P (unop X) ⋙ F))) W :
                  obj (J.diagram P (unop X) ⋙ F) W ⟶
                    obj
                      (obj (const (J.Cover (unop X))ᵒᵖ)
                        (Cocone.pt (J := (J.Cover (unop X))ᵒᵖ) (F := J.diagram P (unop X) ⋙ F)
                          (colimit.cocone (J.diagram P (unop X) ⋙ F))))
                      W)
                (Iso.hom (HasColimit.isoOfNatIso (J.diagramCompIso F P (unop X))) :
                  colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X) ⋙ F) ⟶
                    colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (P ⋙ F) (unop X))) :
              F.obj (multiequalizer ((unop W).index P)) ⟶
                colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (P ⋙ F) (unop X)))
            (colimMap (J.diagramPullback (P ⋙ F) f.unop) :
              colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (P ⋙ F) (unop X)) ⟶
                colimit ((J.pullback f.unop).op ⋙ J.diagram (P ⋙ F) (unop Y))) :
          F.obj (multiequalizer ((unop W).index P)) ⟶ colimit ((J.pullback f.unop).op ⋙ J.diagram (P ⋙ F) (unop Y)))
        (colimit.pre (J.diagram (P ⋙ F) (unop Y)) (J.pullback f.unop).op :
          colimit ((J.pullback f.unop).op ⋙ J.diagram (P ⋙ F) (unop Y)) ⟶
            colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram (P ⋙ F) (unop Y))) :
      F.obj (multiequalizer ((unop W).index P)) ⟶ colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram (P ⋙ F) (unop Y)))
⊢ Eq (α := F.obj (multiequalizer ((unop W).index P)) ⟶ colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram (P ⋙ F) (unop Y)))
    (CategoryStruct.comp (Y := F.obj (colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X))))
        (F.map (colimit.ι (J.diagram P (unop X)) W) :
          F.obj (multiequalizer ((unop W).index P)) ⟶
            F.obj (colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X))))
        (CategoryStruct.comp (Y := F.obj (colimit ((J.pullback f.unop).op ⋙ J.diagram P (unop Y))))
            (F.map (colimMap (J.diagramPullback P f.unop)))
            (CategoryStruct.comp (Y := F.obj (colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram P (unop Y))))
              (F.map (colimit.pre (J.diagram P (unop Y)) (J.pullback f.unop).op))
              (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram P (unop Y) ⋙ F))
                (Iso.hom
                  (IsColimit.coconePointUniqueUpToIso
                    (isColimitOfPreserves F (colimit.isColimit (J.diagram P (unop Y))))
                    (colimit.isColimit (J.diagram P (unop Y) ⋙ F))))
                (Iso.hom (HasColimit.isoOfNatIso (J.diagramCompIso F P (unop Y)))))) :
          F.obj (colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X))) ⟶
            colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram (P ⋙ F) (unop Y))) :
      F.obj (multiequalizer ((unop W).index P)) ⟶ colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram (P ⋙ F) (unop Y)))
    (CategoryStruct.comp (Y := colimit ((J.pullback f.unop).op ⋙ J.diagram (P ⋙ F) (unop Y)))
        (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (P ⋙ F) (unop X)))
            (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X) ⋙ F))
                (NatTrans.app (Cocone.ι (colimit.cocone (J.diagram P (unop X) ⋙ F))) W :
                  obj (J.diagram P (unop X) ⋙ F) W ⟶
                    obj
                      (obj (const (J.Cover (unop X))ᵒᵖ)
                        (Cocone.pt (J := (J.Cover (unop X))ᵒᵖ) (F := J.diagram P (unop X) ⋙ F)
                          (colimit.cocone (J.diagram P (unop X) ⋙ F))))
                      W)
                (Iso.hom (HasColimit.isoOfNatIso (J.diagramCompIso F P (unop X))) :
                  colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X) ⋙ F) ⟶
                    colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (P ⋙ F) (unop X))) :
              F.obj (multiequalizer ((unop W).index P)) ⟶
                colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (P ⋙ F) (unop X)))
            (colimMap (J.diagramPullback (P ⋙ F) f.unop) :
              colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (P ⋙ F) (unop X)) ⟶
                colimit ((J.pullback f.unop).op ⋙ J.diagram (P ⋙ F) (unop Y))) :
          F.obj (multiequalizer ((unop W).index P)) ⟶ colimit ((J.pullback f.unop).op ⋙ J.diagram (P ⋙ F) (unop Y)))
        (colimit.pre (J.diagram (P ⋙ F) (unop Y)) (J.pullback f.unop).op :
          colimit ((J.pullback f.unop).op ⋙ J.diagram (P ⋙ F) (unop Y)) ⟶
            colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram (P ⋙ F) (unop Y))) :
      F.obj (multiequalizer ((unop W).index P)) ⟶ colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram (P ⋙ F) (unop Y)))

Tactic:
slice_lhs 1 3 =>
        simp only [← F.map_comp]
        dsimp [colimMap, IsColimit.map, colimit.pre]
        simp only [colimit.ι_desc_assoc, colimit.ι_desc]
        dsimp [Cocone.precompose]
        simp only [Category.assoc, colimit.ι_desc]
        dsimp [Cocone.whisker]
        rw [F.map_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Cocone.precompose, CategoryTheory.Limits.Cocone.whisker, CategoryTheory.Limits.colimit.ι_desc, CategoryTheory.Limits.colimit.ι_desc_assoc, CategoryTheory.Limits.colimMap, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.colimit.pre, CategoryTheory.Limits.IsColimit.map