∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C}
  (z : F.obj CategoryTheory.Limits.WalkingCospan.one ⟶ G.obj CategoryTheory.Limits.WalkingCospan.one)
  (l : F.obj CategoryTheory.Limits.WalkingCospan.left ⟶ G.obj CategoryTheory.Limits.WalkingCospan.left)
  (r : F.obj CategoryTheory.Limits.WalkingCospan.right ⟶ G.obj CategoryTheory.Limits.WalkingCospan.right)
  (hl :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingCospan.Hom.inl) z =
        CategoryTheory.CategoryStruct.comp l (G.map CategoryTheory.Limits.WalkingCospan.Hom.inl))
      CategoryTheory.Limits.cospanHomMk._auto_1)
  (hr :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingCospan.Hom.inr) z =
        CategoryTheory.CategoryStruct.comp r (G.map CategoryTheory.Limits.WalkingCospan.Hom.inr))
      CategoryTheory.Limits.cospanHomMk._auto_3)
  (X : CategoryTheory.Limits.WalkingCospan),
  (CategoryTheory.Limits.cospanHomMk z l r hl hr).app X =
    Option.casesOn X z fun val => CategoryTheory.Limits.WalkingPair.casesOn val l r