∀ {T : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} T] {X : T} {f g : CategoryTheory.Over X} (p : f ⟶ g)
  {X_1 Y : CategoryTheory.Over f} (f_1 : X_1 ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      ((f.iteratedSliceForward.comp ((CategoryTheory.Over.map p.left).comp g.iteratedSliceBackward)).map f_1)
      ((fun h =>
            CategoryTheory.Over.isoMk
              (CategoryTheory.Over.isoMk
                (CategoryTheory.Iso.refl
                  ((f.iteratedSliceForward.comp ((CategoryTheory.Over.map p.left).comp g.iteratedSliceBackward)).obj
                        h).left.left)
                ⋯)
              ⋯)
          Y).hom =
    CategoryTheory.CategoryStruct.comp
      ((fun h =>
            CategoryTheory.Over.isoMk
              (CategoryTheory.Over.isoMk
                (CategoryTheory.Iso.refl
                  ((f.iteratedSliceForward.comp ((CategoryTheory.Over.map p.left).comp g.iteratedSliceBackward)).obj
                        h).left.left)
                ⋯)
              ⋯)
          X_1).hom
      ((CategoryTheory.Over.map p).map f_1)