∀ {T : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} T] {X : T} (f : CategoryTheory.Over X)
  (X_1 : CategoryTheory.Over f),
  CategoryTheory.CategoryStruct.comp
      (f.iteratedSliceForward.map
        ((CategoryTheory.NatIso.ofComponents
                (fun g =>
                  CategoryTheory.Over.isoMk
                    (CategoryTheory.Over.isoMk
                      (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Over f)).obj g).left.left) ⋯)
                    ⋯)
                ⋯).hom.app
          X_1))
      ((CategoryTheory.NatIso.ofComponents
              (fun g =>
                CategoryTheory.Over.isoMk
                  (CategoryTheory.Iso.refl ((f.iteratedSliceBackward.comp f.iteratedSliceForward).obj g).left) ⋯)
              ⋯).hom.app
        (f.iteratedSliceForward.obj X_1)) =
    CategoryTheory.CategoryStruct.id (f.iteratedSliceForward.obj X_1)