∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {ι : Type u_3} {B : C} {objs : ι → C}
  (arrows : (j : ι) → objs j ⟶ B) {c : CategoryTheory.Limits.Fan objs} (hc : CategoryTheory.Limits.IsLimit c)
  (hB : CategoryTheory.Limits.IsTerminal B) (s : CategoryTheory.Limits.WidePullbackCone arrows),
  CategoryTheory.CategoryStruct.comp (hc.lift (CategoryTheory.Limits.WidePullbackCone.toFan arrows s))
      (CategoryTheory.Limits.WidePullbackCone.ofFan arrows c hB).base =
    s.base