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

State before:
α✝ : Type u_1
inst✝² : Encodable α✝
α : Type u_1
P : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred P
e : ℕ
⊢ encodeDecode { x // P x } e = (encodeDecode α e).bind fun c => if ∃ a ∈ decode c, P a then some c else none
Tactic:
simp[encodeDecode_subtype', encodeDecode]
State after:
α✝ : Type u_1
inst✝² : Encodable α✝
α : Type u_1
P : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred P
e : ℕ
⊢ ((decode e).bind fun a => if P a then some (encode a) else none) =
    (encode (decode e)).predO.bind fun a => if ∃ a_1, decode a = some a_1 ∧ P a_1 then some a else none

State before:
α✝ : Type u_1
inst✝² : Encodable α✝
α : Type u_1
P : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred P
e : ℕ
⊢ ((decode e).bind fun a => if P a then some (encode a) else none) =
    (encode (decode e)).predO.bind fun a => if ∃ a_1, decode a = some a_1 ∧ P a_1 then some a else none
Tactic:
rcases (decode e : Option α) <;> simp
State after:
no goals