Default arguments in typeclasses

Stream: mathlib4

[Yury G. Kudryashov]

We often use default arguments in typeclasses with forgetful inheritance. While this is convenient in many cases, this is also a footgun. E.g., https://github.com/leanprover-community/mathlib4/actions/runs/10642487250/job/29504957359?pr=16348 failed because of a non-defeq diamond introduced by docs#subsetConditionallyCompleteLinearOrder and docs#ConditionallyCompleteLinearOrder.toLinearOrder : they don't set projection to Ord correctly.

[Yury G. Kudryashov]

I suggest that we drop the default values and create custom constructors like docs#UniformSpace.ofCore instead.

[Eric Wieser]

An alternative would be something like #12608, where relying on defaults emits a warning

[Yury G. Kudryashov]

@Yaël Dillies The diamond I mentioned in #16348 is described above.