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

State before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
n : ℕ
β : Type u_2
f : Fin n → β
⊢ ((Equiv.vectorEquivFin β n).symm f).toList = List.ofFn f
Tactic:
ext i b
State after:
case a.a
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
n : ℕ
β : Type u_2
f : Fin n → β
i : ℕ
b : β
⊢ b ∈ ((Equiv.vectorEquivFin β n).symm f).toList.get? i ↔ b ∈ (List.ofFn f).get? i

State before:
case a.a
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
n : ℕ
β : Type u_2
f : Fin n → β
i : ℕ
b : β
⊢ b ∈ ((Equiv.vectorEquivFin β n).symm f).toList.get? i ↔ b ∈ (List.ofFn f).get? i
Tactic:
simp[Equiv.vectorEquivFin, Vector.ofFn]
State after:
no goals