Wrong cardinal theorem names

Stream: mathlib4

[Nir Paz]

Are these 2 theorems in SetTheory/Cardinal/Ordinal.lean named wrong?

theorem add_nat_le_add_nat_iff_of_lt_aleph_0 {α β : Cardinal} (n : ℕ) : α + n ≤ β + n ↔ α ≤ β

theorem add_one_le_add_one_iff_of_lt_aleph_0 {α β : Cardinal} : α + 1 ≤ β + 1 ↔ α ≤ β

I think they should be

theorem add_nat_le_add_nat_iff {α β : Cardinal} (n : ℕ) : α + n ≤ β + n ↔ α ≤ β

theorem add_one_le_add_one_iff {α β : Cardinal} : α + 1 ≤ β + 1 ↔ α ≤ β

Just wanted to make sure I'm not missing something before changing them.

[Riccardo Brasca]

Yes, the names look wrong.

[Yury G. Kudryashov]

These were added by @Damiano Testa in !3#16262. I guess, draft versions had extra assumptions. Could you please submit a PR that

• fixes the names;
• adds @[deprecated] alias old_name := new_name?

[Nir Paz]

Yea I'll do that.

[Damiano Testa]

I think that these were copy-pasted from their brothers add_le_add_iff_of_lt_aleph_0 that really had the lt_aleph_0 assumption. I must have added nat to the name, but left in the lt_aleph_0.

Thanks for catching this!

[Nir Paz]

#10465

[Nir Paz]

I hope it's ok I made a pr before CI finished

[Damiano Testa]

There is also an awaiting-CI tag, in case you want to use it, but I do not think that it is necessary.

[Yury G. Kudryashov]

Delegated to @Damiano Testa

[Eric Wieser]

Nir Paz said:

I hope it's ok I made a pr before CI finished

This is not only totally fine, but often the preferred thing to do