lean#282 changing structure instance elaboration

Stream: PR reviews

[Gabriel Ebner]

This is a somewhat large and fundamental change, but it fixes two bugs (I can't tell whether the bugs are annoying or not). There are some changes to mathlib necessary: https://github.com/leanprover-community/mathlib/compare/si

[Scott Morrison]

Thank you so much for tracking down all the problems in mathlib!

[Scott Morrison]

I would really love to see these bugs in Lean fixed.

[Scott Morrison]

And that level of changes required in mathlib seems like a small price to pay.

[Scott Morrison]

Hopefully some of the mathlib changes can still be cleaned up or refactored further. I won't have a chance tomorrow, but I'd be very happy to see this as part of the Lean 3.15 PR. :-)

[Kevin Buzzard]

I too would love to see these bugs fixed. Having $\in$ randomly unfolding to set.mem confuses newcomers.

[Gabriel Ebner]

Ok, then it is decided.