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

State before:
β✝ : Type u_1
inst✝⁴ : Encodable β✝
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : Primcodable ι
inst✝¹ : DecidableEq ι
β : Type u_3
inst✝ : Primcodable β
e : ℕ
⊢ decode e = (decode e).bind fun l => Option.map (⇑fintypeArrowEquivVector.symm) (List.toVector (Fintype.card ι) l)
Tactic:
simp [Primcodable.ofEquiv_toEncodable, Encodable.decode_ofEquiv, decode_vector]
State after:
β✝ : Type u_1
inst✝⁴ : Encodable β✝
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : Primcodable ι
inst✝¹ : DecidableEq ι
β : Type u_3
inst✝ : Primcodable β
e : ℕ
⊢ Option.map (⇑fintypeArrowEquivFinArrow.symm ∘ ⇑(Equiv.vectorEquivFin β (Fintype.card ι)))
      ((decode e).bind (List.toVector (Fintype.card ι))) =
    (decode e).bind fun l => Option.map (⇑fintypeArrowEquivVector.symm) (List.toVector (Fintype.card ι) l)

State before:
β✝ : Type u_1
inst✝⁴ : Encodable β✝
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : Primcodable ι
inst✝¹ : DecidableEq ι
β : Type u_3
inst✝ : Primcodable β
e : ℕ
⊢ Option.map (⇑fintypeArrowEquivFinArrow.symm ∘ ⇑(Equiv.vectorEquivFin β (Fintype.card ι)))
      ((decode e).bind (List.toVector (Fintype.card ι))) =
    (decode e).bind fun l => Option.map (⇑fintypeArrowEquivVector.symm) (List.toVector (Fintype.card ι) l)
Tactic:
rcases (decode e : Option (List β)) with (_ | bs) <;> simp
State after:
case some
β✝ : Type u_1
inst✝⁴ : Encodable β✝
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : Primcodable ι
inst✝¹ : DecidableEq ι
β : Type u_3
inst✝ : Primcodable β
e : ℕ
bs : List β
⊢ Option.map (⇑fintypeArrowEquivFinArrow.symm ∘ ⇑(Equiv.vectorEquivFin β (Fintype.card ι)))
      (List.toVector (Fintype.card ι) bs) =
    Option.map (⇑fintypeArrowEquivVector.symm) (List.toVector (Fintype.card ι) bs)

State before:
case some
β✝ : Type u_1
inst✝⁴ : Encodable β✝
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : Primcodable ι
inst✝¹ : DecidableEq ι
β : Type u_3
inst✝ : Primcodable β
e : ℕ
bs : List β
⊢ Option.map (⇑fintypeArrowEquivFinArrow.symm ∘ ⇑(Equiv.vectorEquivFin β (Fintype.card ι)))
      (List.toVector (Fintype.card ι) bs) =
    Option.map (⇑fintypeArrowEquivVector.symm) (List.toVector (Fintype.card ι) bs)
Tactic:
{ rfl }
State after:
no goals

State before:
case some
β✝ : Type u_1
inst✝⁴ : Encodable β✝
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : Primcodable ι
inst✝¹ : DecidableEq ι
β : Type u_3
inst✝ : Primcodable β
e : ℕ
bs : List β
⊢ Option.map (⇑fintypeArrowEquivFinArrow.symm ∘ ⇑(Equiv.vectorEquivFin β (Fintype.card ι)))
      (List.toVector (Fintype.card ι) bs) =
    Option.map (⇑fintypeArrowEquivVector.symm) (List.toVector (Fintype.card ι) bs)
Tactic:
rfl
State after:
no goals