Eliminating cases' (for real)

Stream: PR reviews

[Jeremy Tan]

I have now gotten a machine-readable report of all uses of cases' in branch#option2. On the way I encountered seven uses of cases' without with, which is redundant and can always be replaced verbatim with cases.

#21913 makes these replacements.

[Jeremy Tan]

I will wait until #16526 is merged before making further PRs in this direction

[Jeremy Tan]

#21939 deprimes common uses of cases', more than halving the total count

[Jeremy Tan]

#21945 clears up the remainder of the cases' cases left after #16526

[Jeremy Tan]

#21976 halves the cases' count again by replacing single-subgoal instances

[Jeremy Tan]

Can someone merge #21976 before it rots?

[Jeremy Tan]

#22075 manually deprimes (just over) half of the remaining cases'

[Kim Morrison]

I find this thread very difficult to action. I know there are reasonable concerns about some replacements in this direction. It would be much easy, @Jeremy Tan, if you explicitly say "this PR is okay, because I understand concern X and Y, and this does not touch cases affected by those concerns". Otherwise I don't dare reviewing anything without having to check these things myself...

[Jeremy Tan]

Have you read #mathlib4 > The plan to remove cases'?

[Jeremy Tan]

#22079 finishes the job of removing cases'. After these two PRs are merged all that will be left is to write the linter

[Jeremy Tan]

One more! One more!!!

[Kim Morrison]

Jeremy Tan said:

Have you read #mathlib4 > The plan to remove cases'?

Yes, I had. I am asking you to communicate more clearly in future. That in particular includes not assuming that people have read every thread.

[Jeremy Tan]

#21832 is the last PR in this chain, adding the cases' linter

[Jeremy Tan]

#21832 already has maintainer merge. I would like it to be actually merged, and then the cases' case will be solved.

I had to remove cases' in another file again

[Jeremy Tan]

And again, in Data.ENat.Basic!

[Jeremy Tan]

And in RingTheory.Spectrum.Prime.ChevalleyComplexity (and the PR has been placed on the maintainer queue a second time)

[Kim Morrison]

@Jeremy Tan, just feedback as a reviewer: it's helpful if you make it clear to reviewers that you have addressed existing comments without relying on them looking at the diff or git history. As an example, adding a thumbs up emoji to https://github.com/leanprover-community/mathlib4/pull/21832#issuecomment-2712457133 would make life easier for another reviewer coming in "cold".