mathlib3

22790e06 - feat(tactic): new tactics to normalize casts inside expressions (#988)

feat(tactic): new tactics to normalize casts inside expressions (#988) * new tactics for normalizing casts * update using the norm_cast tactics * minor proof update * minor changes * moved a norm_cast lemma * minor changes * fix(doc/tactics): make headers uniform * nicer proof using discharger * fixed numerals handling by adding simp_cast lemmas * add documentation * fixed unnecessary normalizations in assumption_mod_cast * minor proof update * minor coding style update * documentation update * rename flip_equation to expr.flip_eq * update proofs to remove boiler plate code about casts * revert to old proof * fixed imports and moved attributes * add test file * new attribute system - the attribute norm_cast is split into norm_cast and norm_cast_rev - update of the equation flipping mechanism - update of the numerals handling * syntax fix * change attributes names * test update * small update * add elim_cast attribute * add examples for attributes * new examples