∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {ι : Type u_3} {X : C} {Y : ι → C}
  {f : (i : ι) → Y i ⟶ X} (s : CategoryTheory.Limits.WidePullbackCone f) {ι' : Type u_4} (e : ι' ≃ ι),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Iso.refl
          ((CategoryTheory.Limits.Cones.postcompose
                  (CategoryTheory.Limits.WidePullbackShape.functorExt (CategoryTheory.Iso.refl X)
                      (fun i => CategoryTheory.eqToIso ⋯) ⋯).hom).obj
              (CategoryTheory.Limits.Cone.whisker
                (CategoryTheory.Limits.WidePullbackShape.equivalenceOfEquiv ι' e.symm).functor (s.reindex e))).pt).hom
      s.base =
    CategoryTheory.Limits.WidePullbackCone.base
      ((CategoryTheory.Limits.Cones.postcompose
            (CategoryTheory.Limits.WidePullbackShape.functorExt (CategoryTheory.Iso.refl X)
                (fun i => CategoryTheory.eqToIso ⋯) ⋯).hom).obj
        (CategoryTheory.Limits.Cone.whisker
          (CategoryTheory.Limits.WidePullbackShape.equivalenceOfEquiv ι' e.symm).functor (s.reindex e)))