have := ArithPart₁.implicit_fun i (fun _ x => x * x) ((mul 0 1).comp₂ _ head head)
n : ℕ
i : Fin n
⊢ Arith₁ fun v => (v.get i).sqrt
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
⊢ Arith₁ fun v => (v.get i).sqrt