-- 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
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
P Q : Functor.{v, v_1, u, u_1} Cᵒᵖ D
η : P ⟶ Q
X : Cᵒᵖ
W : (J.Cover (unop X))ᵒᵖ
w :
  Eq (α := F.obj (multiequalizer ((unop W).index P)) ⟶ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (Q ⋙ F) (unop X)))
    (CategoryStruct.comp (Y := F.obj (colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram Q (unop X))))
        (F.map
            (NatTrans.app
              (Cocone.ι
                (obj (Cocone.precompose (J.diagramNatTrans η (unop X))) (colimit.cocone (J.diagram Q (unop X)))))
              W) :
          F.obj (multiequalizer ((unop W).index P)) ⟶
            F.obj (colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram Q (unop X))))
        (NatTrans.app (Iso.hom (J.plusCompIso F Q)) X :
          obj.{v, v_2, u, u_2}
              ({ obj := fun (X : Cᵒᵖ) ↦ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram Q (unop X)),
                  map := fun {X Y : Cᵒᵖ} (f : X ⟶ Y) ↦
                    colimit.desc (J.diagram Q (unop X))
                        (obj (Cocone.precompose (J.diagramPullback Q f.unop))
                          (colimit.cocone ((J.pullback f.unop).op ⋙ J.diagram Q (unop Y)))) ≫
                      colimit.pre (J.diagram Q (unop Y)) (J.pullback f.unop).op,
                  map_id := ⋯, map_comp := ⋯ : Functor.{v, v_1, u, u_1} Cᵒᵖ D } ⋙
                F)
              X ⟶
            obj.{v, v_2, u, u_2}
              { obj := fun (X : Cᵒᵖ) ↦ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (Q ⋙ F) (unop X)),
                map := fun {X Y : Cᵒᵖ} (f : X ⟶ Y) ↦
                  colimit.desc (J.diagram (Q ⋙ F) (unop X))
                      (obj (Cocone.precompose (J.diagramPullback (Q ⋙ F) f.unop))
                        (colimit.cocone ((J.pullback f.unop).op ⋙ J.diagram (Q ⋙ F) (unop Y)))) ≫
                    colimit.pre (J.diagram (Q ⋙ F) (unop Y)) (J.pullback f.unop).op,
                map_id := ⋯, map_comp := ⋯ }
              X) :
      F.obj (multiequalizer ((unop W).index P)) ⟶ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (Q ⋙ F) (unop X)))
    (CategoryStruct.comp (Y := multiequalizer ((unop W).index (Q ⋙ F)))
        (CategoryStruct.comp (Y := multiequalizer ((unop W).index (P ⋙ F)))
          (NatTrans.app (Iso.hom (J.diagramCompIso F P (unop X))) W :
            obj (J.diagram P (unop X) ⋙ F) W ⟶ obj (J.diagram (P ⋙ F) (unop X)) W)
          (Multiequalizer.lift ((unop W).index (Q ⋙ F)) (multiequalizer ((unop W).index (P ⋙ F)))
              (fun (x : (unop W).Arrow) ↦ Multiequalizer.ι ((unop W).index (P ⋙ F)) x ≫ F.map (η.app (op x.Y))) ⋯ :
            multiequalizer ((unop W).index (P ⋙ F)) ⟶ multiequalizer ((unop W).index (Q ⋙ F))))
        (colimit.ι (J.diagram (Q ⋙ F) (unop X)) W) :
      F.obj (multiequalizer ((unop W).index P)) ⟶ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (Q ⋙ F) (unop X)))
⊢ Eq (α := F.obj (multiequalizer ((unop W).index P)) ⟶ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (Q ⋙ F) (unop X)))
    (CategoryStruct.comp (Y := F.obj (colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram Q (unop X))))
        (F.map
            (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)))
              (colimit.ι (J.diagram P (unop X)) W)
              (colimit.desc (J.diagram P (unop X))
                (obj (Cocone.precompose (J.diagramNatTrans η (unop X))) (colimit.cocone (J.diagram Q (unop X)))))) :
          F.obj (multiequalizer ((unop W).index P)) ⟶
            F.obj (colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram Q (unop X))))
        (NatTrans.app (Iso.hom (J.plusCompIso F Q)) X :
          obj.{v, v_2, u, u_2}
              ({ obj := fun (X : Cᵒᵖ) ↦ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram Q (unop X)),
                  map := fun {X Y : Cᵒᵖ} (f : X ⟶ Y) ↦
                    colimit.desc (J.diagram Q (unop X))
                        (obj (Cocone.precompose (J.diagramPullback Q f.unop))
                          (colimit.cocone ((J.pullback f.unop).op ⋙ J.diagram Q (unop Y)))) ≫
                      colimit.pre (J.diagram Q (unop Y)) (J.pullback f.unop).op,
                  map_id := ⋯, map_comp := ⋯ : Functor.{v, v_1, u, u_1} Cᵒᵖ D } ⋙
                F)
              X ⟶
            obj.{v, v_2, u, u_2}
              { obj := fun (X : Cᵒᵖ) ↦ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (Q ⋙ F) (unop X)),
                map := fun {X Y : Cᵒᵖ} (f : X ⟶ Y) ↦
                  colimit.desc (J.diagram (Q ⋙ F) (unop X))
                      (obj (Cocone.precompose (J.diagramPullback (Q ⋙ F) f.unop))
                        (colimit.cocone ((J.pullback f.unop).op ⋙ J.diagram (Q ⋙ F) (unop Y)))) ≫
                    colimit.pre (J.diagram (Q ⋙ F) (unop Y)) (J.pullback f.unop).op,
                map_id := ⋯, map_comp := ⋯ }
              X) :
      F.obj (multiequalizer ((unop W).index P)) ⟶ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (Q ⋙ F) (unop X)))
    (CategoryStruct.comp (Y := multiequalizer ((unop W).index (Q ⋙ F)))
        (CategoryStruct.comp (Y := multiequalizer ((unop W).index (P ⋙ F)))
          (NatTrans.app (Iso.hom (J.diagramCompIso F P (unop X))) W :
            obj (J.diagram P (unop X) ⋙ F) W ⟶ obj (J.diagram (P ⋙ F) (unop X)) W)
          (Multiequalizer.lift ((unop W).index (Q ⋙ F)) (multiequalizer ((unop W).index (P ⋙ F)))
              (fun (x : (unop W).Arrow) ↦ Multiequalizer.ι ((unop W).index (P ⋙ F)) x ≫ F.map (η.app (op x.Y))) ⋯ :
            multiequalizer ((unop W).index (P ⋙ F)) ⟶ multiequalizer ((unop W).index (Q ⋙ F))))
        (colimit.ι (J.diagram (Q ⋙ F) (unop X)) W) :
      F.obj (multiequalizer ((unop W).index P)) ⟶ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (Q ⋙ F) (unop X)))

Tactic:
simp only [colimit.ι_desc]

Premises used: CategoryTheory.Limits.colimit.ι_desc