Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
⊢ ∀ {X Y Z : WalkingMulticospan J} (f : X ⟶ Y) (g : Y ⟶ Z),
    (match X, Z, f ≫ g 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 X, Y, f 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 Y, Z, g 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:
rintro (_ | _) (_ | _) (_ | _) (_ | _ | _) (_ | _ | _)

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