α : Type u_1
β : Type ?u.36454
γ : Type ?u.36457
s : Finset α
a b : α
ha : a ∈ s
⊢ ↑s = {a} ∨ Set.Nontrivial ↑s
α : Type u_1
β : Type ?u.36454
γ : Type ?u.36457
s : Finset α
a b : α
ha : a ∈ s
⊢ s = {a} ∨ Set.Nontrivial ↑s
rw [← coe_eq_singleton]
no goals
α : Type u_1
β : Type ?u.36454
γ : Type ?u.36457
s : Finset α
a b : α
ha : a ∈ s
⊢ ↑s = {a} ∨ Set.Nontrivial ↑s
exact Set.eq_singleton_or_nontrivial ha