∀ (J : CategoryTheory.Limits.MulticospanShape),
  Function.RightInverse
    (fun x =>
      match x with
      | CategoryTheory.Limits.WalkingMulticospan.left a => Sum.inl a
      | CategoryTheory.Limits.WalkingMulticospan.right a => Sum.inr a)
    fun x =>
    match x with
    | Sum.inl a => CategoryTheory.Limits.WalkingMulticospan.left a
    | Sum.inr a => CategoryTheory.Limits.WalkingMulticospan.right a