cardinal.le_of_add_le_add

Stream: Is there code for X?

[Andrew Yang]

Do we have any of the following somewhere?

/- This seems to be the right generality. -/
example {α β γ : cardinal} (h : γ < cardinal.aleph_0) (h : α + γ ≤ β + γ) : α ≤ β := sorry
/- I have a lousy lean proof for this -/
example {α β : cardinal} (h : α + 1 ≤ β + 1) : α ≤ β := sorry
/- This is what I actually need -/
example {α β : cardinal} (h : α + 1 = β + 1) : α = β := sorry

[Yaël Dillies]

I think we have neither.

[Damiano Testa]

As for your final example, I do not know if this counts as lousy, but here is a proof:

import set_theory.cardinal.ordinal

example {α β : cardinal} (h : α + 1 = β + 1) : α = β :=
begin
  wlog ab : α ≤ β,
  by_cases α₀ : cardinal.aleph_0 ≤ α;
  by_cases β₀ : cardinal.aleph_0 ≤ β,
  { rwa [cardinal.add_one_eq α₀, cardinal.add_one_eq β₀] at h },
  { exact (lt_irrefl β ((not_le.mp β₀).trans_le (α₀.trans ab))).elim },
  { rwa cardinal.add_one_eq β₀ at h,
    subst h,
    rcases cardinal.lt_aleph_0.mp (not_le.mp α₀) with ⟨n, rfl⟩,
    exact ((not_lt.mpr β₀) (cardinal.lt_aleph_0.mpr ⟨n + 1, by simp⟩)).elim },
  { rcases cardinal.lt_aleph_0.mp (not_le.mp α₀) with ⟨m, rfl⟩,
    rcases cardinal.lt_aleph_0.mp (not_le.mp β₀) with ⟨n, rfl⟩,
    exact nat.cast_inj.mpr (nat.succ_injective (nat.cast_inj.mp h)) },
end

(I never used the cardinal API before, but was curious to try it and your examples were good excuses! :smile: )

[Damiano Testa]

It seems that the cardinal API revolves around using < aleph_0 instead of casting nats:

lemma succ_inj {α β : cardinal} : α + 1 = β + 1 ↔ α = β :=
⟨λ h, cardinal.eq_of_add_eq_add_right h one_lt_aleph_0, λ h, congr_fun (congr_arg (+) h) 1⟩

[Andrew Yang]

Ah I didn't know that docs#cardinal.eq_of_add_eq_add_right exists. Thanks.
My proof of α + 1 ≤ β + 1→ α ≤ β is by constructing the injection explicitly, so your approach is definitely better.
By the way, I think α.succ and α + 1 are not the same thing (regarding the name of your lemma).

[Ruben Van de Velde]

docs#cardinal.succ_order agrees:

Note that the successor of c is not the same as c + 1 except in the case of finite c.

[Damiano Testa]

In case it helps, these are proofs of the statements that you mentioned:

lemma add_one_inj {α β : cardinal} : α + 1 = β + 1 ↔ α = β :=
⟨λ h, cardinal.eq_of_add_eq_add_right h one_lt_aleph_0, λ h, congr_fun (congr_arg (+) h) 1⟩

lemma le_of_add_le_add_of_lt_aleph_0 {α β γ : cardinal}
  (γ₀ : γ < cardinal.aleph_0) (h : α + γ ≤ β + γ) :
  α ≤ β :=
begin
  by_cases β₀ : aleph_0 ≤ β,
  { rw add_eq_left β₀ (γ₀.le.trans β₀) at h,
    exact le_self_add.trans h },
  { rcases lt_aleph_0.mp (not_le.mp β₀) with ⟨b, rfl⟩, clear β₀,
    rcases lt_aleph_0.mp γ₀ with ⟨c, rfl⟩, clear γ₀,
    have : α < aleph_0 := le_self_add.trans_lt (h.trans_lt (lt_aleph_0.mpr ⟨b + c, by simp⟩)),
    rcases lt_aleph_0.mp this with ⟨a, rfl⟩, clear this,
    rw [← nat.cast_add, ← nat.cast_add] at h,
    exact nat_cast_le.mpr (le_of_add_le_add_right (nat_cast_le.mp h)) }
end

example {α β : cardinal} (h : α + 1 ≤ β + 1) : α ≤ β :=
le_of_add_le_add_of_lt_aleph_0 one_lt_aleph_0 h

[Damiano Testa]

Ah, I missed the "not c + 1" bit! I renamed the lemma above!

[Junyan Xu]

golf:

import set_theory.cardinal.ordinal
open cardinal

lemma add_right_inj_of_lt_aleph_0 {α β γ : cardinal} (γ₀ : γ < aleph_0) :
  α + γ = β + γ ↔ α = β :=
⟨λ h, cardinal.eq_of_add_eq_add_right h γ₀, λ h, congr_fun (congr_arg (+) h) γ⟩

lemma add_one_inj {α β : cardinal} : α + 1 = β + 1 ↔ α = β :=
add_right_inj_of_lt_aleph_0 one_lt_aleph_0

lemma add_le_add_iff_of_lt_aleph_0 {α β γ : cardinal} (γ₀ : γ < aleph_0) :
  α + γ ≤ β + γ ↔ α ≤ β :=
begin
  refine ⟨λ h, _, λ h, add_le_add_right h γ⟩,
  contrapose h,
  rw [not_le, lt_iff_le_and_ne, ne] at h ⊢,
  exact ⟨add_le_add_right h.1 γ, mt (add_right_inj_of_lt_aleph_0 γ₀).1 h.2⟩,
end

example {α β : cardinal} (h : α + 1 ≤ β + 1) : α ≤ β :=
(add_le_add_iff_of_lt_aleph_0 one_lt_aleph_0).mp h

[Damiano Testa]

Very nice!

I wonder if this version of injectivity is also useful:

@[simp] lemma add_nat_inj {α β : cardinal} (n : ℕ) :
  α + n = β + n ↔ α = β :=
⟨λ h, cardinal.eq_of_add_eq_add_right h (nat_lt_aleph_0 n), λ h, congr_fun (congr_arg (+) h) n⟩

[Damiano Testa]

To avoid leaving this one hanging, I PRed these lemmas: if anyone wants to add/change stuff, feel free to do so!

#16262

[Andrew Yang]

Thanks!
I think the add_nat and add_one versions of le can also be useful (potentially also as simp lemmas?)

[Damiano Testa]

Just added them!

[Damiano Testa]

We are also lucky enough that one of the hoskinson machines is taking care of building mathlib! :upside_down: