mathlib

90659cbe - fix(tactic/core): Make the `classical` tactic behave like `open_locale classical` (#14122)

fix(tactic/core): Make the `classical` tactic behave like `open_locale 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.