α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m : Sym α n
h : ¬Finset.Nonempty (Finset.sym s n)
⊢ ¬Finset.Nonempty s
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m : Sym α n
h : Finset.sym s n = ∅
⊢ s = ∅
rw [← not_nonempty_iff_eq_empty] at h⊢
no goals
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m : Sym α n
h : ¬Finset.Nonempty (Finset.sym s n)
⊢ ¬Finset.Nonempty s
exact fun hs ↦ h (hs.sym _)