α : Type u_1
β : Type ?u.1557
γ : Type ?u.1560
inst✝ : Finite α
this : Fintype α
⊢ Nat.card α ≤ 1 ↔ Subsingleton α
α : Type u_1
β : Type ?u.1557
γ : Type ?u.1560
inst✝ : Finite α
⊢ Nat.card α ≤ 1 ↔ Subsingleton α
haveI := Fintype.ofFinite α
no goals
α : Type u_1
β : Type ?u.1557
γ : Type ?u.1560
inst✝ : Finite α
this : Fintype α
⊢ Nat.card α ≤ 1 ↔ Subsingleton α
simp only [Nat.card_eq_fintype_card, Fintype.card_le_one_iff_subsingleton]