Theorem: Encodable.encode_decode_sigma_of_some (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 : ℕ
a : α
h : decode e.unpair.1 = some a
⊢ encodeDecode ((a : α) × β a) e = Option.map (fun b => (encode a).pair b) (encodeDecode (β a) e.unpair.2)
Tactic:
simp[encodeDecode, h]
State after:
α✝ : Type u_1
inst✝³ : Encodable α✝
α : Type u_1
P : α → Prop
inst✝² : Encodable α
inst✝¹ : DecidablePred P
β : α → Type u_2
inst✝ : (a : α) → Encodable (β a)
e : ℕ
a : α
h : 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:
α✝ : Type u_1
inst✝³ : Encodable α✝
α : Type u_1
P : α → Prop
inst✝² : Encodable α
inst✝¹ : DecidablePred P
β : α → Type u_2
inst✝ : (a : α) → Encodable (β a)
e : ℕ
a : α
h : 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 with (_ | b) <;> simp
State after:
no goals