∀ {C : Type u_4} [inst : CategoryTheory.Category.{u_3, u_4} C] {J : CategoryTheory.Limits.MultispanShape}
  [inst_1 : Unique J.L] {I : CategoryTheory.Limits.MultispanIndex J C} (h : {J.fst default, J.snd default} = Set.univ),
  J.fst default ≠ J.snd default →
    ∀ (s : CategoryTheory.Limits.PushoutCocone (I.fst default) (I.snd default)) (a : J.L),
      CategoryTheory.CategoryStruct.comp (I.fst a)
          ((fun k =>
              if hk : k = J.fst default then CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) s.inl
              else CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) s.inr)
            (J.fst a)) =
        CategoryTheory.CategoryStruct.comp (I.snd a)
          ((fun k =>
              if hk : k = J.fst default then CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) s.inl
              else CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) s.inr)
            (J.snd a))