∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] (J : CategoryTheory.GrothendieckTopology C)
  (F : CategoryTheory.Functor Cᵒᵖ (Type (max u_1 u_2))),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Subfunctor.sheafify J (CategoryTheory.Subfunctor.range (J.toSheafify F))).ι
      (J.sheafifyLift (CategoryTheory.Subfunctor.toRangeSheafify J (J.toSheafify F)) ⋯) =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.Subfunctor.sheafify J (CategoryTheory.Subfunctor.range (J.toSheafify F))).toFunctor