reenableeta

Stream: lean4

[Scott Morrison]

@Gabriel Ebner, despite your WIP draft PR !4#3414 having description "These aren't the commits you're looking for", during the porting meeting today we went looking for them. (Also the underlying lean4 changes at https://github.com/leanprover/lean4/compare/master...gebner:lean4:reenableeta.)

This came up when we were looking at the slow isDefEq problem discussed at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/LinearAlgebra.2EDeterminant.20!4.233694.

Would you be able to give us a quick update on the status of this branch, and the prospects for it going somewhere? Obviously it would be lovely if it worked, but maybe there are reasons to curb our enthusiasm?