-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CompatiblePlus (goal)
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
inst_3 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst_4 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst_5 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_6 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
F G : Functor.{v_1, v_2, u_1, u_2} D E
η : F ⟶ G
P : Functor.{v, v_1, u, u_1} Cᵒᵖ D
inst_7 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst_8 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D), PreservesLimit (W.index P).multicospan F
inst_9 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ G
inst_10 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D), PreservesLimit (W.index P).multicospan G
X : Cᵒᵖ
W : (J.Cover (unop X))ᵒᵖ
⊢ Eq (α := obj (J.diagram P (unop X) ⋙ F) W ⟶ (J.plusObj (P ⋙ G)).obj X)
    (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))))))
        W)
      (NatTrans.app (Cocone.ι (F.mapCocone (colimit.cocone (J.diagram P (unop X))))) W)
      (NatTrans.app ((J.plusObj P).whiskerLeft η ≫ Iso.hom (J.plusCompIso G P)) X))
    (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))))))
        W)
      (NatTrans.app (Cocone.ι (F.mapCocone (colimit.cocone (J.diagram P (unop X))))) W)
      (NatTrans.app
        (CategoryStruct.comp (Y := J.plusObj (P ⋙ F))
          (Iso.hom (J.plusCompIso F P) : J.plusObj P ⋙ F ⟶ J.plusObj (P ⋙ F))
          (J.plusMap (P.whiskerLeft η) : J.plusObj (P ⋙ F) ⟶ J.plusObj (P ⋙ G)))
        X))
have w : Eq (α := F.obj (multiequalizer ((unop W).index P)) ⟶ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (P ⋙ G) (unop X)))
  (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))))
      (η.app (colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X))) ≫
          NatTrans.app (Iso.hom (J.plusCompIso G P)) X :
        F.obj (colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X))) ⟶
          colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (P ⋙ G) (unop X))) :
    F.obj (multiequalizer ((unop W).index P)) ⟶ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (P ⋙ G) (unop X)))
  (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 := colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (P ⋙ F) (unop X)))
          (NatTrans.app (Iso.hom (J.plusCompIso F P)) X :
            obj.{v, v_2, u, u_2}
                ({ obj := fun (X : Cᵒᵖ) ↦ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)),
                    map := fun {X Y : Cᵒᵖ} (f : X ⟶ Y) ↦
                      CategoryStruct.comp (Y := colimit ((J.pullback f.unop).op ⋙ J.diagram P (unop Y)))
                        (colimMap (J.diagramPullback P f.unop))
                        (colimit.pre (J.diagram P (unop Y)) (J.pullback f.unop).op),
                    map_id := sorry, map_comp := sorry : 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 (P ⋙ F) (unop X)),
                  map := fun {X Y : Cᵒᵖ} (f : X ⟶ Y) ↦
                    CategoryStruct.comp (Y := colimit ((J.pullback f.unop).op ⋙ J.diagram (P ⋙ F) (unop Y)))
                      (colimMap (J.diagramPullback (P ⋙ F) f.unop))
                      (colimit.pre (J.diagram (P ⋙ F) (unop Y)) (J.pullback f.unop).op),
                  map_id := sorry, map_comp := sorry }
                X)
          (colimMap (J.diagramNatTrans (P.whiskerLeft η) (unop X)) :
            colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (P ⋙ F) (unop X)) ⟶
              colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (P ⋙ G) (unop X))) :
        F.obj (colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X))) ⟶
          colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (P ⋙ G) (unop X))) :
    F.obj (multiequalizer ((unop W).index P)) ⟶ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (P ⋙ G) (unop X)))
Tactic: dsimp [plusObj, plusMap]