α : Type u_1
β : Type ?u.685
γ : Type ?u.688
inst✝ : Finite α
this : Fintype α
⊢ 0 < Nat.card α ↔ Nonempty α
α : Type u_1
β : Type ?u.685
γ : Type ?u.688
inst✝ : Finite α
⊢ 0 < Nat.card α ↔ Nonempty α
haveI := Fintype.ofFinite α
no goals
α : Type u_1
β : Type ?u.685
γ : Type ?u.688
inst✝ : Finite α
this : Fintype α
⊢ 0 < Nat.card α ↔ Nonempty α
rw [Nat.card_eq_fintype_card, Fintype.card_pos_iff]