fix: discrepancy in the elaborators for theorem, def, and example

[leodemoura]

When the type of a definition or 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 definitions and
examples when their type was a proposition. This discrepancy often confused users.

Additionally, we considered extending the above behavior whenever
the type of a definition is provided. That is, we would keep the
current behavior only if : <type> was omitted in a definition.
However, this 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

@semorrison @jcommelin: what do you think?

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-4482 build failed against this PR. (2024-06-17 23:06:47) View Log
• 💥 Mathlib branch lean-pr-testing-4482 build failed against this PR. (2024-06-17 23:58:00) View Log
• 💥 Mathlib branch lean-pr-testing-4482 build failed against this PR. (2024-06-24 01:24:55) View Log
• 💥 Mathlib branch lean-pr-testing-4482 build failed against this PR. (2024-06-24 02:29:30) View Log
• 💥 Mathlib branch lean-pr-testing-4482 build failed against this PR. (2024-06-24 02:51:39) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 18c97926a13bfc82c9266bf00483ab13c6acb64f --onto 49249b91074a8eab8926308cedc2b3e31d973b51. (2024-06-27 01:03:22)

[kim-em]

This would be great. I'll take a look at Mathlib.

There are problems in Mathlib, but they are mostly things that deserve to be fixed. Unfortunately the error messages are terrible, and it's completely unclear that the proofs are being rejected because they specialize the universe variables in the statement.

[kim-em]

A typical example of an unhelpful error message is:

example (X : TopCat) (F : Presheaf CommRingCat X)
    (h : Presheaf.IsSheaf (F ⋙ (forget CommRingCat))) :
    F.IsSheaf :=
(isSheaf_iff_isSheaf_comp (forget CommRingCat) F).mpr h

which fails with

type mismatch
  (isSheaf_iff_isSheaf_comp (forget CommRingCat) ?m.3480).mpr ?m.3884
has type
  ?m.3480.IsSheaf : Prop
but is expected to have type
  F.IsSheaf : Prop

giving no clue that the fix is:

example (X : TopCat.{u₁}) (F : Presheaf CommRingCat.{u₁} X)
    (h : Presheaf.IsSheaf (F ⋙ (forget CommRingCat))) :
    F.IsSheaf :=
(isSheaf_iff_isSheaf_comp (forget CommRingCat) F).mpr h

[kim-em]

It turns out that that class of inscrutable error was actually very rare in Mathlib.

Instead I found many instances where authors had implicitly constrained universes via the RHS of the := in ways that were confusing and impossible to see from the type signature. I'm going to backport all the Mathlib fixes to master regardless of whether/when we merge this, but +1 from me!