-- 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
apply :
  ∀ (j : (J.Cover (unop X))ᵒᵖ),
    Eq (α := obj (J.diagram P (unop X) ⋙ F) j ⟶ (J.plusObj (P ⋙ F)).obj Y)
      (CategoryStruct.comp (Y :=
        obj
          (obj (const (J.Cover (unop X))ᵒᵖ)
            (Cocone.pt (J := (J.Cover (unop X))ᵒᵖ) (F := J.diagram P (unop X) ⋙ F)
              (F.mapCocone (colimit.cocone (J.diagram P (unop X))))))
          j)
        (NatTrans.app (Cocone.ι (F.mapCocone (colimit.cocone (J.diagram P (unop X))))) j)
        ((J.plusObj P ⋙ F).map f ≫
          Iso.hom
            ((fun (X : Cᵒᵖ) ↦
                (Iso.trans (Y := colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X) ⋙ F))
                    (IsColimit.coconePointUniqueUpToIso
                      (isColimitOfPreserves F (colimit.isColimit (J.diagram P (unop X))))
                      (colimit.isColimit (J.diagram P (unop X) ⋙ F)))
                    (HasColimit.isoOfNatIso (J.diagramCompIso F P (unop X))) :
                  (J.plusObj P ⋙ F).obj X ≅ (J.plusObj (P ⋙ F)).obj X))
              Y)))
      (CategoryStruct.comp (Y :=
        obj
          (obj (const (J.Cover (unop X))ᵒᵖ)
            (Cocone.pt (J := (J.Cover (unop X))ᵒᵖ) (F := J.diagram P (unop X) ⋙ F)
              (F.mapCocone (colimit.cocone (J.diagram P (unop X))))))
          j)
        (NatTrans.app (Cocone.ι (F.mapCocone (colimit.cocone (J.diagram P (unop X))))) j)
        (Iso.hom
            ((fun (X : Cᵒᵖ) ↦
                (Iso.trans (Y := colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X) ⋙ F))
                    (IsColimit.coconePointUniqueUpToIso
                      (isColimitOfPreserves F (colimit.isColimit (J.diagram P (unop X))))
                      (colimit.isColimit (J.diagram P (unop X) ⋙ F)))
                    (HasColimit.isoOfNatIso (J.diagramCompIso F P (unop X))) :
                  (J.plusObj P ⋙ F).obj X ≅ (J.plusObj (P ⋙ F)).obj X))
              X) ≫
          (J.plusObj (P ⋙ F)).map f))
⊢ (J.plusObj P ⋙ F).map f ≫
      Iso.hom
        ((fun (X : Cᵒᵖ) ↦
            (Iso.trans (Y := colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X) ⋙ F))
                (IsColimit.coconePointUniqueUpToIso (isColimitOfPreserves F (colimit.isColimit (J.diagram P (unop X))))
                  (colimit.isColimit (J.diagram P (unop X) ⋙ F)))
                (HasColimit.isoOfNatIso (J.diagramCompIso F P (unop X))) :
              (J.plusObj P ⋙ F).obj X ≅ (J.plusObj (P ⋙ F)).obj X))
          Y) =
    Iso.hom
        ((fun (X : Cᵒᵖ) ↦
            (Iso.trans (Y := colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X) ⋙ F))
                (IsColimit.coconePointUniqueUpToIso (isColimitOfPreserves F (colimit.isColimit (J.diagram P (unop X))))
                  (colimit.isColimit (J.diagram P (unop X) ⋙ F)))
                (HasColimit.isoOfNatIso (J.diagramCompIso F P (unop X))) :
              (J.plusObj P ⋙ F).obj X ≅ (J.plusObj (P ⋙ F)).obj X))
          X) ≫
      (J.plusObj (P ⋙ F)).map f

Tactic:
apply (isColimitOfPreserves F (colimit.isColimit (J.diagram P X.unop))).hom_ext

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.Limits.colimit.isColimit, Opposite.unop, CategoryTheory.Limits.isColimitOfPreserves, CategoryTheory.GrothendieckTopology.diagram