case zero
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
m : Sym α Nat.zero
⊢ Finset.sym s Nat.zero = ∅ ↔ Nat.zero ≠ 0 ∧ s = ∅

case succ
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n✝ : ℕ
m : Sym α (Nat.succ n✝)
⊢ Finset.sym s (Nat.succ n✝) = ∅ ↔ Nat.succ n✝ ≠ 0 ∧ s = ∅
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m : Sym α n
⊢ Finset.sym s n = ∅ ↔ n ≠ 0 ∧ s = ∅
cases n
no goals
case zero
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
m : Sym α Nat.zero
⊢ Finset.sym s Nat.zero = ∅ ↔ Nat.zero ≠ 0 ∧ s = ∅
exact iff_of_false (singleton_ne_empty _) fun h ↦ (h.1 rfl).elim
case succ
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n✝ : ℕ
m : Sym α (Nat.succ n✝)
⊢ Nat.succ n✝ ≠ 0 ∧ s = ∅ → Finset.sym s (Nat.succ n✝) = ∅
case succ
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n✝ : ℕ
m : Sym α (Nat.succ n✝)
⊢ Finset.sym s (Nat.succ n✝) = ∅ ↔ Nat.succ n✝ ≠ 0 ∧ s = ∅
refine ⟨fun h ↦ ⟨Nat.succ_ne_zero _, eq_empty_of_sym_eq_empty h⟩, ?_⟩
case succ.intro
α : Type u_1
inst✝ : DecidableEq α
t : Finset α
a b : α
n✝ : ℕ
m : Sym α (Nat.succ n✝)
left✝ : Nat.succ n✝ ≠ 0
⊢ Finset.sym ∅ (Nat.succ n✝) = ∅
case succ
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n✝ : ℕ
m : Sym α (Nat.succ n✝)
⊢ Nat.succ n✝ ≠ 0 ∧ s = ∅ → Finset.sym s (Nat.succ n✝) = ∅
rintro ⟨_, rfl⟩
no goals
case succ.intro
α : Type u_1
inst✝ : DecidableEq α
t : Finset α
a b : α
n✝ : ℕ
m : Sym α (Nat.succ n✝)
left✝ : Nat.succ n✝ ≠ 0
⊢ Finset.sym ∅ (Nat.succ n✝) = ∅
exact sym_empty _