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

State before:
α : Type u_1
inst✝ : Encodable α
e i : ℕ
⊢ encodeDecode α e = some i → ∃ a, decode i = some a
Tactic:
simp[encodeDecode]
State after:
α : Type u_1
inst✝ : Encodable α
e i : ℕ
⊢ (encode (decode e)).predO = some i → ∃ a, decode i = some a

State before:
α : Type u_1
inst✝ : Encodable α
e i : ℕ
⊢ (encode (decode e)).predO = some i → ∃ a, decode i = some a
Tactic:
cases (decode e : Option α) <;> simp
State after:
case some
α : Type u_1
inst✝ : Encodable α
e i : ℕ
val✝ : α
⊢ encode val✝ = i → ∃ a, decode i = some a

State before:
case some
α : Type u_1
inst✝ : Encodable α
e i : ℕ
val✝ : α
⊢ encode val✝ = i → ∃ a, decode i = some a
Tactic:
rintro rfl
State after:
case some
α : Type u_1
inst✝ : Encodable α
e : ℕ
val✝ : α
⊢ ∃ a, decode (encode val✝) = some a

State before:
case some
α : Type u_1
inst✝ : Encodable α
e : ℕ
val✝ : α
⊢ ∃ a, decode (encode val✝) = some a
Tactic:
simp
State after:
no goals