∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C)
  (X : CategoryTheory.Limits.WalkingParallelFamily J),
  (CategoryTheory.Limits.diagramIsoParallelFamily F).hom.app X = CategoryTheory.eqToHom ⋯