Theorem: encard_le_one_iff_subsingleton (Matroid/ForMathlib/Card.lean)

State before:
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
⊢ s.encard ≤ 1 ↔ s.Subsingleton
Tactic:
rw [encard_le_one_iff, Set.Subsingleton]
State after:
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
⊢ (∀ (a b : α), a ∈ s → b ∈ s → a = b) ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y

State before:
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
⊢ (∀ (a b : α), a ∈ s → b ∈ s → a = b) ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y
Tactic:
tauto
State after:
no goals