α : Type u_1
β : Type ?u.52121
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.52121
s t : Finset α
f : α → β
n : ℕ
⊢ card s ≤ 1 ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b
rw [card_le_one]
no goals
α : Type u_1
β : Type ?u.52121
s t : Finset α
f : α → β
n : ℕ
⊢ (∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a = b) ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b
tauto