case inl
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) n
⊢ encode (decode (Sum.inl s)) = Sum.inl s

case inr
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α (Nat.succ n)
⊢ encode (decode (Sum.inr s)) = Sum.inr s
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) n ⊕ Sym α (Nat.succ n)
⊢ encode (decode s) = s
obtain s | s := s
no goals
case inl
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) n
⊢ encode (decode (Sum.inl s)) = Sum.inl s
simp
case inr
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α (Nat.succ n)
⊢ (if h : none ∈ decode (Sum.inr s) then Sum.inl (erase (decode (Sum.inr s)) none h)
    else Sum.inr (map (fun o => Option.get ↑o (_ : Option.isSome ↑o = true)) (attach (decode (Sum.inr s))))) =
    Sum.inr s
case inr
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α (Nat.succ n)
⊢ encode (decode (Sum.inr s)) = Sum.inr s
unfold SymOptionSuccEquiv.encode
case inr.inl
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α (Nat.succ n)
h : none ∈ decode (Sum.inr s)
⊢ False

case inr.inr
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α (Nat.succ n)
h : ¬none ∈ decode (Sum.inr s)
⊢ Sum.inr (map (fun o => Option.get ↑o (_ : Option.isSome ↑o = true)) (attach (decode (Sum.inr s)))) = Sum.inr s
case inr
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α (Nat.succ n)
⊢ (if h : none ∈ decode (Sum.inr s) then Sum.inl (erase (decode (Sum.inr s)) none h)
    else Sum.inr (map (fun o => Option.get ↑o (_ : Option.isSome ↑o = true)) (attach (decode (Sum.inr s))))) =
    Sum.inr s
split_ifs with h
case inr.inl.intro.intro
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α (Nat.succ n)
h : none ∈ decode (Sum.inr s)
a : α
left✝ : a ∈ ↑s
ha : ↑Embedding.some a = none
⊢ False
case inr.inl
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α (Nat.succ n)
h : none ∈ decode (Sum.inr s)
⊢ False
obtain ⟨a, _, ha⟩ := Multiset.mem_map.mp h
no goals
case inr.inl.intro.intro
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α (Nat.succ n)
h : none ∈ decode (Sum.inr s)
a : α
left✝ : a ∈ ↑s
ha : ↑Embedding.some a = none
⊢ False
exact Option.some_ne_none _ ha
case inr.inr
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α (Nat.succ n)
h : ¬none ∈ decode (Sum.inr s)
⊢ map (fun o => Option.get ↑o (_ : Option.isSome ↑o = true)) (attach (decode (Sum.inr s))) = s
case inr.inr
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α (Nat.succ n)
h : ¬none ∈ decode (Sum.inr s)
⊢ Sum.inr (map (fun o => Option.get ↑o (_ : Option.isSome ↑o = true)) (attach (decode (Sum.inr s)))) = Sum.inr s
refine' congr_arg Sum.inr _
case inr.inr
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α (Nat.succ n)
h : ¬none ∈ decode (Sum.inr s)
⊢ map some (map (fun o => Option.get ↑o (_ : Option.isSome ↑o = true)) (attach (decode (Sum.inr s)))) = map some s
case inr.inr
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α (Nat.succ n)
h : ¬none ∈ decode (Sum.inr s)
⊢ map (fun o => Option.get ↑o (_ : Option.isSome ↑o = true)) (attach (decode (Sum.inr s))) = s
refine' map_injective (Option.some_injective _) _ _
case inr.inr.refine'_1
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α (Nat.succ n)
h : ¬none ∈ decode (Sum.inr s)
⊢ map some (map (fun o => Option.get ↑o (_ : Option.isSome ↑o = true)) (attach (decode (Sum.inr s)))) =
    map Subtype.val (attach (decode (Sum.inr s)))

case inr.inr.refine'_2
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α (Nat.succ n)
h : ¬none ∈ decode (Sum.inr s)
⊢ decode (Sum.inr s) = map some s
case inr.inr
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α (Nat.succ n)
h : ¬none ∈ decode (Sum.inr s)
⊢ map some (map (fun o => Option.get ↑o (_ : Option.isSome ↑o = true)) (attach (decode (Sum.inr s)))) = map some s
refine' Eq.trans _ (Eq.trans (SymOptionSuccEquiv.decode (Sum.inr s)).attach_map_coe _)
case inr.inr.refine'_2
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α (Nat.succ n)
h : ¬none ∈ decode (Sum.inr s)
⊢ decode (Sum.inr s) = map some s
case inr.inr.refine'_1
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α (Nat.succ n)
h : ¬none ∈ decode (Sum.inr s)
⊢ map some (map (fun o => Option.get ↑o (_ : Option.isSome ↑o = true)) (attach (decode (Sum.inr s)))) =
    map Subtype.val (attach (decode (Sum.inr s)))

case inr.inr.refine'_2
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α (Nat.succ n)
h : ¬none ∈ decode (Sum.inr s)
⊢ decode (Sum.inr s) = map some s
simp
no goals
case inr.inr.refine'_2
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α (Nat.succ n)
h : ¬none ∈ decode (Sum.inr s)
⊢ decode (Sum.inr s) = map some s
simp