feat: Upstream derive handler for ToExpr from Mathlib

[alexkeizer]

This takes the derive handler for ToExpr from mathlib, and upstreams it into core.

The derive handler uses an auxiliary typeclass, ToLevel to ensure the derived ToExpr instances are properly universe polymorphic (when the original type is polymorphic), so we upstream this, too.

/-- A class to create `Level` expressions that denote particular universe levels in Lean.
`Lean.ToLevel.toLevel.{u}` evaluates to a `Lean.Level` term representing `u` -/
class ToLevel.{u} where
  /-- A `Level` that represents the universe level `u`. -/
  toLevel : Level
  /-- The universe itself. This is only here to avoid the "unused universe parameter" error. -/
  univ : Type u := Sort u

Credit goes to @kmill for originally developing the derive handler. We'll use this in a light-weight, basic QQ alternative that currently lives in a PR to LNSym, but we plan to upstream also.

[kmill]

Thanks for your interest Alex — upstreaming this has been on my radar for awhile, especially since #expr now uses ToExpr instances. However, for upstreaming, please be sure to run your plans by core developers ahead of time. It's still not clear how this ToExpr deriving handler will appear in core, and it has some issues that will likely need more core fixes (for example, ToLevel should not need to live in a universe above Type, yet it does).

[alexkeizer]

Thanks for your input, Kyle. For the record, I did mention, quite a while back, on the Zulip that I'd like to have ToExpr available in core, and got as response that this seemed like a good idea. Admittedly, I didn't follow up on that saying I would do it (since I wasn't planning to at the time), but recently figured I might as well get that ball rolling myself. I'll communicate this more clearly in the future.

[alexkeizer]

I've opened an issue to track the discussion at #5909