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

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