Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: 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
⊢ ∀ ⦃X Y : WalkingMulticospan J⦄ (f : X ⟶ Y),
    (((Functor.const (WalkingMulticospan J)).obj P).map f ≫
        match Y with
        | WalkingMulticospan.left a => ι a
        | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) =
      (match X with
        | WalkingMulticospan.left a => ι a
        | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) ≫
        I.multicospan.map f

Tactic:
rintro (_ | _) (_ | _) (_ | _ | _)

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✝))