Commit 2025-01-21 01:06 0d80c6dc

chore: replace open scoped Classical with open scoped Classical in or classical (#20501) reduces some technical debt by replacing "open scoped classical" with (open scoped classical in) for theorem declarations and/or adding a "classical' tactic to a tactic proof. I followed the example in PR #20325.