Theorem: Set.subsingleton_iff_ncard_le_one (Jordan/Mathlib/Set.lean)

State before:
α✝ : Type u_1
α : Type u_2
inst✝ : Finite α
B : Set α
⊢ Set.Subsingleton B ↔ ncard B ≤ 1
Tactic:
rw [← Set.not_nontrivial_iff, not_iff_comm, not_le, ← Set.one_lt_ncard_iff_nontrivial]
State after:
no goals