Junyan Xu

Two examples that don't crash ``` variable {R A : Type} (r : R) (a : A) {f : R → A} (hf : f r = a) structure Subalgebra...

It turns out the issue occurs much earlier than I expected: it's already present in 4.0.0-m2 (3 years ago), while 4.0.0-m1 can't compile this file. ``` > elan run --install...

My realization from [this observation](https://github.com/leanprover-community/mathlib4/pull/7695#discussion_r1360708272) is that, when you have an instance `C.{u,max u v}` that will never file due to this issue, create instead a `C.{u,u}` instance and a...

The same trick can be used to deal with constraints of the form `a ≤ b+1`, but the solution for `a+1 ≤ b`. (Not sure whether they come up in...

Actually, UnivLE seems to be the best solution as it only requires one instance for each of the three cases above: ``` set_option autoImplicit true @[pp_with_univ] abbrev UnivLE.{u, v} :...

Yeah, I wasn't following when UnivLE was developed and I'm certainly rediscovering some considerations you had :-) Your choice to use `max u v` was based on a misconception (that...

lmsys's Elo rating approach is interesting. See also https://gpt4all.io/index.html, "Performance Benchmarks" (displayed only on desktop, not on mobile) https://www.mosaicml.com/blog/mpt-7b, Table 1 for some comprehensive benchmarking results.

I think it's okay to make the PR point to a dependent branch in order to reduce diffs, making it immediately reviewable without using [another link](https://github.com/leanprover-community/mathlib4/compare/datokrat/FME-100...datokrat/FME-99), but you'd better change...

Thanks but note that generalized maxDegree API is almost ready at https://github.com/leanprover-community/mathlib4/compare/supDegree_LinearOrder

~~Because the diff from #7229 is large, maybe it's not a good time to review ...~~ #7229 is now merged!