-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
S : (J.Cover (unop X))ᵒᵖ
simp :
  Eq (α := multiequalizer ((unop S).index P) ⟶ colimit (J := (J.Cover (unop Z))ᵒᵖ) (J.diagram P (unop Z)))
    (CategoryStruct.comp (Y := ((J.pullback (g.unop ≫ f.unop)).op ⋙ J.diagram P (unop Z)).obj S)
      (Multiequalizer.lift ((unop ((J.pullback (g.unop ≫ f.unop)).op.obj S)).index P)
        (Functor.obj (J.diagram P (unop X)) S)
        (fun (I : (unop ((J.pullback (g.unop ≫ f.unop)).op.obj S)).shape.L) ↦
          Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I))
        ⋯)
      (colimit.ι (J.diagram P (unop Z)) ((J.pullback (g.unop ≫ f.unop)).op.obj S)))
    (CategoryStruct.comp (Y := ((J.pullback f.unop).op ⋙ J.diagram P (unop Y)).obj S)
      (Multiequalizer.lift ((unop ((J.pullback f.unop).op.obj S)).index P) (Functor.obj (J.diagram P (unop X)) S)
        (fun (I : (unop ((J.pullback f.unop).op.obj S)).shape.L) ↦
          Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I))
        ⋯)
      (CategoryStruct.comp (Y := ((J.pullback g.unop).op ⋙ J.diagram P (unop Z)).obj ((J.pullback f.unop).op.obj S))
        (Multiequalizer.lift ((unop ((J.pullback g.unop).op.obj ((J.pullback f.unop).op.obj S))).index P)
          (Functor.obj (J.diagram P (unop Y)) ((J.pullback f.unop).op.obj S))
          (fun (I : (unop ((J.pullback g.unop).op.obj ((J.pullback f.unop).op.obj S))).shape.L) ↦
            Multiequalizer.ι ((unop ((J.pullback f.unop).op.obj S)).index P) (Cover.Arrow.base I))
          ⋯)
        (colimit.ι (J.diagram P (unop Z)) ((J.pullback g.unop).op.obj ((J.pullback f.unop).op.obj S)))))
⊢ Eq (α := multiequalizer ((unop S).index P) ⟶ colimit (J := (J.Cover (unop Z))ᵒᵖ) (J.diagram P (unop Z)))
    (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)))
      (colimit.ι (J.diagram P (unop X)) S)
      (CategoryStruct.comp (Y := colimit ((J.pullback (g.unop ≫ f.unop)).op ⋙ J.diagram P (unop Z)))
        (colimMap (J.diagramPullback P (g.unop ≫ f.unop)))
        (colimit.pre (J.diagram P (unop Z)) (J.pullback (g.unop ≫ f.unop)).op)))
    (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)))
      (colimit.ι (J.diagram P (unop X)) S)
      (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram P (unop 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))
        (CategoryStruct.comp (Y := colimit ((J.pullback g.unop).op ⋙ J.diagram P (unop Z)))
          (colimMap (J.diagramPullback P g.unop)) (colimit.pre (J.diagram P (unop Z)) (J.pullback g.unop).op))))

Tactic:
simp only [diagramPullback_app, colimit.ι_pre_assoc, colimit.ι_pre, ι_colimMap_assoc,
      Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.colimit.ι_pre_assoc, CategoryTheory.Limits.ι_colimMap_assoc, CategoryTheory.Limits.colimit.ι_pre, CategoryTheory.GrothendieckTopology.diagramPullback_app