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

State before:
α : Type u_1
s : Set α
inst✝ : Finite ↑s
⊢ 1 < ncard s ↔ Set.Nontrivial s
Tactic:
rw [← Set.one_lt_encard_iff_nontrivial, ← Set.Finite.cast_ncard_eq (toFinite s),
  Nat.one_lt_cast]
State after:
no goals