-- Mathlib/Data/Sym/Basic.lean
theorem encode_decode [DecidableEq α] (s : Sym (Option α) n ⊕ Sym α n.succ) :
    encode (decode s) = s

Proof state:
case neg
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
h : none ∉ decode (Sum.inr s)
⊢ Sum.inr (map (fun o => (↑o).get ⋯) (decode (Sum.inr s)).attach) = Sum.inr s

Tactic:
refine congr_arg Sum.inr ?_

Result:
case neg
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
h : none ∉ decode (Sum.inr s)
⊢ map (fun o => (↑o).get ⋯) (decode (Sum.inr s)).attach = s

Proof state:
case inr
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
⊢ encode (decode (Sum.inr s)) = Sum.inr s

Tactic:
unfold SymOptionSuccEquiv.encode

Result:
case inr
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
⊢ (if h : none ∈ decode (Sum.inr s) then Sum.inl ((decode (Sum.inr s)).erase none h)
    else Sum.inr (map (fun o => (↑o).get ⋯) (decode (Sum.inr s)).attach)) =
    Sum.inr s

Proof state:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) n ⊕ Sym α n.succ
⊢ encode (decode s) = s

Tactic:
obtain s | s := s

Result:
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 α n.succ
⊢ encode (decode (Sum.inr s)) = Sum.inr s

Proof state:
case pos
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
h : none ∈ decode (Sum.inr s)
⊢ False

Tactic:
obtain ⟨a, _, ha⟩ := Multiset.mem_map.mp h

Result:
case pos.intro.intro
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
h : none ∈ decode (Sum.inr s)
a : α
left✝ : a ∈ ↑s
ha : Embedding.some a = none
⊢ False

Proof state:
case neg
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
h : none ∉ decode (Sum.inr s)
⊢ map some (map (fun o => (↑o).get ⋯) (decode (Sum.inr s)).attach) = map some s

Tactic:
refine Eq.trans ?_ (.trans (SymOptionSuccEquiv.decode (Sum.inr s)).attach_map_coe ?_) <;> simp

Result:
no goals

Proof state:
case inr
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
⊢ (if h : none ∈ decode (Sum.inr s) then Sum.inl ((decode (Sum.inr s)).erase none h)
    else Sum.inr (map (fun o => (↑o).get ⋯) (decode (Sum.inr s)).attach)) =
    Sum.inr s

Tactic:
split_ifs with h

Result:
case pos
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
h : none ∈ decode (Sum.inr s)
⊢ False

case neg
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
h : none ∉ decode (Sum.inr s)
⊢ Sum.inr (map (fun o => (↑o).get ⋯) (decode (Sum.inr s)).attach) = Sum.inr s

Proof state:
case pos.intro.intro
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
h : none ∈ decode (Sum.inr s)
a : α
left✝ : a ∈ ↑s
ha : Embedding.some a = none
⊢ False

Tactic:
exact Option.some_ne_none _ ha

Result:
no goals

Proof state:
case neg
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
h : none ∉ decode (Sum.inr s)
⊢ map (fun o => (↑o).get ⋯) (decode (Sum.inr s)).attach = s

Tactic:
refine map_injective (Option.some_injective _) _ ?_

Result:
case neg
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
h : none ∉ decode (Sum.inr s)
⊢ map some (map (fun o => (↑o).get ⋯) (decode (Sum.inr s)).attach) = map some s

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

Tactic:
simp

Result:
no goals