∀ {J : Type u_1} (J' : Type u_2) (h : J ≃ J') {X Y : CategoryTheory.Limits.WidePullbackShape J} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.id (CategoryTheory.Limits.WidePullbackShape J)).map f)
      ((fun j =>
            Option.casesOn (motive := fun t =>
              j = t →
                ((CategoryTheory.Functor.id (CategoryTheory.Limits.WidePullbackShape J)).obj j ≅
                  ((CategoryTheory.Limits.WidePullbackShape.wideCospan none (fun j => some (h j)) fun j =>
                            CategoryTheory.Limits.WidePullbackShape.Hom.term (h j)).comp
                        (CategoryTheory.Limits.WidePullbackShape.wideCospan none (fun j => some (h.invFun j)) fun j =>
                          CategoryTheory.Limits.WidePullbackShape.Hom.term (h.invFun j))).obj
                    j))
              j (fun h_1 => ⋯ ▸ CategoryTheory.eqToIso ⋯) (fun val h_1 => ⋯ ▸ CategoryTheory.eqToIso ⋯) ⋯)
          Y).hom =
    CategoryTheory.CategoryStruct.comp
      ((fun j =>
            Option.casesOn (motive := fun t =>
              j = t →
                ((CategoryTheory.Functor.id (CategoryTheory.Limits.WidePullbackShape J)).obj j ≅
                  ((CategoryTheory.Limits.WidePullbackShape.wideCospan none (fun j => some (h j)) fun j =>
                            CategoryTheory.Limits.WidePullbackShape.Hom.term (h j)).comp
                        (CategoryTheory.Limits.WidePullbackShape.wideCospan none (fun j => some (h.invFun j)) fun j =>
                          CategoryTheory.Limits.WidePullbackShape.Hom.term (h.invFun j))).obj
                    j))
              j (fun h_1 => ⋯ ▸ CategoryTheory.eqToIso ⋯) (fun val h_1 => ⋯ ▸ CategoryTheory.eqToIso ⋯) ⋯)
          X).hom
      (((CategoryTheory.Limits.WidePullbackShape.wideCospan none (fun j => some (h j)) fun j =>
                CategoryTheory.Limits.WidePullbackShape.Hom.term (h j)).comp
            (CategoryTheory.Limits.WidePullbackShape.wideCospan none (fun j => some (h.invFun j)) fun j =>
              CategoryTheory.Limits.WidePullbackShape.Hom.term (h.invFun j))).map
        f)