cases Nat.eq_zero_or_pos (card α) with
| inl h0 =>
  dsimp [card] at h0
  rcases ‹Nonempty α› with ⟨a⟩
  have := List.eq_nil_of_length_eq_zero h0
  have : a ∈ [] := this ▸ mem_elems a
  cases this
| inr h => exact h
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Nonempty α
⊢ card α ≥ 1
no goals