no goals
α : Type u_1
β : Type ?u.156100
s t : Set α
a b x y : α
f : α → β
hs : autoParam (Set.Finite s) _auto✝
⊢ 1 < ncard s ↔ ∃ a, a ∈ s ∧ ∃ b, b ∈ s ∧ a ≠ b
simp_rw [ncard_eq_toFinset_card _ hs, Finset.one_lt_card, Finite.mem_toFinset]