α : Type u_1
β : Type ?u.160
n : ℕ
a a' : α
v : Vector α n
⊢ (∃ i h, List.get (toList v) { val := i, isLt := h } = a) ↔
    ∃ i h, List.get (toList v) (↑(Fin.cast (_ : n = List.length (toList v))) { val := i, isLt := h }) = a
α : Type u_1
β : Type ?u.160
n : ℕ
a a' : α
v : Vector α n
⊢ a ∈ toList v ↔ ∃ i, get v i = a
simp only [List.mem_iff_get, Fin.exists_iff, Vector.get_eq_get]
no goals
α : Type u_1
β : Type ?u.160
n : ℕ
a a' : α
v : Vector α n
⊢ (∃ i h, List.get (toList v) { val := i, isLt := h } = a) ↔
    ∃ i h, List.get (toList v) (↑(Fin.cast (_ : n = List.length (toList v))) { val := i, isLt := h }) = a
exact
  ⟨fun ⟨i, hi, h⟩ => ⟨i, by rwa [toList_length] at hi, h⟩, fun ⟨i, hi, h⟩ =>
    ⟨i, by rwa [toList_length], h⟩⟩
no goals
α : Type u_1
β : Type ?u.160
n : ℕ
a a' : α
v : Vector α n
x✝ : ∃ i h, List.get (toList v) { val := i, isLt := h } = a
i : ℕ
hi : i < List.length (toList v)
h : List.get (toList v) { val := i, isLt := hi } = a
⊢ i < n
rwa [toList_length] at hi
no goals
α : Type u_1
β : Type ?u.160
n : ℕ
a a' : α
v : Vector α n
x✝ : ∃ i h, List.get (toList v) (↑(Fin.cast (_ : n = List.length (toList v))) { val := i, isLt := h }) = a
i : ℕ
hi : i < n
h : List.get (toList v) (↑(Fin.cast (_ : n = List.length (toList v))) { val := i, isLt := hi }) = a
⊢ i < List.length (toList v)
rwa [toList_length]