∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] [inst_1 : CategoryTheory.Abelian C] {X : C}
  {J : Type u_1} [inst_2 : CategoryTheory.SmallCategory J] {Y : CategoryTheory.Functor J C} {j₀ : J} (y : X ⟶ Y.obj j₀)
  {X_1 Y_1 Z : CategoryTheory.Under j₀} (f : X_1 ⟶ Y_1) (g : Y_1 ⟶ Z),
  CategoryTheory.MonoOver.homMk
      ((CategoryTheory.Limits.kernel (CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.g y)).map
        (CategoryTheory.CategoryStruct.comp f g))
      ⋯ =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoOver.homMk
        ((CategoryTheory.Limits.kernel (CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.g y)).map f) ⋯)
      (CategoryTheory.MonoOver.homMk
        ((CategoryTheory.Limits.kernel (CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.g y)).map g) ⋯)