feat(tactic/rcases): clear pattern `-` in rcases (#3868)
This allows you to write:
```lean
example (h : ∃ x : ℕ, true) : true :=
begin
rcases h with ⟨x, -⟩,
-- x : ℕ |- true
end
```
to clear unwanted hypotheses. Note that dependents are also cleared,
meaning that you can get into trouble if you try to keep matching when a
variable later in the pattern is deleted. The `_` pattern will match
a hypothesis even if it has been deleted, so this is the recommended way
to match on variables dependent on a deleted hypothesis.
You can use `-` if you prefer, but watch out for unintended variables
getting deleted if there are duplicate names!
