Commit 2024-12-30 19:50 1dce20e0

chore: Replace open scoped Classical with open scoped Classical in or classical (#20325) I haven't done all the files, but a fair number of them. The only changes in this PR are:

• Replace open scoped Classical with open scoped Classical in (when needed for the statement) or classical in proofs.
• Some term mode proofs with if have been converted to tactic mode proofs with by_cases.
• Some adjacent open ... statements have been merged into a single open ...