∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {B : C} {objs : J → C}
  {arrows : (j : J) → objs j ⟶ B} [inst_1 : CategoryTheory.Limits.HasWidePullback B objs arrows] {X : C} (f f_1 : X ⟶ B)
  (e_f : f = f_1) (fs fs_1 : (j : J) → X ⟶ objs j) (e_fs : fs = fs_1)
  (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (fs j) (arrows j) = f),
  CategoryTheory.Limits.WidePullback.lift f fs w = CategoryTheory.Limits.WidePullback.lift f_1 fs_1 ⋯