feat: use approximate universe inverse when sorry in inductive type

[kmill]

This PR modifies the universe level constraint algorithms for the inductive type elaborator to use an approximation for constructor fields that contain sorry. For example, the following used to fail with an 'accidental higher universe' error due to the fact that the sorry's universe level constraint is of the form u ≤ ?r + 1, which is often a mistake.

inductive Sorry1 where
  | x (a : Array Sorry1)
  | y (b : sorry)

The following example also used to fail, since the constraint was ?u ≤ 1, which does not have a unique solution. It now takes the least solution if there is a sorry.

inductive Sorry2 : Type where
| y (b : sorry)

This PR also avoids a spurious 'accidental higher universe' error in the following case, which has the constraints u ≤ ?r + 1 and u ≤ ?r. While the second implies the first, it would still warn about the first.

inductive NotBadLevelConstraint (α : Sort u) (β : Type u) : Type _ where
  | mk (x : α) (y : β)

[robsimmons]

This makes sense based on our discussion and definitely resolves all the cases I was encountering that motivated #11513.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9cbff55c56488a358d9e0c10c81a692d8b1cc860 --onto 455fd0b4488e2adc85f825a52e2ee7d944a5740a. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-05 19:36:11)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 9cbff55c56488a358d9e0c10c81a692d8b1cc860 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-12-05 19:36:13)