case intro.intro
α : Type u_1
β : Type ?u.1743
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)
α : Type u_1
β : Type ?u.1743
n : ℕ
a a' : α
v : Vector α (n + 1)
⊢ a ∈ toList v ↔ a = head v ∨ a ∈ toList (tail v)
obtain ⟨a', v', h⟩ := exists_eq_cons v
no goals
case intro.intro
α : Type u_1
β : Type ?u.1743
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)
simp_rw [h, Vector.mem_cons_iff, Vector.head_cons, Vector.tail_cons]