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

[kmill]

Great, the ToExpr RFC was just accepted — looking forward to seeing progress on this!

[alexkeizer]

Wonderful! I'm currently on vacation, but will push this forward when I'm back on the 25th!

By the way, where did this acceptance happen? I didn't see any activity on the issue.

[kmill]

It looks like there's a gap in FRO communication here — the triage team accepted it on Thursday and assigned to me seeing that it gets implemented.

I'd suggest that we do two PRs here. One would be adding ToLevel and fixing all the currently existing ToExpr handlers, and then the second would be this PR, upstreaming the ToExpr handler. Does that sound reasonable? (No need to respond until you get back!)

[alexkeizer]

@kmill Thanks for clarifying. Splitting it into 2 PRs makes sense to me!

For the first PR, should I upstream the ToLevel class as-is, or should I use the alternative definition I proposed in #5909 to avoid the universe bump?

[kmill]

We should use the improved ToLevel since we definitely don't want the universe bump.

[alexkeizer]

I've opened a PR to upstream ToLevel at #6285