α : Type u_1
β : Type ?u.155682
s✝ t : Set α
a b x y : α
f : α → β
inst✝ : Subsingleton α
s : Set α
⊢ Finset.card (Finite.toFinset (_ : Set.Finite s)) ≤ 1
α : Type u_1
β : Type ?u.155682
s✝ t : Set α
a b x y : α
f : α → β
inst✝ : Subsingleton α
s : Set α
⊢ ncard s ≤ 1
rw [ncard_eq_toFinset_card]
no goals
α : Type u_1
β : Type ?u.155682
s✝ t : Set α
a b x y : α
f : α → β
inst✝ : Subsingleton α
s : Set α
⊢ Finset.card (Finite.toFinset (_ : Set.Finite s)) ≤ 1
exact Finset.card_le_one_of_subsingleton _