Linter for overly specific typeclass assumptions?

Stream: mathlib4

[Geoffrey Irving]

Say I write a lemma for variables in a LinearlyOrderedField, but actually the same lemma and proof works if we weaken the hypotheses to LinearlyOrderedSemifield. Is there a linter that can notice mistakes of this type?

[Eric Rodriguez]

@Alex J. Best made such a linter in lean3, not sure if it's ported

[Yury G. Kudryashov]

Most probably, no.

[Kim Morrison]

Talk, paper, but I can't actually find the code right now. I definitely ran it myself in mathlib3 days, so it was usable by other-than-Alex.

I'm pretty sure that if someone wanted to port/rewrite this for Lean 4 everyone would be happy.

[Alex J. Best]

https://github.com/alexjbest/lean-generalisation is the code. I would be very happy to assist someone in porting / rewriting a simplified version to Lean 4 for example (with the idea that a simple version might be more useful (less false positives)).

[Alex J. Best]

I don't really have time myself to write a port right now, as much as I'd love to. It really isn't all that complicated though (especially if you have an ok DAG library already)

[Geoffrey Irving]

Cool that this at least used to exist!