a cardinal <= 1 is 0 or 1

Stream: Is there code for X?

[Kevin Buzzard]

import Mathlib

open Cardinal

lemma aargh {c : Cardinal} (h1 : c ≤ 1) (h0 : c ≠ 0) : c = 1 :=
  sorry

[Sébastien Gouëzel]

lemma aargh {c : Cardinal} (h1 : c ≤ 1) (h0 : c ≠ 0) : c = 1 := by
  lift c to ℕ using h1.trans_lt one_lt_aleph0
  norm_cast at h0 h1 ⊢
  omega

[Markus Himmel]

Maybe something like

lemma aargh {c : Cardinal} (h1 : c ≤ 1) (h0 : c ≠ 0) : c = 1 := by
  obtain ⟨m, hm, rfl⟩ := Cardinal.exists_nat_eq_of_le_nat h1
  simp_all
  omega

(or if you want a one-liner, obtain ⟨m|m|m, hm, rfl⟩ := Cardinal.exists_nat_eq_of_le_nat h1 <;> simp at *)

[Kevin Buzzard]

Thanks to both of you!

[Jz Pan]

Maybe you should use docs#Cardinal.lt_one_iff_zero

[Jz Pan]

If it's ≤ 1 and ≠ 0 then it's < 1, you can use the above result directly.

[Eric Wieser]

@Yaël Dillies, is there some trick using covBy or wcovBy here?

[Yaël Dillies]

Nothing easier than what Sébastien suggested, I'm afraid

[Jz Pan]

Yaël Dillies said:

Nothing easier than what Sébastien suggested, I'm afraid

One line shorter:

import Mathlib

open Cardinal

lemma aargh {c : Cardinal} (h1 : c ≤ 1) (h0 : c ≠ 0) : c = 1 := by
  contrapose! h0
  exact lt_one_iff_zero.1 (h1.lt_of_ne h0)

[Jz Pan]

the last line can also be simpa using h1.lt_of_ne h0

[Aaron Liu]

This is something I would use aesop for, if only it worked

[Aaron Liu]

Jz Pan said:

Maybe you should use docs#Cardinal.lt_one_iff_zero

Is there a suitable abstraction that derives this lemma? We have this same lemma for Nat, UInt8 through UInt64, USize, Fin (n + 2), ENat, Cardinal, Ordinal, and Nimber

[Jireh Loreaux]

Probably some combination of docs#SuccAddOrder and docs#CanonicallyOrderedAdd

[Jireh Loreaux]

import Mathlib

lemma lt_one_iff_eq_zero {α : Type*} {x : α} [LinearOrder α] [AddMonoidWithOne α]
    [SuccAddOrder α] [CanonicallyOrderedAdd α] [NeZero (1 : α)] :
    x < 1 ↔ x = 0 := by
  simp [Order.lt_one_iff_nonpos]

example (x : ℕ) : x < 1 ↔ x = 0 := lt_one_iff_eq_zero

open scoped ENat in
example (x : ℕ∞) : x < 1 ↔ x = 0 := lt_one_iff_eq_zero

This doesn't work for Ordinal because we are missing a CanonicallyOrderedAdd instance.

[Jireh Loreaux]

And I guess it wouldn't work for Cardinal anyway because it isn't a SuccAddOrder. :thinking:

[Yury G. Kudryashov]

BTW, docs#CovBy.intCast is about Nat.cast. IMHO, this breaks our naming convention.

[Yury G. Kudryashov]

import Mathlib

open Cardinal

lemma aargh {c : Cardinal} (h1 : c ≤ 1) (h0 : c ≠ 0) : c = 1 := by
  simp_all [← Cardinal.succ_zero, Order.le_succ_iff_eq_or_le]

[Yury G. Kudryashov]

Should we have IsAtom (c : Cardinal) \iff c = 1?

[Matt Diamond]

We have docs#Ordinal.le_one_iff so we could add a parallel lemma for Cardinal, at which point the proof is easy:

import Mathlib

lemma Cardinal.le_one_iff {c : Cardinal} : c ≤ 1 ↔ c = 0 ∨ c = 1 :=
by simpa using Order.le_succ_bot_iff (a := c)

example {c : Cardinal} (h1 : c ≤ 1) (h0 : c ≠ 0) : c = 1 :=
(Cardinal.le_one_iff.mp h1).resolve_left h0