exact this.of_eq <| by
  intro v; simp[unpair]
  by_cases v.get i - (v.get i).sqrt * (v.get i).sqrt < sqrt (v.get i) <;> simp[*]
n : ℕ
i : Fin n
hf : Arith₁ fun v => (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt
hg : Arith₁ fun v => (v.get i).sqrt
hh : Arith₁ fun v => v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt
this :
  Arith₁ fun v =>
    if 0 < (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt then (v.get i).sqrt
    else v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt
⊢ Arith₁ fun v => (v.get i).unpair.2
no goals