mathlib

2297d200 - feat(tactic/clear): add clear' tactic (#1899)

feat(tactic/clear): add clear' tactic (#1899) * feat(tactic/clear): add clear' tactic We add an improved version of the `clear` tactic. When clearing multiple hypotheses, `clear` can fail even though all hypotheses could be cleared. This happens when the hypotheses depend on each other and are given in the wrong order: ```lean example : ∀ {α : Type} {β : α → Type} (a : α) (b : β a), unit := begin intros α β a b, clear a b, -- fails exact () end ``` When `clear` tries to clear `a`, `b`, which depends on `a`, is still in the context, so the operation fails. We give a tactic `clear'` which recognises this and clears `b` before `a`. * refactor(tactic/clear): better implementation of clear' We refactor `clear'`, replacing the old implementation with one that is more concise and should be faster. The new implementation strategy also gives us a new variant of `clear`, `clear_dependent`, almost for free. `clear_dependent` works like `clear'`, but in addition to the given hypotheses, it also clears any other hypotheses which depend on them. * style(test/tactics, docs/tactics): less indentation * test(test/tactics): better tests for clear' and clear_dependent We make the tests for `clear'` and `clear_dependent` more meaningful: They now permit less illegal behaviours. * refactor(tactic/clear): simplify error message formatting Co-authored-by: Simon Hudon <simon.hudon@gmail.com> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>