case pos
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) (Nat.succ n)
h : none ∈ s
⊢ decode (encode s) = s

case neg
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) (Nat.succ n)
h : ¬none ∈ s
⊢ decode (encode s) = s
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) (Nat.succ n)
⊢ decode (encode s) = s
by_cases h : none ∈ s
no goals
case pos
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) (Nat.succ n)
h : none ∈ s
⊢ decode (encode s) = s
simp [h]
case neg
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) (Nat.succ n)
h : ¬none ∈ s
⊢ map (fun x => ↑x) (attach s) = s
case neg
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) (Nat.succ n)
h : ¬none ∈ s
⊢ decode (encode s) = s
simp only [decode, h, not_false_iff, encode_of_not_none_mem, Embedding.some_apply, map_map,
  comp_apply, Option.some_get]
no goals
case neg
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) (Nat.succ n)
h : ¬none ∈ s
⊢ map (fun x => ↑x) (attach s) = s
convert s.attach_map_coe