retrieve old lemma

Stream: mathlib4

[Antoine Chambert-Loir]

It seems that a while ago, Set.ncard_coe used to exist, but that it does not exist anymore. How could I find what it did?

[Riccardo Brasca]

There is https://mathlib-changelog.org, but it not finding your lemma.

[Riccardo Brasca]

well, you can always go to any commit at any time. do you have an idea when it existed? like one year ago? two years ago?

[Anatole Dedecker]

It sounds weird because this lemma isn't even found in Mathlib 3 documentation

[Riccardo Brasca]

Anyway, are you sure? I don't find it with git log (but maybe I don't know how to use it)

[Riccardo Brasca]

Note that is exists on the internet, where the author says "Modifications to the Iwasawa pull request by Antoine Chambert-Loir (Chambert-Loir,2024), compared to its state on 2024-05-28"

[Riccardo Brasca]

Indeed you add it in #12048

[Eric Wieser]

I guess the moral here is to split out all your trivial lemmas from large PRs, else you'll go mad wondering where they went in other PRs.

[Antoine Chambert-Loir]

indeed I go mad, but what do you mean precisely?

[Antoine Chambert-Loir]

As a matter of fact, I don't understand how you manage to have a big lean project be safely split out into small PRs, on which many important modifications are made, while keeping the whole stuff OK.

[Yaël Dillies]

That's great, Antoine, because I am in the process of writing a paper on just this :wink:

[Yaël Dillies]

Will let you know when I am at a point where you can reasonably get something from reading it