mathlib3

5c093726 - A `ring_exp` tactic for dealing with exponents in rings (#1715)

A `ring_exp` tactic for dealing with exponents in rings (#1715) * Test for ring_exp * Implement -a/b * -a/b = a/b * a/b * Hide extra information in the `ex` type in `ex_info` * Some attempts to make the proof returned by ring_exp shorter * Fix that ring_exp wouldn't handle pow that isn't monomial.has_pow * Some optimizations in ring_exp * Make all proofs explicit, halving execution time more or less * Cache `has_add` and `has_mul` instances for another 2x speedup * ring_exp can replace ring to compile mathlib * Revert `ring` to non-test version * Code cleanup and documentation * Revert the test changes to `linarith` * Undo the test changes to `ring2` * Whitespace cleanup * Fix overzealous error handling Instead of catching any `fail` in eval, we just catch the operations that can safely `fail` (i.e. `invert` and `negate`). This should make internal errors visible again. * Fix the TODO's * Example use of ring_exp in data.polynomial * Check that `ring_exp` deals well with natural number subtraction * Fix incorrect docstring * Improve documentation * Small stylistic fixes * Fix slow behaviour on large exponents * Add `ring_exp` to the default tactics * Use applicative notation where appropriate * The `ring_exp` tactic also does normalization Co-Authored-By: Rob Lewis <Rob.y.lewis@gmail.com> * Move `normalize` from `tactic.interactive` to `ring_exp` namespace * Fix name collision between `equiv` in data.equiv.basic and `equiv` in `test/tactics.lean` I just renamed the definition in `test/tactics.lean` to `my_equiv` and the operator to `my≅`. * Fixes for the linter * Fix the usage of type classes for `sub_pf` and `div_pf` * Fix an additional linting error * Optimization: we don't need norm_num to determine `x * 1 = x` * Improve documentation of `test/ring_exp.lean` * Rename `resolve_atoms` to `resolve_atom_aux` for clarity * Small stylistic fixes * Remove unneccessary hidden fields to `ex` * Control how much unfolding `ring_exp` does by putting a `!` after it * Reword comment for `ex_type` * Use `ring_exp!` to deal with `(n : ℕ) + 1 - 1 = n` * Document the `!` flag for `ring`, `ring_exp` and `ring_exp_eq` * Get rid of searching for another cached instance * Fix `ring_exp` failing on terms on the form `0^succ (succ ...)`