Sum.elim_elim

Stream: Is there code for X?

[Wrenna Robson]

theorem Sum.elim_elim {α β γ δ ε} {f : α → γ ⊕ δ} {g : β → γ ⊕ δ}
 {p : γ → ε} {q : δ → ε} {x} :
 Sum.elim p q (Sum.elim f g x) =
Sum.elim (Sum.elim p q ∘ f) (Sum.elim p q ∘ g) x := by cases x <;> simp

[Wrenna Robson]

Do we have this?

[Wrenna Robson]

Ah I think it's an applied form of docs#Sum.comp_elim