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 : MulticospanShape
I : MulticospanIndex J C
a✝ : J.L
⊢ (match WalkingMulticospan.left a✝, WalkingMulticospan.left a✝,
      WalkingMulticospan.Hom.id (WalkingMulticospan.left a✝) ≫
        WalkingMulticospan.Hom.id (WalkingMulticospan.left a✝) with
    | x, .(x), WalkingMulticospan.Hom.id .(x) =>
      𝟙
        (match x with
        | WalkingMulticospan.left a => I.left a
        | WalkingMulticospan.right b => I.right b)
    | .(WalkingMulticospan.left (J.fst b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b => I.fst b
    | .(WalkingMulticospan.left (J.snd b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b => I.snd b) =
    (match WalkingMulticospan.left a✝, WalkingMulticospan.left a✝,
        WalkingMulticospan.Hom.id (WalkingMulticospan.left a✝) with
      | x, .(x), WalkingMulticospan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMulticospan.left a => I.left a
          | WalkingMulticospan.right b => I.right b)
      | .(WalkingMulticospan.left (J.fst b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b => I.fst b
      | .(WalkingMulticospan.left (J.snd b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b => I.snd b) ≫
      match WalkingMulticospan.left a✝, WalkingMulticospan.left a✝,
        WalkingMulticospan.Hom.id (WalkingMulticospan.left a✝) with
      | x, .(x), WalkingMulticospan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMulticospan.left a => I.left a
          | WalkingMulticospan.right b => I.right b)
      | .(WalkingMulticospan.left (J.fst b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b => I.fst b
      | .(WalkingMulticospan.left (J.snd b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b => I.snd b

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

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

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

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

pp: case right.right.right.id.id
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
a✝ : J.R
⊢ (match WalkingMulticospan.right a✝, WalkingMulticospan.right a✝,
      WalkingMulticospan.Hom.id (WalkingMulticospan.right a✝) ≫
        WalkingMulticospan.Hom.id (WalkingMulticospan.right a✝) with
    | x, .(x), WalkingMulticospan.Hom.id .(x) =>
      𝟙
        (match x with
        | WalkingMulticospan.left a => I.left a
        | WalkingMulticospan.right b => I.right b)
    | .(WalkingMulticospan.left (J.fst b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b => I.fst b
    | .(WalkingMulticospan.left (J.snd b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b => I.snd b) =
    (match WalkingMulticospan.right a✝, WalkingMulticospan.right a✝,
        WalkingMulticospan.Hom.id (WalkingMulticospan.right a✝) with
      | x, .(x), WalkingMulticospan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMulticospan.left a => I.left a
          | WalkingMulticospan.right b => I.right b)
      | .(WalkingMulticospan.left (J.fst b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b => I.fst b
      | .(WalkingMulticospan.left (J.snd b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b => I.snd b) ≫
      match WalkingMulticospan.right a✝, WalkingMulticospan.right a✝,
        WalkingMulticospan.Hom.id (WalkingMulticospan.right a✝) with
      | x, .(x), WalkingMulticospan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMulticospan.left a => I.left a
          | WalkingMulticospan.right b => I.right b)
      | .(WalkingMulticospan.left (J.fst b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b => I.fst b
      | .(WalkingMulticospan.left (J.snd b)), .(WalkingMulticospan.right b), WalkingMulticospan.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 : MulticospanShape
I : MulticospanIndex J C
a✝ : J.L
⊢ (match WalkingMulticospan.left a✝, WalkingMulticospan.left a✝,
      WalkingMulticospan.Hom.id (WalkingMulticospan.left a✝) ≫
        WalkingMulticospan.Hom.id (WalkingMulticospan.left a✝) with
    | x, .(x), WalkingMulticospan.Hom.id .(x) =>
      𝟙
        (match x with
        | WalkingMulticospan.left a => I.left a
        | WalkingMulticospan.right b => I.right b)
    | .(WalkingMulticospan.left (J.fst b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b => I.fst b
    | .(WalkingMulticospan.left (J.snd b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b => I.snd b) =
    (match WalkingMulticospan.left a✝, WalkingMulticospan.left a✝,
        WalkingMulticospan.Hom.id (WalkingMulticospan.left a✝) with
      | x, .(x), WalkingMulticospan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMulticospan.left a => I.left a
          | WalkingMulticospan.right b => I.right b)
      | .(WalkingMulticospan.left (J.fst b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b => I.fst b
      | .(WalkingMulticospan.left (J.snd b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b => I.snd b) ≫
      match WalkingMulticospan.left a✝, WalkingMulticospan.left a✝,
        WalkingMulticospan.Hom.id (WalkingMulticospan.left a✝) with
      | x, .(x), WalkingMulticospan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMulticospan.left a => I.left a
          | WalkingMulticospan.right b => I.right b)
      | .(WalkingMulticospan.left (J.fst b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b => I.fst b
      | .(WalkingMulticospan.left (J.snd b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b => I.snd b

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

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

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

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

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