Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.left.id
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.L
⊢ (((Functor.const (WalkingMulticospan J)).obj P).map (WalkingMulticospan.Hom.id (WalkingMulticospan.left a✝)) ≫
      match WalkingMulticospan.left a✝ with
      | WalkingMulticospan.left a => ι a
      | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) =
    (match WalkingMulticospan.left a✝ with
      | WalkingMulticospan.left a => ι a
      | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) ≫
      I.multicospan.map (WalkingMulticospan.Hom.id (WalkingMulticospan.left a✝))

pp: case left.right.fst
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.R
⊢ (((Functor.const (WalkingMulticospan J)).obj P).map (WalkingMulticospan.Hom.fst a✝) ≫
      match WalkingMulticospan.right a✝ with
      | WalkingMulticospan.left a => ι a
      | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) =
    (match WalkingMulticospan.left (J.fst a✝) with
      | WalkingMulticospan.left a => ι a
      | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) ≫
      I.multicospan.map (WalkingMulticospan.Hom.fst a✝)

pp: case left.right.snd
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.R
⊢ (((Functor.const (WalkingMulticospan J)).obj P).map (WalkingMulticospan.Hom.snd a✝) ≫
      match WalkingMulticospan.right a✝ with
      | WalkingMulticospan.left a => ι a
      | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) =
    (match WalkingMulticospan.left (J.snd a✝) with
      | WalkingMulticospan.left a => ι a
      | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) ≫
      I.multicospan.map (WalkingMulticospan.Hom.snd a✝)

pp: case right.right.id
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.R
⊢ (((Functor.const (WalkingMulticospan J)).obj P).map (WalkingMulticospan.Hom.id (WalkingMulticospan.right a✝)) ≫
      match WalkingMulticospan.right a✝ with
      | WalkingMulticospan.left a => ι a
      | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) =
    (match WalkingMulticospan.right a✝ with
      | WalkingMulticospan.left a => ι a
      | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) ≫
      I.multicospan.map (WalkingMulticospan.Hom.id (WalkingMulticospan.right a✝))

Tactic:
<;>

Goal state after:
case left.left.id
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.L
⊢ (((Functor.const (WalkingMulticospan J)).obj P).map (WalkingMulticospan.Hom.id (WalkingMulticospan.left a✝)) ≫
      match WalkingMulticospan.left a✝ with
      | WalkingMulticospan.left a => ι a
      | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) =
    (match WalkingMulticospan.left a✝ with
      | WalkingMulticospan.left a => ι a
      | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) ≫
      I.multicospan.map (WalkingMulticospan.Hom.id (WalkingMulticospan.left a✝))

case left.right.fst
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.R
⊢ (((Functor.const (WalkingMulticospan J)).obj P).map (WalkingMulticospan.Hom.fst a✝) ≫
      match WalkingMulticospan.right a✝ with
      | WalkingMulticospan.left a => ι a
      | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) =
    (match WalkingMulticospan.left (J.fst a✝) with
      | WalkingMulticospan.left a => ι a
      | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) ≫
      I.multicospan.map (WalkingMulticospan.Hom.fst a✝)

case left.right.snd
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.R
⊢ (((Functor.const (WalkingMulticospan J)).obj P).map (WalkingMulticospan.Hom.snd a✝) ≫
      match WalkingMulticospan.right a✝ with
      | WalkingMulticospan.left a => ι a
      | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) =
    (match WalkingMulticospan.left (J.snd a✝) with
      | WalkingMulticospan.left a => ι a
      | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) ≫
      I.multicospan.map (WalkingMulticospan.Hom.snd a✝)

case right.right.id
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.R
⊢ (((Functor.const (WalkingMulticospan J)).obj P).map (WalkingMulticospan.Hom.id (WalkingMulticospan.right a✝)) ≫
      match WalkingMulticospan.right a✝ with
      | WalkingMulticospan.left a => ι a
      | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) =
    (match WalkingMulticospan.right a✝ with
      | WalkingMulticospan.left a => ι a
      | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) ≫
      I.multicospan.map (WalkingMulticospan.Hom.id (WalkingMulticospan.right a✝))