α : Type u_1
β : Type ?u.150013
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.150013
s t : Set α
a b x y : α
f : α → β
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard s ≤ 1 ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b
rw [ncard_le_one hs]
no goals
α : Type u_1
β : Type ?u.150013
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
tauto