mathlib

6623e6af - fix(*): add missing `classical` tactics and `decidable` arguments (#18277)

fix(*): add missing `classical` tactics and `decidable` arguments (#18277) As discussed in [this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60classical.60.20attribute.20leakage/near/282726128), the `classical` tactic is buggy in Mathlib3, and "leaks" into subsequent declarations. This doesn't port well, as the bug is fixed in lean 4. This PR installs a temporary hack to contain these leaks, fixes all of the correponding breakages, then reverts the hack. The result is that the new `classical` tactics in the diff are not needed in Lean 3, but will be needed in Lean 4. In a future PR, I will try committing the hack itself; but in the meantime, these files are very close to (if not beyond) the port, so the sooner they are fixed the better.