[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
a a' : α
i : Fin n
v : Vector α n
⊢ get v i ∈ toList v
[PROOFSTEP]
rw [get_eq_get]
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
a a' : α
i : Fin n
v : Vector α n
⊢ List.get (toList v) (↑(Fin.castIso (_ : n = List.length (toList v))) i) ∈ toList v
[PROOFSTEP]
exact List.get_mem _ _ _
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
a a' : α
v : Vector α n
⊢ a ∈ toList v ↔ ∃ i, get v i = a
[PROOFSTEP]
simp only [List.mem_iff_get, Fin.exists_iff, Vector.get_eq_get]
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
a a' : α
v : Vector α n
⊢ (∃ i h, List.get (toList v) { val := i, isLt := h } = a) ↔
    ∃ i h, List.get (toList v) (↑(Fin.castIso (_ : n = List.length (toList v))) { val := i, isLt := h }) = a
[PROOFSTEP]
exact ⟨fun ⟨i, hi, h⟩ => ⟨i, by rwa [toList_length] at hi , h⟩, fun ⟨i, hi, h⟩ => ⟨i, by rwa [toList_length], h⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
rwa [toList_length] at hi 
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
a a' : α
v : Vector α n
x✝ : ∃ i h, List.get (toList v) (↑(Fin.castIso (_ : n = List.length (toList v))) { val := i, isLt := h }) = a
i : ℕ
hi : i < n
h : List.get (toList v) (↑(Fin.castIso (_ : n = List.length (toList v))) { val := i, isLt := hi }) = a
⊢ i < List.length (toList v)
[PROOFSTEP]
rwa [toList_length]
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
a a' : α
⊢ ¬a ∈ toList nil
[PROOFSTEP]
unfold Vector.nil
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
a a' : α
⊢ ¬a ∈ toList { val := [], property := (_ : List.length [] = List.length []) }
[PROOFSTEP]
dsimp
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
a a' : α
⊢ ¬a ∈ []
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
a a' : α
v : Vector α n
⊢ a' ∈ toList (a ::ᵥ v) ↔ a' = a ∨ a' ∈ toList v
[PROOFSTEP]
rw [Vector.toList_cons, List.mem_cons]
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
a a' : α
v : Vector α (n + 1)
⊢ a ∈ toList v ↔ a = head v ∨ a ∈ toList (tail v)
[PROOFSTEP]
obtain ⟨a', v', h⟩ := exists_eq_cons v
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
n : ℕ
a a'✝ : α
v : Vector α (n + 1)
a' : α
v' : Vector α n
h : v = a' ::ᵥ v'
⊢ a ∈ toList v ↔ a = head v ∨ a ∈ toList (tail v)
[PROOFSTEP]
simp_rw [h, Vector.mem_cons_iff, Vector.head_cons, Vector.tail_cons]
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
a a' : α
v : Vector α n
ha : a ∈ toList (tail v)
⊢ a ∈ toList v
[PROOFSTEP]
induction' n with n _
[GOAL]
case zero
α : Type u_1
β : Type u_2
n : ℕ
a a' : α
v✝ : Vector α n
ha✝ : a ∈ toList (tail v✝)
v : Vector α Nat.zero
ha : a ∈ toList (tail v)
⊢ a ∈ toList v
[PROOFSTEP]
exact False.elim (Vector.not_mem_zero a v.tail ha)
[GOAL]
case succ
α : Type u_1
β : Type u_2
n✝ : ℕ
a a' : α
v✝ : Vector α n✝
ha✝ : a ∈ toList (tail v✝)
n : ℕ
n_ih✝ : ∀ (v : Vector α n), a ∈ toList (tail v) → a ∈ toList v
v : Vector α (Nat.succ n)
ha : a ∈ toList (tail v)
⊢ a ∈ toList v
[PROOFSTEP]
exact (mem_succ_iff a v).2 (Or.inr ha)
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
a a' : α
b : β
v : Vector α n
f : α → β
⊢ b ∈ toList (map f v) ↔ ∃ a, a ∈ toList v ∧ f a = b
[PROOFSTEP]
rw [Vector.toList_map, List.mem_map]
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
a a' : α
b : β
v : Vector α 0
f : α → β
⊢ ¬b ∈ toList (map f v)
[PROOFSTEP]
simpa only [Vector.eq_nil v, Vector.map_nil, Vector.toList_nil] using List.not_mem_nil b
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
a a' : α
b : β
v : Vector α (n + 1)
f : α → β
⊢ b ∈ toList (map f v) ↔ f (head v) = b ∨ ∃ a, a ∈ toList (tail v) ∧ f a = b
[PROOFSTEP]
rw [mem_succ_iff, head_map, tail_map, mem_map_iff, @eq_comm _ b]
