…e classical` (#14122)

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:
```lean
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 `congr`s can be eliminated with this change.