Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.left.left.id.id
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
a✝ : J.L
⊢ (match WalkingMultispan.left a✝, WalkingMultispan.left a✝,
      WalkingMultispan.Hom.id (WalkingMultispan.left a✝) ≫ WalkingMultispan.Hom.id (WalkingMultispan.left a✝) with
    | x, .(x), WalkingMultispan.Hom.id .(x) =>
      𝟙
        (match x with
        | WalkingMultispan.left a => I.left a
        | WalkingMultispan.right b => I.right b)
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b) =
    (match WalkingMultispan.left a✝, WalkingMultispan.left a✝, WalkingMultispan.Hom.id (WalkingMultispan.left a✝) with
      | x, .(x), WalkingMultispan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b)
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b) ≫
      match WalkingMultispan.left a✝, WalkingMultispan.left a✝, WalkingMultispan.Hom.id (WalkingMultispan.left a✝) with
      | x, .(x), WalkingMultispan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b)
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b

pp: case left.left.right.id.fst
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
a✝ : J.L
⊢ (match WalkingMultispan.left a✝, WalkingMultispan.right (J.fst a✝),
      WalkingMultispan.Hom.id (WalkingMultispan.left a✝) ≫ WalkingMultispan.Hom.fst a✝ with
    | x, .(x), WalkingMultispan.Hom.id .(x) =>
      𝟙
        (match x with
        | WalkingMultispan.left a => I.left a
        | WalkingMultispan.right b => I.right b)
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b) =
    (match WalkingMultispan.left a✝, WalkingMultispan.left a✝, WalkingMultispan.Hom.id (WalkingMultispan.left a✝) with
      | x, .(x), WalkingMultispan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b)
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b) ≫
      match WalkingMultispan.left a✝, WalkingMultispan.right (J.fst a✝), WalkingMultispan.Hom.fst a✝ with
      | x, .(x), WalkingMultispan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b)
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b

pp: case left.left.right.id.snd
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
a✝ : J.L
⊢ (match WalkingMultispan.left a✝, WalkingMultispan.right (J.snd a✝),
      WalkingMultispan.Hom.id (WalkingMultispan.left a✝) ≫ WalkingMultispan.Hom.snd a✝ with
    | x, .(x), WalkingMultispan.Hom.id .(x) =>
      𝟙
        (match x with
        | WalkingMultispan.left a => I.left a
        | WalkingMultispan.right b => I.right b)
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b) =
    (match WalkingMultispan.left a✝, WalkingMultispan.left a✝, WalkingMultispan.Hom.id (WalkingMultispan.left a✝) with
      | x, .(x), WalkingMultispan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b)
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b) ≫
      match WalkingMultispan.left a✝, WalkingMultispan.right (J.snd a✝), WalkingMultispan.Hom.snd a✝ with
      | x, .(x), WalkingMultispan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b)
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b

pp: case left.right.right.fst.id
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
a✝ : J.L
⊢ (match WalkingMultispan.left a✝, WalkingMultispan.right (J.fst a✝),
      WalkingMultispan.Hom.fst a✝ ≫ WalkingMultispan.Hom.id (WalkingMultispan.right (J.fst a✝)) with
    | x, .(x), WalkingMultispan.Hom.id .(x) =>
      𝟙
        (match x with
        | WalkingMultispan.left a => I.left a
        | WalkingMultispan.right b => I.right b)
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b) =
    (match WalkingMultispan.left a✝, WalkingMultispan.right (J.fst a✝), WalkingMultispan.Hom.fst a✝ with
      | x, .(x), WalkingMultispan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b)
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b) ≫
      match WalkingMultispan.right (J.fst a✝), WalkingMultispan.right (J.fst a✝),
        WalkingMultispan.Hom.id (WalkingMultispan.right (J.fst a✝)) with
      | x, .(x), WalkingMultispan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b)
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b

pp: case left.right.right.snd.id
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
a✝ : J.L
⊢ (match WalkingMultispan.left a✝, WalkingMultispan.right (J.snd a✝),
      WalkingMultispan.Hom.snd a✝ ≫ WalkingMultispan.Hom.id (WalkingMultispan.right (J.snd a✝)) with
    | x, .(x), WalkingMultispan.Hom.id .(x) =>
      𝟙
        (match x with
        | WalkingMultispan.left a => I.left a
        | WalkingMultispan.right b => I.right b)
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b) =
    (match WalkingMultispan.left a✝, WalkingMultispan.right (J.snd a✝), WalkingMultispan.Hom.snd a✝ with
      | x, .(x), WalkingMultispan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b)
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b) ≫
      match WalkingMultispan.right (J.snd a✝), WalkingMultispan.right (J.snd a✝),
        WalkingMultispan.Hom.id (WalkingMultispan.right (J.snd a✝)) with
      | x, .(x), WalkingMultispan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b)
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b

pp: case right.right.right.id.id
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
a✝ : J.R
⊢ (match WalkingMultispan.right a✝, WalkingMultispan.right a✝,
      WalkingMultispan.Hom.id (WalkingMultispan.right a✝) ≫ WalkingMultispan.Hom.id (WalkingMultispan.right a✝) with
    | x, .(x), WalkingMultispan.Hom.id .(x) =>
      𝟙
        (match x with
        | WalkingMultispan.left a => I.left a
        | WalkingMultispan.right b => I.right b)
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b) =
    (match WalkingMultispan.right a✝, WalkingMultispan.right a✝,
        WalkingMultispan.Hom.id (WalkingMultispan.right a✝) with
      | x, .(x), WalkingMultispan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b)
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b) ≫
      match WalkingMultispan.right a✝, WalkingMultispan.right a✝,
        WalkingMultispan.Hom.id (WalkingMultispan.right a✝) with
      | x, .(x), WalkingMultispan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b)
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b

Tactic:
<;>

Goal state after:
case left.left.left.id.id
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
a✝ : J.L
⊢ (match WalkingMultispan.left a✝, WalkingMultispan.left a✝,
      WalkingMultispan.Hom.id (WalkingMultispan.left a✝) ≫ WalkingMultispan.Hom.id (WalkingMultispan.left a✝) with
    | x, .(x), WalkingMultispan.Hom.id .(x) =>
      𝟙
        (match x with
        | WalkingMultispan.left a => I.left a
        | WalkingMultispan.right b => I.right b)
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b) =
    (match WalkingMultispan.left a✝, WalkingMultispan.left a✝, WalkingMultispan.Hom.id (WalkingMultispan.left a✝) with
      | x, .(x), WalkingMultispan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b)
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b) ≫
      match WalkingMultispan.left a✝, WalkingMultispan.left a✝, WalkingMultispan.Hom.id (WalkingMultispan.left a✝) with
      | x, .(x), WalkingMultispan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b)
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b

case left.left.right.id.fst
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
a✝ : J.L
⊢ (match WalkingMultispan.left a✝, WalkingMultispan.right (J.fst a✝),
      WalkingMultispan.Hom.id (WalkingMultispan.left a✝) ≫ WalkingMultispan.Hom.fst a✝ with
    | x, .(x), WalkingMultispan.Hom.id .(x) =>
      𝟙
        (match x with
        | WalkingMultispan.left a => I.left a
        | WalkingMultispan.right b => I.right b)
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b) =
    (match WalkingMultispan.left a✝, WalkingMultispan.left a✝, WalkingMultispan.Hom.id (WalkingMultispan.left a✝) with
      | x, .(x), WalkingMultispan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b)
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b) ≫
      match WalkingMultispan.left a✝, WalkingMultispan.right (J.fst a✝), WalkingMultispan.Hom.fst a✝ with
      | x, .(x), WalkingMultispan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b)
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b

