simp only [tail_cons, head_cons, get_cons_succ, or_pos_iff, inv_pos_iff, not_lt,
  nonpos_iff_eq_zero, isLeNat_pos_iff, Bool.decide_or, PFun.coe_val, eq_some_iff, mem_map_iff,
  mem_rfind, mem_some_iff, F]
n : ℕ
p : Vector ℕ n → ℕ → ℕ
hp : Arith₁ fun v => p v.tail v.head
i : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (p v.tail v.head).inv.or ((v.get i.succ).isLeNat v.head)
hF : Arith₁ F
this✝ : Arith₁ fun v => v.head.isEqNat (v.get i.succ)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isEqNat (v.get i)) v) (rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v))))
v : Vector ℕ n
⊢ Part.map ((fun v x => x.isEqNat (v.get i)) v) (rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v)))) =
    (↑fun v => (v.get i).ball (p v)) v
n : ℕ
p : Vector ℕ n → ℕ → ℕ
hp : Arith₁ fun v => p v.tail v.head
i : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (p v.tail v.head).inv.or ((v.get i.succ).isLeNat v.head)
hF : Arith₁ F
this✝ : Arith₁ fun v => v.head.isEqNat (v.get i.succ)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isEqNat (v.get i)) v) (rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v))))
v : Vector ℕ n
⊢ ∃ a,
    (true = (decide (p v a = 0) || decide (v.get i ≤ a)) ∧
        ∀ {m : ℕ}, m < a → false = (decide (p v m = 0) || decide (v.get i ≤ m))) ∧
      a.isEqNat (v.get i) = (v.get i).ball (p v)