Fin.succAbove

Stream: std4

[Scott Morrison]

What has happened to Fin.succAbove? It used to be in Std, and now is gone. I'm trying to do a dependency bump in Mathlib...

[Mario Carneiro]

It was moved back to mathlib

[Scott Morrison]

I see. I found https://github.com/leanprover/std4/commit/cd11695b18ffc0f91407e48b9084d85a46481f72, where it is deleted.

[Mario Carneiro]

after looking at the lemmas I decided against moving it as it is quite tied up in mathlib notions

[Scott Morrison]

Is there an open PR for adding it to mathlib?

[Mario Carneiro]

yours :)

[Scott Morrison]

I see, it just vanished. :-)

[Mario Carneiro]

you can probably pull it out of mathlib4 history too

[Scott Morrison]

I think we need to work out better coordination for moving stuff back and forth between Std and Mathlib. No problem if things move and then need to move back, but we need a better way for people to know what's going on.

[Mario Carneiro]

I thought that the version prior to std4#173 was never actually aligned to mathlib

[Mario Carneiro]

that was why the lemmas had to be ported in the first place

[Mario Carneiro]

so I would have expected there never to be a mathlib4 version that lacked Fin.succAbove

[Mario Carneiro]

I did not investigate in detail how the std4 bump from last week was finally resolved though since I was conferencing at the time

[Scott Morrison]

No problem! I think I've got everything tracked down. I've put the definitions back in at #5992, still lots of things to fix.

[Scott Morrison]

Ugh, I've just noticed #5847, which does lots of Mathlib refactoring based on changes to Fin in Std4.

[Scott Morrison]

I am going to ignore that for now and try to finish the bump...

[Scott Morrison]

Bump PRs std4#188 looks good to go.

[Scott Morrison]

And #5992 (the bump PR to mathlib4, with many changes to Fin) is building locally so should be ready for review.

[Scott Morrison]

Great, I've updated #5992 to point back to Std4@main.