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

State before:
α✝ : Type u_1
inst✝³ : Encodable α✝
α : Type u_1
P : α → Prop
inst✝² : Encodable α
inst✝¹ : DecidablePred P
β : α → Type u_2
inst✝ : (a : α) → Encodable (β a)
e : ℕ
⊢ encodeDecode ((a : α) × β a) e =
    (decode e.unpair.1).bind fun a => Option.map (fun b => (encode a).pair b) (encodeDecode (β a) e.unpair.2)
Tactic:
rcases ha : (decode e.unpair.1 : Option α) with (_ | a) <;> simp[*, encodeDecode]
State after:
case some
α✝ : Type u_1
inst✝³ : Encodable α✝
α : Type u_1
P : α → Prop
inst✝² : Encodable α
inst✝¹ : DecidablePred P
β : α → Type u_2
inst✝ : (a : α) → Encodable (β a)
e : ℕ
a : α
ha : decode e.unpair.1 = some a
⊢ (encode (Option.map (Sigma.mk a) (decode e.unpair.2))).predO =
    Option.map (fun b => (encode a).pair b) (encode (decode e.unpair.2)).predO

State before:
case some
α✝ : Type u_1
inst✝³ : Encodable α✝
α : Type u_1
P : α → Prop
inst✝² : Encodable α
inst✝¹ : DecidablePred P
β : α → Type u_2
inst✝ : (a : α) → Encodable (β a)
e : ℕ
a : α
ha : decode e.unpair.1 = some a
⊢ (encode (Option.map (Sigma.mk a) (decode e.unpair.2))).predO =
    Option.map (fun b => (encode a).pair b) (encode (decode e.unpair.2)).predO
Tactic:
{ rcases (decode e.unpair.2 : Option (β a)) with (_ | b) <;> simp[*] }
State after:
no goals

State before:
case some
α✝ : Type u_1
inst✝³ : Encodable α✝
α : Type u_1
P : α → Prop
inst✝² : Encodable α
inst✝¹ : DecidablePred P
β : α → Type u_2
inst✝ : (a : α) → Encodable (β a)
e : ℕ
a : α
ha : decode e.unpair.1 = some a
⊢ (encode (Option.map (Sigma.mk a) (decode e.unpair.2))).predO =
    Option.map (fun b => (encode a).pair b) (encode (decode e.unpair.2)).predO
Tactic:
rcases (decode e.unpair.2 : Option (β a)) with (_ | b) <;> simp[*]
State after:
no goals