no goals
α : Type u_1
β : Type ?u.24655
γ : Type ?u.24658
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ 2 < card α ↔ ∃ a b c, a ≠ b ∧ a ≠ c ∧ b ≠ c
simp_rw [← Finset.card_univ, two_lt_card_iff, mem_univ, true_and_iff]