∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X Y : C}
  (f : Y ⟶ X) (X_1 : CategoryTheory.Over X),
  ((CategoryTheory.toOverIteratedSliceForwardIsoPullback f).inv.app X_1).left =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Over.mk f).iteratedSliceEquiv.counitInv.app
          ((CategoryTheory.ChosenPullbacksAlong.pullback f).obj X_1)).left
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.ChosenPullbacksAlong.lift
          (CategoryTheory.CategoryStruct.id ((CategoryTheory.ChosenPullbacksAlong.pullback f).obj X_1).left)
          ((CategoryTheory.ChosenPullbacksAlong.pullback f).obj X_1).hom ⋯)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight
              (CategoryTheory.CategoryStruct.id
                ((CategoryTheory.Over.map f).obj ((CategoryTheory.ChosenPullbacksAlong.pullback f).obj X_1)))
              (CategoryTheory.Over.mk f)).left
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight
              ((CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj f).counit.app X_1) (CategoryTheory.Over.mk f)).left))