chore(combinatorics/*): Fix lint

[YaelDillies]

Fix the linting errors coming from fintype_finite, to_additive_doc and doc_blame. Pull out a [projective_plane P L] assumption to a variables declaration in combinatorics.configuration.

---

[b-mehta]

This PR also adds additional variable declarations, and changes some proofs (in ways which aren't just renames and fixes). Please add this to be PR description.

[YaelDillies]

The changes to the proof are just adding casesI nonempty_fintype _, as preconized by the fintype_finite linter.

[b-mehta]

There's also the anti-golf in the proof of one_lt_order, and a different proof in coloring.color_classes_finite.

[YaelDillies]

This is all just fintype_finite:

• The "anti-golf" is required because the previous proof was creating another metavariable midway that appeared in a fintype instance. Now that I need to promote the finite instance to the fintype one, I cannot afford to leave this metavariable.
• The different proof for coloring.color_classes_finite is because the previous one was calling the fintype V assumption.

[jcommelin]

bors merge p=3

[bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests