exact this.of_eq <| by intro v; simp [F]
n : ℕ
i : Fin n
f : ℕ → ℕ
hf : Arith₁ fun v => f (v.get 0)
F : ℕ → ℕ → ℕ := fun x y => ((f x).isLeNat y).and (y.isLtNat (f (x + 1)))
this : ArithPart₁ fun v => Nat.rfind fun n_1 => Part.some (decide (0 < F n_1 (v.get i)))
⊢ ArithPart₁ fun v => Nat.rfind fun x => Part.some (decide (f x ≤ v.get i ∧ v.get i < f (x + 1)))
no goals