bunch of lemmas to upstream

Stream: Is there code for X?

[Jakob von Raumer]

Hi all, I have a bunch of lemmas I could PR to mathlib, if they're deemed worthy, should I just post them here to make sure I haven't missed them being already included somehow?

[Yaël Dillies]

You can simply open a PR and we'll tell you

[Jakob von Raumer]

(kind of wanted to avoid unnecesarily doing work of trying to find the right files to fit them in etc)

[Ruben Van de Velde]

Do you know about #find_home?

[Jakob von Raumer]

Oh wow, that's brilliant! :grinning:

[Jakob von Raumer]

Is there a linter or command in order to generalize type class assumptions (some of the stuff is phrased in terms of ℝ right now, even if it's probably applicable to some class of ordered semirings or so)

[Johan Commelin]

Hmm, @Alex J. Best had some tools in that direction, but that was Lean 3...

[Ruben Van de Velde]

I would very much like that to come back as well :innocent:

[Jakob von Raumer]

Ruben Van de Velde said:

Do you know about #find_home?

Pretty wild suggestions for some parts though :sweat_smile:

[Jakob von Raumer]

Yaël Dillies said:

You can simply open a PR and we'll tell you

Did so at #12726 :)

[Jakob von Raumer]

Since @David Loeffler 's reply sounded that way: Should mathematically uninteresting lemmas that are currently not used in mathlib but instead in FV projects, rather go somewhere else but mathlib?

[Ruben Van de Velde]

It seems like there was a bit of miscommunication there. I think all of these lemmas would be welcome, but reviewer time is scarce, so anything you can do to make it easier on reviewers is helpful. One thing you can do is keeping each PR covering a single "idea" - required reviewer effort scales much faster than linearly with the number of independent changes in a PR

[David Loeffler]

I agree with Ruben here – the lemmas are certainly mathlib-worthy, but the way the PR is currently written makes the review process unnecessarily hard. (FWIW, I had already posted on Jakob's PR to this effect, before his comment here was posted.)

[Yaël Dillies]

Especially because David is right that I don't have infinite time (especially right now, it's exam season) and it would help a lot if I could get the lemmas I agree with (most of them) and leave the few I disagree with for others to decide

[Yury G. Kudryashov]

E.g., if you open a separate PR with your Option.get!_* lemmas, then we'll merge it very quickly.