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