fix: universe parameter order discrepancy between theorem and def

[leodemoura]

Before this commit, the theorem and def declarations had different
universe parameter orders.
For example, the following theorem:

theorem f (a : α) (f : α → β) : f a = f a := by
  rfl

was elaborated as

theorem f.{u_2, u_1} : ∀ {α : Sort u_1} {β : Sort u_2} (a : α) (f : α → β), f a = f a :=
  fun {α} {β} a f => Eq.refl (f a)

However, if we declare f as a def, the expected order is produced.

def f.{u_1, u_2} : ∀ {α : Sort u_1} {β : Sort u_2} (a : α) (f : α → β), f a = f a :=
  fun {α} {β} a f => Eq.refl (f a)

This commit fixes this discrepancy.

@semorrison @jcommelin: This might be a disruptive change to Mathlib, but it is better to fix the issue asap. I am surprised nobody has complained about this issue before. I discovered it while trying to reduce discrepancies between theorem and def elaboration.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-4408 build failed against this PR. (2024-06-09 01:09:43) View Log
• 💥 Mathlib branch lean-pr-testing-4408 build failed against this PR. (2024-06-09 02:10:08) View Log
• 🟡 Mathlib branch lean-pr-testing-4408 build against this PR was cancelled. (2024-06-10 23:30:38) View Log
• 🟡 Mathlib branch lean-pr-testing-4408 build against this PR was cancelled. (2024-06-10 23:37:45) View Log
• ❌ Mathlib branch lean-pr-testing-4408 built against this PR, but testing failed. (2024-06-11 00:21:09) View Log