Lemmas to handle part_enat.card, #19198

Stream: PR reviews

[Antoine Chambert-Loir]

In PR #19198, I prove a bunch of lemmas analogous to those existing for nat.card that allow to work with docs#part_enat.card

[Antoine Chambert-Loir]

I wrote the companion PR !4#5307 for mathlib4.

(Lint complains there are lines with “by” only; they were created by mathport, how should I format them?)

[Floris van Doorn]

put by at the end of the previous line.

[Scott Morrison]

(sometimes this requires also breaking the previous line, and then you need to remember the "type signature gets indented by 4 spaces" rules.)

[Yury G. Kudryashov]

@Antoine Chambert-Loir You forgot to update SHA sums, so these files are still on the #outofsync list. Could you please create a new PR that updates SHA sums and mention the old PR in the description?

[Antoine Chambert-Loir]

I don't know how to do that! If you give me (even approximate) instructions, I'll do it.

[Yury G. Kudryashov]

You open a PR, then go over the list of files touched by your old PR and replace the SHA sum in the header (line 7) with the one found at https://leanprover-community.github.io/mathlib-port-status/file/data/nat/part_enat (and similarly for other files). Most probably, you'll need 3ff3f2d6a3118b8711063de7111a0d77a53219a8 in all your files.

[Antoine Chambert-Loir]

Done : #5799