case zero
α : Type u_1
β : Type ?u.2767
n : ℕ
a a' : α
v✝ : Vector α n
ha✝ : a ∈ toList (tail v✝)
v : Vector α Nat.zero
ha : a ∈ toList (tail v)
⊢ a ∈ toList v

case succ
α : Type u_1
β : Type ?u.2767
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
α : Type u_1
β : Type ?u.2767
n : ℕ
a a' : α
v : Vector α n
ha : a ∈ toList (tail v)
⊢ a ∈ toList v
induction' n with n _
no goals
case zero
α : Type u_1
β : Type ?u.2767
n : ℕ
a a' : α
v✝ : Vector α n
ha✝ : a ∈ toList (tail v✝)
v : Vector α Nat.zero
ha : a ∈ toList (tail v)
⊢ a ∈ toList v
exact False.elim (Vector.not_mem_zero a v.tail ha)
no goals
case succ
α : Type u_1
β : Type ?u.2767
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
exact (mem_succ_iff a v).2 (Or.inr ha)