Generalize instances

Stream: Is there code for X?

[Nir Paz]

Is there something in lean that checks a proof and finds the minimal set of instances used, or something similar to that? It can be really tricky to find what you need in the hierarchy of instances.

[Yury G. Kudryashov]

This was discussed multiple times but AFAIK wasn't implemented

[Kim Morrison]

Alex Best implemented this in Lean 3 but the work was never finished/migrated.

https://www.youtube.com/watch?v=pudd4F749tE

[Yury G. Kudryashov]

@Alex J. Best