case refine'_1
α : Type u_1
β : Type ?u.54709
s t : Finset α
f : α → β
n : ℕ
inst✝ : Nonempty α
H : card s ≤ 1
⊢ ∃ x, s ⊆ {x}

case refine'_2
α : Type u_1
β : Type ?u.54709
s t : Finset α
f : α → β
n : ℕ
inst✝ : Nonempty α
⊢ (∃ x, s ⊆ {x}) → card s ≤ 1
α : Type u_1
β : Type ?u.54709
s t : Finset α
f : α → β
n : ℕ
inst✝ : Nonempty α
⊢ card s ≤ 1 ↔ ∃ x, s ⊆ {x}
refine' ⟨fun H => _, _⟩
case refine'_1.inl
α : Type u_1
β : Type ?u.54709
t : Finset α
f : α → β
n : ℕ
inst✝ : Nonempty α
H : card ∅ ≤ 1
⊢ ∃ x, ∅ ⊆ {x}

case refine'_1.inr.intro
α : Type u_1
β : Type ?u.54709
s t : Finset α
f : α → β
n : ℕ
inst✝ : Nonempty α
H : card s ≤ 1
x : α
hx : x ∈ s
⊢ ∃ x, s ⊆ {x}
case refine'_1
α : Type u_1
β : Type ?u.54709
s t : Finset α
f : α → β
n : ℕ
inst✝ : Nonempty α
H : card s ≤ 1
⊢ ∃ x, s ⊆ {x}
obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
no goals
case refine'_1.inl
α : Type u_1
β : Type ?u.54709
t : Finset α
f : α → β
n : ℕ
inst✝ : Nonempty α
H : card ∅ ≤ 1
⊢ ∃ x, ∅ ⊆ {x}
exact ⟨Classical.arbitrary α, empty_subset _⟩
no goals
case refine'_1.inr.intro
α : Type u_1
β : Type ?u.54709
s t : Finset α
f : α → β
n : ℕ
inst✝ : Nonempty α
H : card s ≤ 1
x : α
hx : x ∈ s
⊢ ∃ x, s ⊆ {x}
exact ⟨x, fun y hy => by rw [card_le_one.1 H y hy x hx, mem_singleton]⟩
no goals
α : Type u_1
β : Type ?u.54709
s t : Finset α
f : α → β
n : ℕ
inst✝ : Nonempty α
H : card s ≤ 1
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ y ∈ {x}
rw [card_le_one.1 H y hy x hx, mem_singleton]
case refine'_2.intro
α : Type u_1
β : Type ?u.54709
s t : Finset α
f : α → β
n : ℕ
inst✝ : Nonempty α
x : α
hx : s ⊆ {x}
⊢ card s ≤ 1
case refine'_2
α : Type u_1
β : Type ?u.54709
s t : Finset α
f : α → β
n : ℕ
inst✝ : Nonempty α
⊢ (∃ x, s ⊆ {x}) → card s ≤ 1
rintro ⟨x, hx⟩
case refine'_2.intro
α : Type u_1
β : Type ?u.54709
s t : Finset α
f : α → β
n : ℕ
inst✝ : Nonempty α
x : α
hx : s ⊆ {x}
⊢ card s ≤ card {x}
case refine'_2.intro
α : Type u_1
β : Type ?u.54709
s t : Finset α
f : α → β
n : ℕ
inst✝ : Nonempty α
x : α
hx : s ⊆ {x}
⊢ card s ≤ 1
rw [← card_singleton x]
no goals
case refine'_2.intro
α : Type u_1
β : Type ?u.54709
s t : Finset α
f : α → β
n : ℕ
inst✝ : Nonempty α
x : α
hx : s ⊆ {x}
⊢ card s ≤ card {x}
exact card_le_of_subset hx