intro v
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 - (v.get i).sqrt * (v.get i).sqrt
hh : Arith₁ fun v => (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 - (v.get i).sqrt * (v.get i).sqrt
    else (v.get i).sqrt
⊢ ∀ (i_1 : Vector ℕ n),
    (if 0 < (i_1.get i - (i_1.get i).sqrt * (i_1.get i).sqrt).isLtNat (i_1.get i).sqrt then
        i_1.get i - (i_1.get i).sqrt * (i_1.get i).sqrt
      else (i_1.get i).sqrt) =
      (i_1.get i).unpair.1
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 - (v.get i).sqrt * (v.get i).sqrt
hh : Arith₁ fun v => (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 - (v.get i).sqrt * (v.get i).sqrt
    else (v.get i).sqrt
v : Vector ℕ n
⊢ (if 0 < (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt then
      v.get i - (v.get i).sqrt * (v.get i).sqrt
    else (v.get i).sqrt) =
    (v.get i).unpair.1