have hh : Arith₁ (fun v => sqrt (v.get i)) := Arith₁.sqrt i
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
⊢ Arith₁ fun v => (v.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
⊢ Arith₁ fun v => (v.get i).unpair.1