∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{t, w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  {X : C} {K : Type s} [inst_3 : CategoryTheory.SmallCategory K] [inst_4 : CategoryTheory.Limits.HasLimitsOfShape K D]
  {W : (J.Cover X)ᵒᵖ} (F : CategoryTheory.Functor K (CategoryTheory.Functor Cᵒᵖ D))
  (E :
    CategoryTheory.Limits.Cone
      (F.comp ((J.diagramFunctor D X).comp ((CategoryTheory.evaluation (J.Cover X)ᵒᵖ D).obj W))))
  (i : (Opposite.unop W).Arrow) (k : K) {Z : D} (h : (F.obj k).obj (Opposite.op i.Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.liftToDiagramLimitObjAux F E i)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.limit.π F k).app (Opposite.op i.Y)) h) =
    CategoryTheory.CategoryStruct.comp (E.π.app k)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι ((Opposite.unop W).index (F.obj k)) i)
        h)