∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {J : CategoryTheory.GrothendieckTopology C}
  {D : Type u_4} [inst_1 : CategoryTheory.Category.{u_3, u_4} D] {K : Type u_6}
  [inst_2 : CategoryTheory.Category.{u_5, u_6} K] [inst_3 : CategoryTheory.Limits.HasLimitsOfShape K D]
  (F : CategoryTheory.Functor K (CategoryTheory.Sheaf J D))
  (E : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.sheafToPresheaf J D))) (hE : CategoryTheory.Limits.IsLimit E)
  (X : C) (W : J.Cover X) (E_1 : CategoryTheory.Limits.Multifork (W.index E.pt)) (i : W.shape.L),
  CategoryTheory.CategoryStruct.comp
      ((fun S =>
          (CategoryTheory.Limits.isLimitOfPreserves ((CategoryTheory.evaluation Cᵒᵖ D).obj (Opposite.op X)) hE).lift
            (CategoryTheory.Sheaf.multiforkEvaluationCone F E X W S))
        E_1)
      ((W.multifork E.pt).ι i) =
    E_1.ι i