∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D] {K : Type z} [inst_2 : CategoryTheory.Category.{z', z} K]
  [inst_3 : CategoryTheory.HasWeakSheafify J D] {F : CategoryTheory.Functor K (CategoryTheory.Sheaf J D)}
  (E : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.sheafToPresheaf J D))) (k : K)
  {Z : CategoryTheory.Functor Cᵒᵖ D}
  (h : (((CategoryTheory.Functor.const K).obj (CategoryTheory.Sheaf.sheafifyCocone E).pt).obj k).val ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Sheaf.sheafifyCocone E).ι.app k).val h =
    CategoryTheory.CategoryStruct.comp (E.ι.app k)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J E.pt) h)