rcases hz : v 0 with (_ | a) <;> simp
case succ
α : Type u_1
n : ℕ
ih : ∀ {w : Fin n → α} {v : Fin n → Option α}, toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
w : Fin (n + 1) → α
v : Fin (n + 1) → Option α
⊢ ((toOptionVec (v ∘ succ)).bind fun vs => Option.map (fun z => z :> vs) (v 0)) = some w ↔
    ∀ (i : Fin (n + 1)), v i = some (w i)
case succ.none
α : Type u_1
n : ℕ
ih : ∀ {w : Fin n → α} {v : Fin n → Option α}, toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
w : Fin (n + 1) → α
v : Fin (n + 1) → Option α
hz : v 0 = none
⊢ ∃ x, ¬v x = some (w x)

case succ.some
α : Type u_1
n : ℕ
ih : ∀ {w : Fin n → α} {v : Fin n → Option α}, toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
w : Fin (n + 1) → α
v : Fin (n + 1) → Option α
a : α
hz : v 0 = some a
⊢ ((toOptionVec (v ∘ succ)).bind fun a_1 => some (a :> a_1)) = some w ↔ ∀ (i : Fin (n + 1)), v i = some (w i)