case intro
α : Type u_1
β : Type ?u.1716
γ : Type ?u.1719
inst✝¹ : Fintype α
s t : Finset α
inst✝ : Subsingleton α
x : α
hx : x ∈ s
⊢ s = univ
α : Type u_1
β : Type ?u.1716
γ : Type ?u.1719
inst✝¹ : Fintype α
s t : Finset α
inst✝ : Subsingleton α
⊢ Finset.Nonempty s → s = univ
rintro ⟨x, hx⟩
no goals
case intro
α : Type u_1
β : Type ?u.1716
γ : Type ?u.1719
inst✝¹ : Fintype α
s t : Finset α
inst✝ : Subsingleton α
x : α
hx : x ∈ s
⊢ s = univ
refine' eq_univ_of_forall fun y => by rwa [Subsingleton.elim y x]
no goals
α : Type u_1
β : Type ?u.1716
γ : Type ?u.1719
inst✝¹ : Fintype α
s t : Finset α
inst✝ : Subsingleton α
x : α
hx : x ∈ s
y : α
⊢ y ∈ s
rwa [Subsingleton.elim y x]