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

State before:
β : Type u_1
inst✝ : Encodable β
⊢ decode 0 = mapM' decode (Denumerable.ofNat (List ℕ) 0)
Tactic:
simp
State after:
no goals

State before:
β : Type u_1
inst✝ : Encodable β
e : ℕ
this : e.unpair.2 < e + 1
⊢ decode (e + 1) = mapM' decode (Denumerable.ofNat (List ℕ) (e + 1))
Tactic:
simp
State after:
β : Type u_1
inst✝ : Encodable β
e : ℕ
this : e.unpair.2 < e + 1
⊢ (Seq.seq (Option.map (fun x x_1 => x :: x_1) (decode e.unpair.1)) fun x => decode e.unpair.2) =
    (decode e.unpair.1).bind fun __do_lift =>
      (mapM' decode (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun __do_lift_1 => some (__do_lift :: __do_lift_1)

State before:
β : Type u_1
inst✝ : Encodable β
e : ℕ
this : e.unpair.2 < e + 1
⊢ (Seq.seq (Option.map (fun x x_1 => x :: x_1) (decode e.unpair.1)) fun x => decode e.unpair.2) =
    (decode e.unpair.1).bind fun __do_lift =>
      (mapM' decode (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun __do_lift_1 => some (__do_lift :: __do_lift_1)
Tactic:
rcases (decode e.unpair.1 : Option β) with (_ | b) <;> simp[seq_eq_bind, Option.bind_eq_bind]
State after:
case some
β : Type u_1
inst✝ : Encodable β
e : ℕ
this : e.unpair.2 < e + 1
b : β
⊢ Option.map (fun x => b :: x) (decode e.unpair.2) =
    (mapM' decode (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun __do_lift => some (b :: __do_lift)

State before:
case some
β : Type u_1
inst✝ : Encodable β
e : ℕ
this : e.unpair.2 < e + 1
b : β
⊢ Option.map (fun x => b :: x) (decode e.unpair.2) =
    (mapM' decode (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun __do_lift => some (b :: __do_lift)
Tactic:
have := decode_list (e.unpair.2)
State after:
case some
β : Type u_1
inst✝ : Encodable β
e : ℕ
this✝ : e.unpair.2 < e + 1
b : β
this : decode e.unpair.2 = mapM' decode (Denumerable.ofNat (List ℕ) e.unpair.2)
⊢ Option.map (fun x => b :: x) (decode e.unpair.2) =
    (mapM' decode (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun __do_lift => some (b :: __do_lift)

State before:
case some
β : Type u_1
inst✝ : Encodable β
e : ℕ
this✝ : e.unpair.2 < e + 1
b : β
this : decode e.unpair.2 = mapM' decode (Denumerable.ofNat (List ℕ) e.unpair.2)
⊢ Option.map (fun x => b :: x) (decode e.unpair.2) =
    (mapM' decode (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun __do_lift => some (b :: __do_lift)
Tactic:
simp[this, Option.pure_eq_some, Option.map_eq_bind, Function.comp]
State after:
no goals