Changes that use merged core PR

Stream: mathlib4

[Peiran Wu]

I made a PR leanprover/lean4#4037 that was merged two days ago and it contained two lemmas. I have things I want to add to Mathlib that use these lemmas. Is there some nightly branch to which I can make a PR now or should I wait just for v4.9.0-rc1?

I suppose the former option would be slightly complicated, as the core PR requires changes to Mathlib that are still on the "lean-pr-testing-4037" branch.

[Matthew Ballard]

I don't think things would make it into mathlib itself until the toolchain changes. I am not sure I would develop on top of nightly but @Kim Morrison or @Ruben Van de Velde might have a better sense of whether this is actually a bad idea or not

[Peiran Wu]

My expectation is for my "second-order" changes to make it into Mathlib after it moves to v4.9.0-rc1. But I felt it would be nice to have a placeholder saying I've already done such and such work and also to receive feedback.

I can also just make a draft PR to the master branch, adding the two lemmas and required changes temporarily, and remove them later.

[Matthew Ballard]

That last approach sounds very sensible to me!

[Ruben Van de Velde]

Yeah, just add the lemmas to your pr when you make it. We'll remove them on nighty-testing when needed. (Just make sure they do match exactly, so we don't have to think about it)