α : Type u_1
β : Type ?u.3400
γ : Type ?u.3403
inst✝ : Finite α
this : Fintype α
⊢ Nat.card α = 0 ↔ IsEmpty α
α : Type u_1
β : Type ?u.3400
γ : Type ?u.3403
inst✝ : Finite α
⊢ Nat.card α = 0 ↔ IsEmpty α
haveI := Fintype.ofFinite α
no goals
α : Type u_1
β : Type ?u.3400
γ : Type ?u.3403
inst✝ : Finite α
this : Fintype α
⊢ Nat.card α = 0 ↔ IsEmpty α
simp only [Nat.card_eq_fintype_card, Fintype.card_eq_zero_iff]