∀ {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] (Y_1 : CategoryTheory.Over Y),
  CategoryTheory.CategoryStruct.comp
      ({
            app := fun Q =>
              CategoryTheory.Over.homMk
                (CategoryTheory.ChosenPullbacksAlong.lift
                  (CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id C).obj Q.left))
                  (CategoryTheory.CategoryStruct.comp Q.hom (CategoryTheory.ChosenPullbacksAlong.snd f g)) ⋯)
                ⋯,
            naturality := ⋯ }.app
        ({
              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 := ⋯ }.obj
          Y_1))
      ({
            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 := ⋯ }.map
        ({
              app := fun W =>
                CategoryTheory.Over.homMk
                  (CategoryTheory.ChosenPullbacksAlong.fst (CategoryTheory.CategoryStruct.comp W.hom f) g) ⋯,
              naturality := ⋯ }.app
          Y_1)) =
    CategoryTheory.CategoryStruct.id
      ({
            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 := ⋯ }.obj
        Y_1)