{ rcases hs : toOptionVec (v ∘ Fin.succ) with (_ | z) <;> simp
  { have : ∃ i : Fin n, v i.succ = none := by simpa using hs
    rcases this with ⟨i, hi⟩
    exact ⟨i.succ, by simp[hi]⟩ }
  { have : ∀ i, v i.succ = some (z i) := ih.mp hs
    have : v = some a :> (fun i => some (z i)) :=
      by funext i; cases i using Fin.cases <;> simp[hz, this]
    simp[this, ←comp_vecCons', Iff.symm Function.funext_iff ] } }
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)
no goals