card_nonempty

Stream: general

[Johan Commelin]

Is there some easy way to tackle this goal:

n : Type u,
_inst_1 : fintype n,
h : nonempty n
⊢ 0 < fintype.card n

[Kenny Lau]

import data.fintype

universe u
variables (n : Type u) [fintype n]
example (h : nonempty n) : 0 < fintype.card n :=
begin
  by_contra H,
  rw [not_lt, nat.le_zero_iff, fintype.card_eq_zero_iff] at H,
  exact h.rec_on H
end

[Johan Commelin]

I guess this could be a simp lemma in mathlib?

[Johan Commelin]

Ooh, and thanks!

[Kenny Lau]

import set_theory.cardinal

universe u
variables (n : Type u)
example (h : nonempty n) : 0 < cardinal.mk n :=
by rwa [cardinal.pos_iff_ne_zero, cardinal.ne_zero_iff_nonempty]

[Kenny Lau]

I think Mario likes cardinal.mk more than fintype.card

[Chris Hughes]

It is in mathlib. fintype.card_pos_iff I believe.

[Johan Commelin]

Aaah, thanks! (Sorry, Kenny)