Allowing multiple targets in `case`

Stream: metaprogramming / tactics

[Eric Wieser]

Is this a good idea? I can't post a mwe because I rely on private meta defs visible only within core lean, but a PR is at https://github.com/leanprover-community/lean/pull/508.

This enables syntax like:

example (α β : Type*) (i j : α ⊕ β) : ℕ :=
begin
  with_cases {cases hi : i; cases hj : j},
  case [sum.inl sum.inl : i j, sum.inr sum.inr : i j] {
    exact 1,
    exact 1,
  },
  case [sum.inl sum.inr : i j, sum.inr sum.inl : i j] {
    exact 2,
    exact 2,
  },
end