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

State before:
α✝ : Type u_1
inst✝² : Encodable α✝
α : Type u_1
P : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred P
e : ℕ
⊢ encode (decode e) = encode (encodeDecode α e)
Tactic:
simp[encodeDecode]
State after:
α✝ : Type u_1
inst✝² : Encodable α✝
α : Type u_1
P : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred P
e : ℕ
⊢ encode (decode e) = encode (encode (decode e)).predO

State before:
α✝ : Type u_1
inst✝² : Encodable α✝
α : Type u_1
P : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred P
e : ℕ
⊢ encode (decode e) = encode (encode (decode e)).predO
Tactic:
cases (decode e : Option α) <;> simp
State after:
no goals