[Merged by Bors] - refactor(logic/basic): classical -> root, root -> decidable

[digama0]

This moves all logic lemmas with decidable instances into the decidable namespace, and moves or adds classical versions of these to the root namespace. This change hits a lot of files, mostly to remove the classical. prefix on explicit references to classical lemmas.

[bryangingechen]

Could you add docs on the decidable namespace and classical versions going in the root? I'm not sure whether that would fit best in a library note or a module doc string though.

[digama0]

I thought about leaving the classical.* lemmas there as aliases, this would have decreased the size of the diff a lot, but I think it's better to do the cleanup.

Most likely this PR has caused more lemmas to use classical logic that didn't intend to, since I didn't do a find/replace of root lemmas to decidable.*, only classical.* to root, but it's easier to maintain AC freedom when this is explicitly marked with e.g. the decidable namespace, so it's mostly just a win with smaller proofs and less typeclass searching.

[bryangingechen]

Otherwise LGTM.

[robertylewis]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests