fix: discrepancy theorem vs example

[leodemoura]

When the type of an example is a proposition,
we should elaborate on them as we elaborate on theorems.
This is particularly important for examples that are often
used in educational material.

Recall that when elaborating theorem headers, we convert unassigned
universe metavariables into universe parameters. The motivation is
that the proof of a theorem should not influence its statement.
However, before this commit, this was not the case for examples when their type was a proposition.
This discrepancy often confused users.

Additionally, we considered extending the above behavior to definitions when
1- When their type is a proposition. However, it still caused disruption in Mathlib.
2- When their type is provided. That is, we would keep the current behavior only if : <type> was omitted. This would make the elaborator for def much closer to the one for theorem, but it proved to be too restrictive.
For example, the following instance in Core.lean would fail:

instance {α : Sort u} [Setoid α] : HasEquiv α :=
  ⟨Setoid.r⟩

and we would have to write instead:

instance {α : Sort u} [Setoid α] : HasEquiv.{u, 0} α :=
  ⟨Setoid.r⟩

There are other failures like this in the core, and we assume many more in Mathlib.

closes #4398
closes #4482 Remark: PR #4482 implements option 1 above. We may consider it again in the future.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-4493 build failed against this PR. (2024-06-20 00:40:05) View Log
• 💥 Mathlib branch lean-pr-testing-4493 build failed against this PR. (2024-06-20 01:32:42) View Log
• ❌ Mathlib branch lean-pr-testing-4493 built against this PR, but testing failed. (2024-06-24 01:31:16) View Log

[kim-em]

Mathlib should be working now (it was an example which really was "wrong": from the statement it looks like it was more universe polymorphic than the proof actually allowed).