Theorem: Encodable.encode_decode_subtype (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 ((decode e).bind fun a => if P a then some a else none)
Tactic:
rcases h : decode (α := α) e with (_ | s) <;> simp[*, decode, decodeSubtype, encode, encodeSubtype]
State after:
case some
α✝ : Type u_1
inst✝² : Encodable α✝
α : Type u_1
P : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred P
e : ℕ
s : α
h : decode e = some s
⊢ Option.rec 0 (fun val => encode ↑val + 1) (if h : P s then some ⟨s, ⋯⟩ else none) =
    Option.rec 0 (fun val => encode val + 1) (if P s then some s else none)

State before:
case some
α✝ : Type u_1
inst✝² : Encodable α✝
α : Type u_1
P : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred P
e : ℕ
s : α
h : decode e = some s
⊢ Option.rec 0 (fun val => encode ↑val + 1) (if h : P s then some ⟨s, ⋯⟩ else none) =
    Option.rec 0 (fun val => encode val + 1) (if P s then some s else none)
Tactic:
{ by_cases hs : P s <;> simp[hs] }
State after:
no goals

State before:
case some
α✝ : Type u_1
inst✝² : Encodable α✝
α : Type u_1
P : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred P
e : ℕ
s : α
h : decode e = some s
⊢ Option.rec 0 (fun val => encode ↑val + 1) (if h : P s then some ⟨s, ⋯⟩ else none) =
    Option.rec 0 (fun val => encode val + 1) (if P s then some s else none)
Tactic:
by_cases hs : P s <;> simp[hs]
State after:
no goals