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
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
a : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
⊢ ∀ ⦃X Y : WalkingMulticospan J⦄ (f : X ⟶ Y),
    (((Functor.const (WalkingMulticospan J)).obj a.pt).map f ≫
        match Y with
        | WalkingMulticospan.left a_1 => a.ι ≫ c.proj a_1
        | WalkingMulticospan.right a_1 => a.ι ≫ I.fstPiMapOfIsLimit c hd ≫ d.proj a_1) =
      (match X with
        | WalkingMulticospan.left a_1 => a.ι ≫ c.proj a_1
        | WalkingMulticospan.right a_1 => a.ι ≫ I.fstPiMapOfIsLimit c hd ≫ d.proj a_1) ≫
        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
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
a : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
a✝ : J.L
⊢ (((Functor.const (WalkingMulticospan J)).obj a.pt).map (WalkingMulticospan.Hom.id (WalkingMulticospan.left a✝)) ≫
      match WalkingMulticospan.left a✝ with
      | WalkingMulticospan.left a_1 => a.ι ≫ c.proj a_1
      | WalkingMulticospan.right a_1 => a.ι ≫ I.fstPiMapOfIsLimit c hd ≫ d.proj a_1) =
    (match WalkingMulticospan.left a✝ with
      | WalkingMulticospan.left a_1 => a.ι ≫ c.proj a_1
      | WalkingMulticospan.right a_1 => a.ι ≫ I.fstPiMapOfIsLimit c hd ≫ d.proj a_1) ≫
      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
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
a : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
a✝ : J.R
⊢ (((Functor.const (WalkingMulticospan J)).obj a.pt).map (WalkingMulticospan.Hom.fst a✝) ≫
      match WalkingMulticospan.right a✝ with
      | WalkingMulticospan.left a_1 => a.ι ≫ c.proj a_1
      | WalkingMulticospan.right a_1 => a.ι ≫ I.fstPiMapOfIsLimit c hd ≫ d.proj a_1) =
    (match WalkingMulticospan.left (J.fst a✝) with
      | WalkingMulticospan.left a_1 => a.ι ≫ c.proj a_1
      | WalkingMulticospan.right a_1 => a.ι ≫ I.fstPiMapOfIsLimit c hd ≫ d.proj a_1) ≫
      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
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
a : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
a✝ : J.R
⊢ (((Functor.const (WalkingMulticospan J)).obj a.pt).map (WalkingMulticospan.Hom.snd a✝) ≫
      match WalkingMulticospan.right a✝ with
      | WalkingMulticospan.left a_1 => a.ι ≫ c.proj a_1
      | WalkingMulticospan.right a_1 => a.ι ≫ I.fstPiMapOfIsLimit c hd ≫ d.proj a_1) =
    (match WalkingMulticospan.left (J.snd a✝) with
      | WalkingMulticospan.left a_1 => a.ι ≫ c.proj a_1
      | WalkingMulticospan.right a_1 => a.ι ≫ I.fstPiMapOfIsLimit c hd ≫ d.proj a_1) ≫
      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
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
a : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
a✝ : J.R
⊢ (((Functor.const (WalkingMulticospan J)).obj a.pt).map (WalkingMulticospan.Hom.id (WalkingMulticospan.right a✝)) ≫
      match WalkingMulticospan.right a✝ with
      | WalkingMulticospan.left a_1 => a.ι ≫ c.proj a_1
      | WalkingMulticospan.right a_1 => a.ι ≫ I.fstPiMapOfIsLimit c hd ≫ d.proj a_1) =
    (match WalkingMulticospan.right a✝ with
      | WalkingMulticospan.left a_1 => a.ι ≫ c.proj a_1
      | WalkingMulticospan.right a_1 => a.ι ≫ I.fstPiMapOfIsLimit c hd ≫ d.proj a_1) ≫
      I.multicospan.map (WalkingMulticospan.Hom.id (WalkingMulticospan.right a✝))