mathlib3

b1da074a - feat(data/sum/basic): Shortcuts for the ternary sum of types (#13678)

feat(data/sum/basic): Shortcuts for the ternary sum of types (#13678) Define `sum3.in₀`, `sum3.in₁`, `sum3.in₂`, shortcut patterns for pattern-matching on a ternary sum of types. Co-authored-by: Bhavik Mehta <bhavik.mehta8@gmail.com>