∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {X : C} [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {S T : C} (f : X ⟶ T) (i : T ⟶ S),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp f
        (CategoryTheory.inv (CategoryTheory.Limits.pullback.fst i (CategoryTheory.CategoryStruct.id S))))
      (CategoryTheory.Limits.pullback.fst i (CategoryTheory.CategoryStruct.id S)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X) f