case inl
α : Type u_1
β : Type ?u.48906
t : Finset α
f : α → β
n : ℕ
⊢ card ∅ ≤ 1 ↔ ∀ (a : α), a ∈ ∅ → ∀ (b : α), b ∈ ∅ → a = b

case inr.intro
α : Type u_1
β : Type ?u.48906
s t : Finset α
f : α → β
n : ℕ
x : α
hx : x ∈ s
⊢ card s ≤ 1 ↔ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a = b
α : Type u_1
β : Type ?u.48906
s t : Finset α
f : α → β
n : ℕ
⊢ card s ≤ 1 ↔ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a = b
obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
case inr.intro.refine'_1
α : Type u_1
β : Type ?u.48906
s t : Finset α
f : α → β
n : ℕ
x : α
hx : x ∈ s
⊢ (∃ a, s = {a}) → ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a = b

case inr.intro.refine'_2
α : Type u_1
β : Type ?u.48906
s t : Finset α
f : α → β
n : ℕ
x : α
hx : x ∈ s
⊢ (∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a = b) → ∃ a, s = {a}
case inr.intro
α : Type u_1
β : Type ?u.48906
s t : Finset α
f : α → β
n : ℕ
x : α
hx : x ∈ s
⊢ card s ≤ 1 ↔ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a = b
refine' (Nat.succ_le_of_lt (card_pos.2 ⟨x, hx⟩)).le_iff_eq.trans (card_eq_one.trans ⟨_, _⟩)
no goals
case inl
α : Type u_1
β : Type ?u.48906
t : Finset α
f : α → β
n : ℕ
⊢ card ∅ ≤ 1 ↔ ∀ (a : α), a ∈ ∅ → ∀ (b : α), b ∈ ∅ → a = b
simp
case inr.intro.refine'_1.intro
α : Type u_1
β : Type ?u.48906
t : Finset α
f : α → β
n : ℕ
x y : α
hx : x ∈ {y}
⊢ ∀ (a : α), a ∈ {y} → ∀ (b : α), b ∈ {y} → a = b
case inr.intro.refine'_1
α : Type u_1
β : Type ?u.48906
s t : Finset α
f : α → β
n : ℕ
x : α
hx : x ∈ s
⊢ (∃ a, s = {a}) → ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a = b
rintro ⟨y, rfl⟩
no goals
case inr.intro.refine'_1.intro
α : Type u_1
β : Type ?u.48906
t : Finset α
f : α → β
n : ℕ
x y : α
hx : x ∈ {y}
⊢ ∀ (a : α), a ∈ {y} → ∀ (b : α), b ∈ {y} → a = b
simp
no goals
case inr.intro.refine'_2
α : Type u_1
β : Type ?u.48906
s t : Finset α
f : α → β
n : ℕ
x : α
hx : x ∈ s
⊢ (∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a = b) → ∃ a, s = {a}
exact fun h => ⟨x, eq_singleton_iff_unique_mem.2 ⟨hx, fun y hy => h _ hy _ hx⟩⟩