Commit 2023-01-24 23:10 6623e6af

fix(*): add missing classical tactics and decidable arguments (#18277) As discussed in this Zulip thread, 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.