[Merged by Bors] - fix(tactic/core): Make the classical tactic behave like open_locale classical

[eric-wieser]

This renames the existing classical tactic to classical!, and adds a new classical tactic that is equivalent to open_locale classical.

Comparing the effects of these:

import tactic.interactive
import tactic.localized

-- this uses the noncomputable instance
noncomputable def foo : decidable_eq ℕ :=
λ m n, begin classical!, apply_instance, end

def bar : decidable_eq ℕ :=
λ m n, begin classical, apply_instance, end

section
open_locale classical

def baz : decidable_eq ℕ :=
λ m n, by apply_instance

end

example : baz = bar := rfl

In a few places classical was actually just being used as a resetI. Only a very small number of uses of classical actually needed the more aggressive classical! (there are roughtly 500 uses in total); while a number of congrs can be eliminated with this change.

---

[fpvandoorn]

Note: if this works, we probably want to mimic open_locale classical even better, which does a little more

[eric-wieser]

Alternatively, we might want to just remove those lines from the classical locale; it's not immediately clear to me what purpose they serve.

[eric-wieser]

Oh, actually decidable_eq_of_decidable_le has been de-instanced upstream anyway

[fpvandoorn]

Presumably it is to deal with performance issues causes by those instances. But the de-instantiated instances should of course be removed.

[fpvandoorn]

This looks great!

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests