no goals
α : Type u_1
β : Type ?u.158307
s t : Set α
a b x y : α
f : α → β
hs : autoParam (Set.Finite s) _auto✝
⊢ 2 < ncard s ↔ ∃ a, a ∈ s ∧ ∃ b, b ∈ s ∧ ∃ c, c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
simp only [two_lt_ncard_iff hs, exists_and_left, exists_prop]