∀ {J : CategoryTheory.Limits.MultispanShape} {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  {F G : CategoryTheory.Functor (CategoryTheory.Limits.WalkingMultispan J) C}
  (left :
    (i : J.L) →
      F.obj (CategoryTheory.Limits.WalkingMultispan.left i) ≅ G.obj (CategoryTheory.Limits.WalkingMultispan.left i))
  (right :
    (i : J.R) →
      F.obj (CategoryTheory.Limits.WalkingMultispan.right i) ≅ G.obj (CategoryTheory.Limits.WalkingMultispan.right i))
  (wl :
    autoParam
      (∀ (i : J.L),
        CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.WalkingMultispan.Hom.fst i))
            (right (J.fst i)).hom =
          CategoryTheory.CategoryStruct.comp (left i).hom (G.map (CategoryTheory.Limits.WalkingMultispan.Hom.fst i)))
      CategoryTheory.Limits.WalkingMultispan.functorExt._auto_1)
  (wr :
    autoParam
      (∀ (i : J.L),
        CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.WalkingMultispan.Hom.snd i))
            (right (J.snd i)).hom =
          CategoryTheory.CategoryStruct.comp (left i).hom (G.map (CategoryTheory.Limits.WalkingMultispan.Hom.snd i)))
      CategoryTheory.Limits.WalkingMultispan.functorExt._auto_3)
  (X : CategoryTheory.Limits.WalkingMultispan J),
  (CategoryTheory.Limits.WalkingMultispan.functorExt left right wl wr).inv.app X =
    (match X with
      | CategoryTheory.Limits.WalkingMultispan.left i => left i
      | CategoryTheory.Limits.WalkingMultispan.right i => right i).inv