feat: generalize panic to Sort

[tydeu]

This PR generalizes the panic functions to a type of Sort u rather than Type u. This better supports universe polymorphic types and avoids confusing errors.

An minimal (but somewhat contrived) example of such a confusing error is:

/-
stuck at solving universe constraint
  ?u.59+1 =?= max 1 ?u.7
while trying to unify
  Subtype.{?u.7} P : Sort (max 1 ?u.7)
with
  Subtype.{?u.7} P : Sort (max 1 ?u.7)
-/
def assertSubtype! {P : α → Prop} [Inhabited (Subtype P)] (a : α) [Decidable (P a)] : Subtype P := -- errors on :=
  if h : P a then 
    ⟨a, h⟩ 
  else 
    panic! "Property not satisified"

[leanprover-community-bot]

Mathlib CI status (docs):

• 🟡 Mathlib branch lean-pr-testing-6333 build against this PR was cancelled. (2024-12-08 01:09:04) View Log
• ✅ Mathlib branch lean-pr-testing-6333 has successfully built against this PR. (2024-12-10 06:05:30) View Log