∀ {J : Type u_3} {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C]
  {F : CategoryTheory.Functor (CategoryTheory.Limits.WidePullbackShape J) C} {X : C} (f : X ⟶ F.obj none)
  (π : (j : J) → X ⟶ F.obj (some j)),
  (∀ (j : J),
      CategoryTheory.CategoryStruct.comp (π j) (F.map (CategoryTheory.Limits.WidePullbackShape.Hom.term j)) = f) →
    ∀ (j j' : CategoryTheory.Limits.WidePullbackShape J) (f_1 : j ⟶ j'),
      CategoryTheory.CategoryStruct.comp
          (((CategoryTheory.Functor.const (CategoryTheory.Limits.WidePullbackShape J)).obj X).map f_1)
          (match j' with
          | none => f
          | some j => π j) =
        CategoryTheory.CategoryStruct.comp
          (match j with
          | none => f
          | some j => π j)
          (F.map f_1)