rcases Part.eq_none_or_eq_some (g v) with (_ | ⟨x, _⟩) <;> simp[*]
n : ℕ
f : Vector ℕ n → ℕ → ℕ
hf : Arith₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
⊢ ((g v).bind fun x => Part.some (f v x)) = Part.map (f v) (g v)
no goals