Theorem: Encodable.encodeDecode_eq_encode_map_decode (Logic/Vorspiel/Computability.lean)

State before:
α : Type u_1
inst✝ : Encodable α
e : ℕ
⊢ encodeDecode α e = Option.map encode (decode e)
Tactic:
simp[encodeDecode]
State after:
α : Type u_1
inst✝ : Encodable α
e : ℕ
⊢ (encode (decode e)).predO = Option.map encode (decode e)

State before:
α : Type u_1
inst✝ : Encodable α
e : ℕ
⊢ (encode (decode e)).predO = Option.map encode (decode e)
Tactic:
rcases (decode e) <;> simp
State after:
no goals