Tactic to find minimal typeclass

Stream: Is there code for X?

[Vasily Ilin]

Is there a tactic to find the minimal typeclass for a conclusion to hold?
For example, example [LT β] : Refl (List.le (α := β)) := sorry is not true but this is: example [Preorder β] : Refl (List.le (α := β)) := List.le_refl.

[Eric Wieser]

@Alex J. Best had a project for this a while ago, and someone else did more recently

[Ruben Van de Velde]

"for a conclusion to hold", no. "for the given proof to work, assuming you've got a working typeclass already (e.g. Preorder in your case)", that's workable

[Alex J. Best]

@Anand Rao Tadipatri is one of the more recent people whose thought about this.

[Anand Rao Tadipatri]

The proof generalization that @AG and I worked on doesn't handle typeclass generalization at the moment, but I believe @Vlad Tsyrklevich has worked in this direction a bit in Lean4.

[Vlad Tsyrklevich]

Assuming you are starting with a working proof, Jovan had some faster code here #mathlib4 > Linter for generalizing type class hypotheses. I think it may not always find the most general type class, but you could run it to a fixpoint if necessary. There's nothing conveniently packaged up as far as I know.