∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) [inst_1 : CategoryTheory.Limits.HasProduct I.left]
  [inst_2 : CategoryTheory.Limits.HasProduct I.right]
  (a :
    CategoryTheory.Limits.Fork
      (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left))
        (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))
      (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left))
        (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right))))
  (x : CategoryTheory.Limits.WalkingMulticospan J),
  (I.multiforkEquivPiFork.inverse.obj a).π.app x =
    match x with
    | CategoryTheory.Limits.WalkingMulticospan.left a_1 =>
      CategoryTheory.CategoryStruct.comp a.ι
        (CategoryTheory.Limits.Fan.proj (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) a_1)
    | CategoryTheory.Limits.WalkingMulticospan.right a_1 =>
      CategoryTheory.CategoryStruct.comp a.ι
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.Fan.proj (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left))
            (J.fst a_1))
          (I.fst a_1))