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

State before:
β✝ : Type u_1
inst✝¹ : Encodable β✝
k : ℕ
β : Type u_2
inst✝ : Primcodable β
e : ℕ
⊢ decode e = (decode e).bind fun l => Option.map (⇑(Equiv.vectorEquivFin β k)) (List.toVector k l)
Tactic:
simp[Primcodable.ofEquiv_toEncodable, Encodable.decode_ofEquiv]
State after:
β✝ : Type u_1
inst✝¹ : Encodable β✝
k : ℕ
β : Type u_2
inst✝ : Primcodable β
e : ℕ
⊢ Option.map (⇑(Equiv.vectorEquivFin β k)) (decode e) =
    (decode e).bind fun l => Option.map (⇑(Equiv.vectorEquivFin β k)) (List.toVector k l)

State before:
β✝ : Type u_1
inst✝¹ : Encodable β✝
k : ℕ
β : Type u_2
inst✝ : Primcodable β
e : ℕ
⊢ Option.map (⇑(Equiv.vectorEquivFin β k)) (decode e) =
    (decode e).bind fun l => Option.map (⇑(Equiv.vectorEquivFin β k)) (List.toVector k l)
Tactic:
rw[decode_vector]
State after:
β✝ : Type u_1
inst✝¹ : Encodable β✝
k : ℕ
β : Type u_2
inst✝ : Primcodable β
e : ℕ
⊢ Option.map (⇑(Equiv.vectorEquivFin β k)) ((decode e).bind (List.toVector k)) =
    (decode e).bind fun l => Option.map (⇑(Equiv.vectorEquivFin β k)) (List.toVector k l)

State before:
β✝ : Type u_1
inst✝¹ : Encodable β✝
k : ℕ
β : Type u_2
inst✝ : Primcodable β
e : ℕ
⊢ Option.map (⇑(Equiv.vectorEquivFin β k)) ((decode e).bind (List.toVector k)) =
    (decode e).bind fun l => Option.map (⇑(Equiv.vectorEquivFin β k)) (List.toVector k l)
Tactic:
rcases (decode e : Option (List β)) with (_ | bs) <;> simp
State after:
no goals