mathlib

e1a8b886 - feat(tactic/itauto): add support for [decidable p] assumptions (#10744)

feat(tactic/itauto): add support for [decidable p] assumptions (#10744) This allows proving theorems like the following, which use excluded middle selectively through `decidable` assumptions: ``` example (p q r : Prop) [decidable p] : (p → (q ∨ r)) → ((p → q) ∨ (p → r)) := by itauto ``` This also fixes a bug in the proof search order of the original itauto implementation causing nontermination in one of the new tests, which also makes the "big test" at the end run instantly. Also adds a `!` option to enable decidability for all propositions using classical logic. Because adding decidability instances can be expensive for proof search, they are disabled by default. You can specify specific decidable instances to add by `itauto [p, q]`, or use `itauto*` which adds all decidable atoms. (The `!` option is useless on its own, and should be combined with `*` or `[p]` options.)