case left.left.right.id.snd
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
a✝ : J.L
⊢ (match WalkingMultispan.left a✝, WalkingMultispan.right (J.snd a✝),
      WalkingMultispan.Hom.id (WalkingMultispan.left a✝) ≫ WalkingMultispan.Hom.snd a✝ with
    | x, .(x), WalkingMultispan.Hom.id .(x) =>
      𝟙
        (match x with
        | WalkingMultispan.left a => I.left a
        | WalkingMultispan.right b => I.right b)
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b) =
    (match WalkingMultispan.left a✝, WalkingMultispan.left a✝, WalkingMultispan.Hom.id (WalkingMultispan.left a✝) with
      | x, .(x), WalkingMultispan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b)
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b) ≫
      match WalkingMultispan.left a✝, WalkingMultispan.right (J.snd a✝), WalkingMultispan.Hom.snd a✝ with
      | x, .(x), WalkingMultispan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b)
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b

case left.right.right.fst.id
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
a✝ : J.L
⊢ (match WalkingMultispan.left a✝, WalkingMultispan.right (J.fst a✝),
      WalkingMultispan.Hom.fst a✝ ≫ WalkingMultispan.Hom.id (WalkingMultispan.right (J.fst a✝)) with
    | x, .(x), WalkingMultispan.Hom.id .(x) =>
      𝟙
        (match x with
        | WalkingMultispan.left a => I.left a
        | WalkingMultispan.right b => I.right b)
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b) =
    (match WalkingMultispan.left a✝, WalkingMultispan.right (J.fst a✝), WalkingMultispan.Hom.fst a✝ with
      | x, .(x), WalkingMultispan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b)
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b) ≫
      match WalkingMultispan.right (J.fst a✝), WalkingMultispan.right (J.fst a✝),
        WalkingMultispan.Hom.id (WalkingMultispan.right (J.fst a✝)) with
      | x, .(x), WalkingMultispan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b)
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b

case left.right.right.snd.id
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
a✝ : J.L
⊢ (match WalkingMultispan.left a✝, WalkingMultispan.right (J.snd a✝),
      WalkingMultispan.Hom.snd a✝ ≫ WalkingMultispan.Hom.id (WalkingMultispan.right (J.snd a✝)) with
    | x, .(x), WalkingMultispan.Hom.id .(x) =>
      𝟙
        (match x with
        | WalkingMultispan.left a => I.left a
        | WalkingMultispan.right b => I.right b)
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b) =
    (match WalkingMultispan.left a✝, WalkingMultispan.right (J.snd a✝), WalkingMultispan.Hom.snd a✝ with
      | x, .(x), WalkingMultispan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b)
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b) ≫
      match WalkingMultispan.right (J.snd a✝), WalkingMultispan.right (J.snd a✝),
        WalkingMultispan.Hom.id (WalkingMultispan.right (J.snd a✝)) with
      | x, .(x), WalkingMultispan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b)
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b

case right.right.right.id.id
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
a✝ : J.R
⊢ (match WalkingMultispan.right a✝, WalkingMultispan.right a✝,
      WalkingMultispan.Hom.id (WalkingMultispan.right a✝) ≫ WalkingMultispan.Hom.id (WalkingMultispan.right a✝) with
    | x, .(x), WalkingMultispan.Hom.id .(x) =>
      𝟙
        (match x with
        | WalkingMultispan.left a => I.left a
        | WalkingMultispan.right b => I.right b)
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b) =
    (match WalkingMultispan.right a✝, WalkingMultispan.right a✝,
        WalkingMultispan.Hom.id (WalkingMultispan.right a✝) with
      | x, .(x), WalkingMultispan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b)
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b) ≫
      match WalkingMultispan.right a✝, WalkingMultispan.right a✝,
        WalkingMultispan.Hom.id (WalkingMultispan.right a✝) with
      | x, .(x), WalkingMultispan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b)
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b