∀ (J : Type u_2) [inst : CategoryTheory.Category.{u_1, u_2} J] (C : Type u_4)
  [inst_1 : CategoryTheory.Category.{u_3, u_4} C]
  [inst_2 : ∀ (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)), CategoryTheory.Limits.HasEnd F]
  (X : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)),
  CategoryTheory.Limits.end_.map (CategoryTheory.CategoryStruct.id X) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.end_ X)