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