Chore: Replace open scoped Classical with (open scoped Classical in) or (classical)

[kvanvels]

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.

---

[sgouezel]

Personally, I would put it at the start of the proof for simplicity (it's not that it enables classical reasoning, which is always enabled in fact, it's that it provides decidability assumptions for some lemmas that need it, so it's mostly a technical implementation detail IMHO). But putting it in the middle of the proof as you did is also fine.

[kvanvels]

Hmmm, ok. So I was mixing up classical reasoning (the axiom of choice and its consequences) and decidability/computability?

[kvanvels]

I think committed at faux pas. I did some more work in removing some "Classical"s this morning (in new files) and I added them to this pull request. I modified some pretty basic (close to the root) files and my computer was taking forever to compile them. I pushed them here (without thinking it through) to have the servers here compile them.

Should I make a new branch to continue fixing these "classical"s?

[sgouezel]

It's not really a faux pas, but the PR is reaching a critical size, so I think it is a good point to stop there and wait for a review. If you want to go on working on this, you can do it on another branch (either based on this one, or from master).

[sgouezel]

You can also see that there is an "Awaiting-author" label on the PR. This means that the PR will not show up on the reviewers dashboard currently. So, once you are happy with the state of your PR, it is important that you remove this tag, to indicate that your PR is ready for review.

[kvanvels]

There was one final request from your initial review that I just fixed. Am I correct in assuming that that is what removed the "awaiting-author" tag on the PR?

[j-loreaux]

No, you removed the awaiting-author tag (probably by clicking on it). This is fine if and only if you're ready for the PR to be reviewed again, which it seems is the case because all the conversations are marked as resolved.

[j-loreaux]

some pretty minor comments.