mathlib

fe9d7ff4 - feat(tactic/nat_cases): a tactic to case bash inequalities on natural numbers (#1596)

feat(tactic/nat_cases): a tactic to case bash inequalities on natural numbers (#1596) * starting on finset_cases * looking pretty nice * moving lemma that rewrites nat.add back to (+) * update tactics.md * cleanup * suggestions from review * Update src/tactic/fin_cases.lean Co-Authored-By: semorrison <scott@tqft.net> * incomplete implementation of `with` syntax * looks good * failed attempt to use unification * test showing elaboration problem * elaborating the `with` argument with respect to the expected type * testing the type of A in `x ∈ A` using unification rather than syntactic matching * refactor and cleanup * refactor * initial start on nat_cases * initial start on nat_cases * resuming work on nat_cases * looks reasonable * documentation * reverting bad merge in fin_cases * fix module comment * move non-meta lemmas * add tests for Chris' use case * cleanup * oops * starting on fintype instances for Icos * finishing fintypes * minor * not really sure what to do next * oops, forgot to commit?? * oops * bit more work * more progress * everything works? * moving everything to their natural homes * rearrange * cleanup * linting * doc-strings * merge two interactive tactics, via `using` keyword * improve documentation, in response to review * add interval_cases to tactic.default * Apply suggestions from code review Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>