case h
ε : Type u
α : Type u_1
⊢ ∀ (x : Except ε α), Except.map id x = id x
ε : Type u
α : Type u_1
⊢ Except.map id = id
apply funext
case h
ε : Type u
α : Type u_1
e : Except ε α
⊢ Except.map id e = id e
case h
ε : Type u
α : Type u_1
⊢ ∀ (x : Except ε α), Except.map id x = id x
intro e
case h
ε : Type u
α : Type u_1
e : Except ε α
⊢ (match e with
    | error err => error err
    | ok v => ok v) =
    e
case h
ε : Type u
α : Type u_1
e : Except ε α
⊢ Except.map id e = id e
simp [Except.map]
no goals
case h
ε : Type u
α : Type u_1
e : Except ε α
⊢ (match e with
    | error err => error err
    | ok v => ok v) =
    e
cases e <;> rfl