α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m : Sym α n
⊢ ¬Finset.sym s n = ∅ ↔ n = 0 ∨ ¬s = ∅
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m : Sym α n
⊢ Finset.Nonempty (Finset.sym s n) ↔ n = 0 ∨ Finset.Nonempty s
simp_rw [nonempty_iff_ne_empty, Ne.def]
no goals
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m : Sym α n
⊢ ¬Finset.sym s n = ∅ ↔ n = 0 ∨ ¬s = ∅
rwa [sym_eq_empty, not_and_or, not_ne_iff]