[Merged by Bors] - feat: four small lemmas about successors of finite cardinals

[grunweg]

Co-authored-by: @fpvandoorn

[grunweg]

Actually, I wonder if the right decision is "remove the first two lemmas" instead...

[fpvandoorn]

I added comments in the Zulip thread

[fpvandoorn]

A lemma Cardinal.succ_eq_of_lt_omega would probably also useful (I think you can guess the statement from the name)

[grunweg]

A lemma Cardinal.succ_eq_of_lt_omega would probably also useful (I think you can guess the statement from the name)

I agree, but I don't find that easy to prove. (It's also the first time I'm seriously looking at the library for cardinals and ordinals.) There is a proof using more advanced tools:

import Mathlib.SetTheory.Cardinal.Ordinal
set_option autoImplicit false
open scoped Cardinal
lemma Cardinal.succ_eq_of_lt_aleph0 {c : Cardinal} (hc : ℵ₀ ≤ c): c + 1 = c := by
  rw [Cardinal.add_eq_max hc]
  exact max_eq_left (aleph0_le.mp hc 1)  

aleph0_le is in Cardinal.Basic, but inlining add_eq_max and related lemmas is tedious. For instance, here is the proof of add_eq_max inlined - and that's not even close to it.

lemma Cardinal.succ_eq_of_lt_aleph0 {c : Cardinal} (hc : ℵ₀ ≤ c): c + 1 = c := by
  apply le_antisymm _ (self_le_add_right c 1)
  have h1 : 1 ≤ c := aleph0_le.mp hc 1
  -- this requires inlining lots of `mul` lemmas, or a new proof
  have b : c + c = c := sorry
  nth_rw 2 [← b]
  exact add_le_add (le_refl c) h1

I could add the lemma to Ordinal, but that feels way too specialised compared to the lemmas there. What do you think?
(My current preference is to add a comment in Basic - unless there is better proof which could go in Basic.)

[grunweg]

I have used your proofs and golfed the special case (n=1).
awaiting-review

[fpvandoorn]

Note that in Cardinal, we distinguish between add_one and succ, because they're not the same for infinite cardinals.
Cardinal.add_one_eq already exists, as do many other similar lemmas. The proof uses ordinals, and so was probably in a file you didn't import...

For the lemma Cardinal.succ_eq_of_lt_aleph0 (sorry, I forgot that Cardinal.omega was renamed to Cardinal.aleph0 a while back), I want (h : c < \aleph\_0) : Order.succ c = c + 1, which is a combination of the lemma in this PR and
Cardinal.lt_aleph0.

Can you add that?

Other than that, LGTM
bors d+

[mathlib-bors]

✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[fpvandoorn]

(please update PR title)

[grunweg]

Don't worry, figured out the renaming. (omega still exists, but as ordinal number...)
That lemma you mentioned seems easy to prove, added. Thanks for all the input!
bors r+

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style