Cardinal = 2 -> can't have 3 different elements

Stream: new members

[Weiyi Wang]

Just to show my effort, behold my ugly code

theorem eq_of_card2.{u} {α : Type u} (h : Cardinal.mk α = 2) {x y z: α} (hx : x ≠ z) (hy : y ≠ z) :
    x = y := by
  contrapose! h with hxy
  apply ne_of_gt
  apply lt_of_lt_of_le (by norm_num : (2 : Cardinal.{u}) < (3 : Cardinal.{u}) )
  let f : ULift.{u} (Fin 3) → α := fun a ↦ match a with
  | ULift.up 0 => x
  | ULift.up 1 => y
  | ULift.up 2 => z
  have hinj : Function.Injective f := by
    intro a b h
    match a with
    | ULift.up 0 => match b with
      | ULift.up 0 => rfl
      | ULift.up 1 => simp only [f] at h; exact False.elim (hxy h)
      | ULift.up 2 => simp only [f] at h; exact False.elim (hx h)
    | ULift.up 1 => match b with
      | ULift.up 0 => simp only [f] at h; exact False.elim (hxy (Eq.symm h))
      | ULift.up 1 => rfl
      | ULift.up 2 => simp only [f] at h; exact False.elim (hy h)
    | ULift.up 2 => match b with
      | ULift.up 0 => simp only [f] at h; exact False.elim (hx (Eq.symm h))
      | ULift.up 1 => simp only [f] at h; exact False.elim (hy (Eq.symm h))
      | ULift.up 2 => rfl
  apply Cardinal.mk_le_of_injective hinj

So my questions are...

• Is there a more elegant way to do this?
• General advise on working with cardinal? Any helpful theorems/tactics I can use?

[Andrew Yang]

I would suggest to avoid cardinal if you only care about finite types. Translating everything back to Fintype.card makes things way easier.

theorem eq_of_card2.{u} {α : Type u} (h : Cardinal.mk α = 2) {x y z: α} (hx : x ≠ z) (hy : y ≠ z) :
    x = y := by
  have : Finite α := Cardinal.mk_lt_aleph0_iff.mp (h.trans_lt (Cardinal.lt_aleph0.mpr ⟨2, rfl⟩))
  cases nonempty_fintype α
  replace h : Fintype.card α = 2 := Nat.cast_injective ((Cardinal.mk_fintype _).symm.trans h)
  classical
  by_contra hxy
  simpa [hx, hy, hxy] using (Finset.card_le_univ {x, y, z}).trans_eq h

[Matt Diamond]

import Mathlib

theorem eq_of_card2.{u} {α : Type u} (h : Cardinal.mk α = 2) {x y z: α} (hx : x ≠ z) (hy : y ≠ z) :
    x = y := by
  rw [Cardinal.mk_eq_two_iff' z] at h
  exact h.unique hx hy

[Matt Diamond]

I searched the mathlib docs for "cardinal two", but I can't say that this strategy will scale to higher numbers...

[Matt Diamond]

but yes, there are a few cardinal lemmas dealing with small cardinalities

[Aaron Liu]

Should this be a simproc?

[Aaron Liu]

Maybe a new tactic

[Weiyi Wang]

For some reason the search refused to give me result when I search for "two"... Thankss

[Eric Wieser]

Or should the conclusion be \not [x, y, z].Nodup or \not Injective ![x, y, z]?