intro v
n : ℕ
i : Fin n
f : Vector ℕ n → ℕ → ℕ
hf : Arith₁ fun v => f v.tail v.head
F : Vector ℕ (n + 1) → ℕ :=
  fun v => ((f v.tail v.head).isLeNat (v.get i.succ)).and ((v.get i.succ).isLtNat (f v.tail (v.head + 1)))
this✝ : Arith₁ F
this : ArithPart₁ fun v => Nat.rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v)))
⊢ ∀ (i_1 : Vector ℕ n),
    (Nat.rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ i_1)))) =
      Nat.rfind fun x => Part.some (decide (f i_1 x ≤ i_1.get i ∧ i_1.get i < f i_1 (x + 1)))
n : ℕ
i : Fin n
f : Vector ℕ n → ℕ → ℕ
hf : Arith₁ fun v => f v.tail v.head
F : Vector ℕ (n + 1) → ℕ :=
  fun v => ((f v.tail v.head).isLeNat (v.get i.succ)).and ((v.get i.succ).isLtNat (f v.tail (v.head + 1)))
this✝ : Arith₁ F
this : ArithPart₁ fun v => Nat.rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v)))
v : Vector ℕ n
⊢ (Nat.rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v)))) =
    Nat.rfind fun x => Part.some (decide (f v x ≤ v.get i ∧ v.get i < f v (x + 1)))