∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {Y Z X : C} (f : Y ⟶ X) (g : Z ⟶ X)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong g] ⦃X_1 Y_1 : CategoryTheory.Over Y⦄ (f_1 : X_1 ⟶ Y_1),
  CategoryTheory.CategoryStruct.comp
      (({
                obj := fun W =>
                  CategoryTheory.Over.mk
                    (CategoryTheory.ChosenPullbacksAlong.pullbackMap f g (CategoryTheory.CategoryStruct.comp W.hom f) g
                      W.hom (CategoryTheory.CategoryStruct.id Z) (CategoryTheory.CategoryStruct.id X) ⋯ ⋯),
                map := fun {W' W} k =>
                  CategoryTheory.Over.homMk
                    (CategoryTheory.ChosenPullbacksAlong.lift
                      (CategoryTheory.CategoryStruct.comp
                        (CategoryTheory.ChosenPullbacksAlong.fst (CategoryTheory.CategoryStruct.comp W'.hom f) g)
                        k.left)
                      (CategoryTheory.ChosenPullbacksAlong.snd (CategoryTheory.CategoryStruct.comp W'.hom f) g) ⋯)
                    ⋯,
                map_id := ⋯, map_comp := ⋯ }.comp
            (CategoryTheory.Over.map (CategoryTheory.ChosenPullbacksAlong.fst f g))).map
        f_1)
      (CategoryTheory.Over.homMk
        (CategoryTheory.ChosenPullbacksAlong.fst (CategoryTheory.CategoryStruct.comp Y_1.hom f) g) ⋯) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.homMk
        (CategoryTheory.ChosenPullbacksAlong.fst (CategoryTheory.CategoryStruct.comp X_1.hom f) g) ⋯)
      ((CategoryTheory.Functor.id (CategoryTheory.Over Y)).map f_1)