case intro
α : Type u_1
β : Type ?u.30706
n n' m : ℕ
s✝ : Sym α n
a✝ b : α
s : Sym α (Nat.succ n)
a : α
ha : a ∈ s
⊢ ∃ a s', s = a ::ₛ s'
α : Type u_1
β : Type ?u.30706
n n' m : ℕ
s✝ : Sym α n
a b : α
s : Sym α (Nat.succ n)
⊢ ∃ a s', s = a ::ₛ s'
obtain ⟨a, ha⟩ := exists_mem s
no goals
case intro
α : Type u_1
β : Type ?u.30706
n n' m : ℕ
s✝ : Sym α n
a✝ b : α
s : Sym α (Nat.succ n)
a : α
ha : a ∈ s
⊢ ∃ a s', s = a ::ₛ s'
classical exact ⟨a, s.erase a ha, (cons_erase ha).symm⟩
no goals
case intro
α : Type u_1
β : Type ?u.30706
n n' m : ℕ
s✝ : Sym α n
a✝ b : α
s : Sym α (Nat.succ n)
a : α
ha : a ∈ s
⊢ ∃ a s', s = a ::ₛ s'
exact ⟨a, s.erase a ha, (cons_erase ha).symm⟩