style: `.some`/`.none` vs `some`/`none`

Stream: mathlib4

[Jovan Gerbscheid]

I've made a PR replacing .some/.none with some/none whenever possible (#27896). The reason for this change is as follows:

• .some has to figure out the expected type T, and then elaborates to T.some.
• some always elaborates to Option.some.

So, when I'm reading code that says .some, I need to think about what the expected type is in order to figure out what constant this elaborates to. On the other hand with some I immediately know what it means. And some has the added benefit of being 1 character shorter.

I think the same logic applies to other inductive constructors that live in the global namespace, such as true and false. It always makes more sense to write true/false than .true/.false.

Should this be added to some style guide?