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 = (decode e).bind fun a => if P a then some (encode a) else none
Tactic:
simp[encodeDecode, encode_decode_subtype]
State after:
α✝ : Type u_1
inst✝² : Encodable α✝
α : Type u_1
P : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred P
e : ℕ
⊢ (encode ((decode e).bind fun a => if P a then some a else none)).predO =
    (decode e).bind fun a => if P a then some (encode a) else none

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

State before:
case some
α✝ : Type u_1
inst✝² : Encodable α✝
α : Type u_1
P : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred P
e : ℕ
a : α
⊢ (encode (if P a then some a else none)).predO = if P a then some (encode a) else none
Tactic:
{ by_cases ha : P a <;> simp[*] }
State after:
no goals

State before:
case some
α✝ : Type u_1
inst✝² : Encodable α✝
α : Type u_1
P : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred P
e : ℕ
a : α
⊢ (encode (if P a then some a else none)).predO = if P a then some (encode a) else none
Tactic:
by_cases ha : P a <;> simp[*]
State after:
no goals