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
c : Cofan I.left
hc : IsColimit c
d : Cofan I.right
hd : IsColimit d
a : Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)
⊢ ∀ ⦃X Y : WalkingMultispan J⦄ (f : X ⟶ Y),
    (I.multispan.map f ≫
        match Y with
        | WalkingMultispan.left a_1 => c.inj a_1 ≫ I.fstSigmaMapOfIsColimit d hc ≫ a.π
        | WalkingMultispan.right a_1 => d.inj a_1 ≫ a.π) =
      (match X with
        | WalkingMultispan.left a_1 => c.inj a_1 ≫ I.fstSigmaMapOfIsColimit d hc ≫ a.π
        | WalkingMultispan.right a_1 => d.inj a_1 ≫ a.π) ≫
        ((Functor.const (WalkingMultispan J)).obj a.pt).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
c : Cofan I.left
hc : IsColimit c
d : Cofan I.right
hd : IsColimit d
a : Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)
a✝ : J.L
⊢ (I.multispan.map (WalkingMultispan.Hom.id (WalkingMultispan.left a✝)) ≫
      match WalkingMultispan.left a✝ with
      | WalkingMultispan.left a_1 => c.inj a_1 ≫ I.fstSigmaMapOfIsColimit d hc ≫ a.π
      | WalkingMultispan.right a_1 => d.inj a_1 ≫ a.π) =
    (match WalkingMultispan.left a✝ with
      | WalkingMultispan.left a_1 => c.inj a_1 ≫ I.fstSigmaMapOfIsColimit d hc ≫ a.π
      | WalkingMultispan.right a_1 => d.inj a_1 ≫ a.π) ≫
      ((Functor.const (WalkingMultispan J)).obj a.pt).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
c : Cofan I.left
hc : IsColimit c
d : Cofan I.right
hd : IsColimit d
a : Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)
a✝ : J.L
⊢ (I.multispan.map (WalkingMultispan.Hom.fst a✝) ≫
      match WalkingMultispan.right (J.fst a✝) with
      | WalkingMultispan.left a_1 => c.inj a_1 ≫ I.fstSigmaMapOfIsColimit d hc ≫ a.π
      | WalkingMultispan.right a_1 => d.inj a_1 ≫ a.π) =
    (match WalkingMultispan.left a✝ with
      | WalkingMultispan.left a_1 => c.inj a_1 ≫ I.fstSigmaMapOfIsColimit d hc ≫ a.π
      | WalkingMultispan.right a_1 => d.inj a_1 ≫ a.π) ≫
      ((Functor.const (WalkingMultispan J)).obj a.pt).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
c : Cofan I.left
hc : IsColimit c
d : Cofan I.right
hd : IsColimit d
a : Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)
a✝ : J.L
⊢ (I.multispan.map (WalkingMultispan.Hom.snd a✝) ≫
      match WalkingMultispan.right (J.snd a✝) with
      | WalkingMultispan.left a_1 => c.inj a_1 ≫ I.fstSigmaMapOfIsColimit d hc ≫ a.π
      | WalkingMultispan.right a_1 => d.inj a_1 ≫ a.π) =
    (match WalkingMultispan.left a✝ with
      | WalkingMultispan.left a_1 => c.inj a_1 ≫ I.fstSigmaMapOfIsColimit d hc ≫ a.π
      | WalkingMultispan.right a_1 => d.inj a_1 ≫ a.π) ≫
      ((Functor.const (WalkingMultispan J)).obj a.pt).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
c : Cofan I.left
hc : IsColimit c
d : Cofan I.right
hd : IsColimit d
a : Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)
a✝ : J.R
⊢ (I.multispan.map (WalkingMultispan.Hom.id (WalkingMultispan.right a✝)) ≫
      match WalkingMultispan.right a✝ with
      | WalkingMultispan.left a_1 => c.inj a_1 ≫ I.fstSigmaMapOfIsColimit d hc ≫ a.π
      | WalkingMultispan.right a_1 => d.inj a_1 ≫ a.π) =
    (match WalkingMultispan.right a✝ with
      | WalkingMultispan.left a_1 => c.inj a_1 ≫ I.fstSigmaMapOfIsColimit d hc ≫ a.π
      | WalkingMultispan.right a_1 => d.inj a_1 ≫ a.π) ≫
      ((Functor.const (WalkingMultispan J)).obj a.pt).map (WalkingMultispan.Hom.id (WalkingMultispan.right a✝))