α : Type u_1
β : Type ?u.55605
s t : Finset α
f : α → β
n : ℕ
⊢ (∃ a, a ∈ s ∧ ∃ b, b ∈ s ∧ a ≠ b) ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b
α : Type u_1
β : Type ?u.55605
s t : Finset α
f : α → β
n : ℕ
⊢ 1 < card s ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b
rw [one_lt_card]
no goals
α : Type u_1
β : Type ?u.55605
s t : Finset α
f : α → β
n : ℕ
⊢ (∃ a, a ∈ s ∧ ∃ b, b ∈ s ∧ a ≠ b) ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b
simp only [exists_prop, exists_and_left]