Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J✝ : MultispanShape
I✝ : MultispanIndex J✝ C
K : Multicofork I✝
J : MultispanShape
I : MultispanIndex J C
P : C
π : (b : J.R) → I.right b ⟶ P
w : ∀ (a : J.L), I.fst a ≫ π (J.fst a) = I.snd a ≫ π (J.snd a)
⊢ ∀ ⦃X Y : WalkingMultispan J⦄ (f : X ⟶ Y),
    (I.multispan.map f ≫
        match Y with
        | WalkingMultispan.left a => I.fst a ≫ π (J.fst a)
        | WalkingMultispan.right a => π a) =
      (match X with
        | WalkingMultispan.left a => I.fst a ≫ π (J.fst a)
        | WalkingMultispan.right a => π a) ≫
        ((Functor.const (WalkingMultispan J)).obj P).map f

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

Goal state after:
case left.left.id
C : Type u
inst✝ : Category.{v, u} C
J✝ : MultispanShape
I✝ : MultispanIndex J✝ C
K : Multicofork I✝
J : MultispanShape
I : MultispanIndex J C
P : C
π : (b : J.R) → I.right b ⟶ P
w : ∀ (a : J.L), I.fst a ≫ π (J.fst a) = I.snd a ≫ π (J.snd a)
a✝ : J.L
⊢ (I.multispan.map (WalkingMultispan.Hom.id (WalkingMultispan.left a✝)) ≫
      match WalkingMultispan.left a✝ with
      | WalkingMultispan.left a => I.fst a ≫ π (J.fst a)
      | WalkingMultispan.right a => π a) =
    (match WalkingMultispan.left a✝ with
      | WalkingMultispan.left a => I.fst a ≫ π (J.fst a)
      | WalkingMultispan.right a => π a) ≫
      ((Functor.const (WalkingMultispan J)).obj P).map (WalkingMultispan.Hom.id (WalkingMultispan.left a✝))

case left.right.fst
C : Type u
inst✝ : Category.{v, u} C
J✝ : MultispanShape
I✝ : MultispanIndex J✝ C
K : Multicofork I✝
J : MultispanShape
I : MultispanIndex J C
P : C
π : (b : J.R) → I.right b ⟶ P
w : ∀ (a : J.L), I.fst a ≫ π (J.fst a) = I.snd a ≫ π (J.snd a)
a✝ : J.L
⊢ (I.multispan.map (WalkingMultispan.Hom.fst a✝) ≫
      match WalkingMultispan.right (J.fst a✝) with
      | WalkingMultispan.left a => I.fst a ≫ π (J.fst a)
      | WalkingMultispan.right a => π a) =
    (match WalkingMultispan.left a✝ with
      | WalkingMultispan.left a => I.fst a ≫ π (J.fst a)
      | WalkingMultispan.right a => π a) ≫
      ((Functor.const (WalkingMultispan J)).obj P).map (WalkingMultispan.Hom.fst a✝)

case left.right.snd
C : Type u
inst✝ : Category.{v, u} C
J✝ : MultispanShape
I✝ : MultispanIndex J✝ C
K : Multicofork I✝
J : MultispanShape
I : MultispanIndex J C
P : C
π : (b : J.R) → I.right b ⟶ P
w : ∀ (a : J.L), I.fst a ≫ π (J.fst a) = I.snd a ≫ π (J.snd a)
a✝ : J.L
⊢ (I.multispan.map (WalkingMultispan.Hom.snd a✝) ≫
      match WalkingMultispan.right (J.snd a✝) with
      | WalkingMultispan.left a => I.fst a ≫ π (J.fst a)
      | WalkingMultispan.right a => π a) =
    (match WalkingMultispan.left a✝ with
      | WalkingMultispan.left a => I.fst a ≫ π (J.fst a)
      | WalkingMultispan.right a => π a) ≫
      ((Functor.const (WalkingMultispan J)).obj P).map (WalkingMultispan.Hom.snd a✝)

case right.right.id
C : Type u
inst✝ : Category.{v, u} C
J✝ : MultispanShape
I✝ : MultispanIndex J✝ C
K : Multicofork I✝
J : MultispanShape
I : MultispanIndex J C
P : C
π : (b : J.R) → I.right b ⟶ P
w : ∀ (a : J.L), I.fst a ≫ π (J.fst a) = I.snd a ≫ π (J.snd a)
a✝ : J.R
⊢ (I.multispan.map (WalkingMultispan.Hom.id (WalkingMultispan.right a✝)) ≫
      match WalkingMultispan.right a✝ with
      | WalkingMultispan.left a => I.fst a ≫ π (J.fst a)
      | WalkingMultispan.right a => π a) =
    (match WalkingMultispan.right a✝ with
      | WalkingMultispan.left a => I.fst a ≫ π (J.fst a)
      | WalkingMultispan.right a => π a) ≫
      ((Functor.const (WalkingMultispan J)).obj P).map (WalkingMultispan.Hom.id (WalkingMultispan.right a✝))