Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case id
J : MultispanShape
left✝ : WalkingMultispan J
⊢ Sum.elim (fun X ↦ Arrow.mk (𝟙 X)) (Sum.elim (fun a ↦ Arrow.mk (Hom.fst a)) fun a ↦ Arrow.mk (Hom.snd a))
      ((fun f ↦
          match f.right, f.left, f.hom with
          | x, .(x), Hom.id .(x) => Sum.inl x
          | .(right (J.fst a)), .(left a), Hom.fst a => Sum.inr (Sum.inl a)
          | .(right (J.snd a)), .(left a), Hom.snd a => Sum.inr (Sum.inr a))
        { left := left✝, right := left✝, hom := Hom.id ((𝟭 (WalkingMultispan J)).obj left✝) }) =
    { left := left✝, right := left✝, hom := Hom.id ((𝟭 (WalkingMultispan J)).obj left✝) }

pp: case fst
J : MultispanShape
a✝ : J.L
⊢ Sum.elim (fun X ↦ Arrow.mk (𝟙 X)) (Sum.elim (fun a ↦ Arrow.mk (Hom.fst a)) fun a ↦ Arrow.mk (Hom.snd a))
      ((fun f ↦
          match f.right, f.left, f.hom with
          | x, .(x), Hom.id .(x) => Sum.inl x
          | .(right (J.fst a)), .(left a), Hom.fst a => Sum.inr (Sum.inl a)
          | .(right (J.snd a)), .(left a), Hom.snd a => Sum.inr (Sum.inr a))
        { left := left a✝, right := right (J.fst a✝), hom := Hom.fst a✝ }) =
    { left := left a✝, right := right (J.fst a✝), hom := Hom.fst a✝ }

pp: case snd
J : MultispanShape
a✝ : J.L
⊢ Sum.elim (fun X ↦ Arrow.mk (𝟙 X)) (Sum.elim (fun a ↦ Arrow.mk (Hom.fst a)) fun a ↦ Arrow.mk (Hom.snd a))
      ((fun f ↦
          match f.right, f.left, f.hom with
          | x, .(x), Hom.id .(x) => Sum.inl x
          | .(right (J.fst a)), .(left a), Hom.fst a => Sum.inr (Sum.inl a)
          | .(right (J.snd a)), .(left a), Hom.snd a => Sum.inr (Sum.inr a))
        { left := left a✝, right := right (J.snd a✝), hom := Hom.snd a✝ }) =
    { left := left a✝, right := right (J.snd a✝), hom := Hom.snd a✝ }

Tactic:
<;>

Goal state after:
case id
J : MultispanShape
left✝ : WalkingMultispan J
⊢ Sum.elim (fun X ↦ Arrow.mk (𝟙 X)) (Sum.elim (fun a ↦ Arrow.mk (Hom.fst a)) fun a ↦ Arrow.mk (Hom.snd a))
      ((fun f ↦
          match f.right, f.left, f.hom with
          | x, .(x), Hom.id .(x) => Sum.inl x
          | .(right (J.fst a)), .(left a), Hom.fst a => Sum.inr (Sum.inl a)
          | .(right (J.snd a)), .(left a), Hom.snd a => Sum.inr (Sum.inr a))
        { left := left✝, right := left✝, hom := Hom.id ((𝟭 (WalkingMultispan J)).obj left✝) }) =
    { left := left✝, right := left✝, hom := Hom.id ((𝟭 (WalkingMultispan J)).obj left✝) }

case fst
J : MultispanShape
a✝ : J.L
⊢ Sum.elim (fun X ↦ Arrow.mk (𝟙 X)) (Sum.elim (fun a ↦ Arrow.mk (Hom.fst a)) fun a ↦ Arrow.mk (Hom.snd a))
      ((fun f ↦
          match f.right, f.left, f.hom with
          | x, .(x), Hom.id .(x) => Sum.inl x
          | .(right (J.fst a)), .(left a), Hom.fst a => Sum.inr (Sum.inl a)
          | .(right (J.snd a)), .(left a), Hom.snd a => Sum.inr (Sum.inr a))
        { left := left a✝, right := right (J.fst a✝), hom := Hom.fst a✝ }) =
    { left := left a✝, right := right (J.fst a✝), hom := Hom.fst a✝ }

case snd
J : MultispanShape
a✝ : J.L
⊢ Sum.elim (fun X ↦ Arrow.mk (𝟙 X)) (Sum.elim (fun a ↦ Arrow.mk (Hom.fst a)) fun a ↦ Arrow.mk (Hom.snd a))
      ((fun f ↦
          match f.right, f.left, f.hom with
          | x, .(x), Hom.id .(x) => Sum.inl x
          | .(right (J.fst a)), .(left a), Hom.fst a => Sum.inr (Sum.inl a)
          | .(right (J.snd a)), .(left a), Hom.snd a => Sum.inr (Sum.inr a))
        { left := left a✝, right := right (J.snd a✝), hom := Hom.snd a✝ }) =
    { left := left a✝, right := right (J.snd a✝), hom := Hom.snd a✝ }