-- 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 : Cᵒᵖ
w :
  Eq (α := F.obj (P.obj x) ⟶ (J.plusObj (P ⋙ F)).obj x)
    (CategoryStruct.comp (Y :=
        F.obj (multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ P)))
        (F.map (Cover.toMultiequalizer ⊤ P) :
          F.obj (P.obj x) ⟶
            F.obj (multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ P)))
        (CategoryStruct.comp (Y := obj (C := (J.Cover (unop x))ᵒᵖ) (J.diagram (P ⋙ F) (unop x)) (op ⊤))
            (NatTrans.app (Iso.hom (J.diagramCompIso F P (unop x))) (op ⊤) :
              obj (C := (J.Cover (unop x))ᵒᵖ) (J.diagram P (unop x) ⋙ F) (op ⊤) ⟶
                obj (C := (J.Cover (unop x))ᵒᵖ) (J.diagram (P ⋙ F) (unop x)) (op ⊤))
            (colimit.ι (J.diagram (P ⋙ F) (unop x)) (op ⊤) :
              obj (C := (J.Cover (unop x))ᵒᵖ) (J.diagram (P ⋙ F) (unop x)) (op ⊤) ⟶
                colimit (J := (J.Cover (unop x))ᵒᵖ) (J.diagram (P ⋙ F) (unop x))) :
          obj (C := (J.Cover (unop x))ᵒᵖ) (J.diagram P (unop x) ⋙ F) (op ⊤) ⟶
            colimit (J := (J.Cover (unop x))ᵒᵖ) (J.diagram (P ⋙ F) (unop x))) :
      F.obj (P.obj x) ⟶ (J.plusObj (P ⋙ F)).obj x)
    (CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ (P ⋙ F)))
        (Cover.toMultiequalizer ⊤ (P ⋙ F)) (colimit.ι (J.diagram (P ⋙ F) (unop x)) (op ⊤)) :
      F.obj (P.obj x) ⟶ (J.plusObj (P ⋙ F)).obj x)
⊢ Eq (α := F.obj (P.obj x) ⟶ (J.plusObj (P ⋙ F)).obj x)
    (CategoryStruct.comp (Y := F.obj ((J.plusObj P).obj x))
        (F.map
            (CategoryStruct.comp (Y :=
              multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ P))
              (Cover.toMultiequalizer ⊤ P) (colimit.ι (J.diagram P (unop x)) (op ⊤))) :
          F.obj (P.obj x) ⟶ F.obj ((J.plusObj P).obj x))
        (NatTrans.app (Iso.hom (J.plusCompIso F P)) x : (J.plusObj P ⋙ F).obj x ⟶ (J.plusObj (P ⋙ F)).obj x) :
      F.obj (P.obj x) ⟶ (J.plusObj (P ⋙ F)).obj x)
    (CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ (P ⋙ F)))
        (Cover.toMultiequalizer ⊤ (P ⋙ F)) (colimit.ι (J.diagram (P ⋙ F) (unop x)) (op ⊤)) :
      F.obj (P.obj x) ⟶ (J.plusObj (P ⋙ F)).obj x)

Tactic:
simp only [ι_plusCompIso_hom, Functor.map_comp, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp, CategoryTheory.GrothendieckTopology.ι_plusCompIso_hom