n : ℕ
f : Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v => Nat.sqrt (f v)
⊢ Primrec' fun v => (unpair (f v)).fst
n : ℕ
f : Vector ℕ n → ℕ
hf : Primrec' f
⊢ Primrec' fun v => (unpair (f v)).fst
have s := sqrt.comp₁ _ hf
n : ℕ
f : Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v => Nat.sqrt (f v)
fss : Primrec' fun v => f v - Nat.sqrt (f v) * Nat.sqrt (f v)
⊢ Primrec' fun v => (unpair (f v)).fst
n : ℕ
f : Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v => Nat.sqrt (f v)
⊢ Primrec' fun v => (unpair (f v)).fst
have fss := sub.comp₂ _ hf (mul.comp₂ _ s s)
n : ℕ
f : Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v => Nat.sqrt (f v)
fss : Primrec' fun v => f v - Nat.sqrt (f v) * Nat.sqrt (f v)
v : Vector ℕ n
⊢ (if f v - Nat.sqrt (f v) * Nat.sqrt (f v) < Nat.sqrt (f v) then f v - Nat.sqrt (f v) * Nat.sqrt (f v)
    else Nat.sqrt (f v)) =
    (unpair (f v)).fst
n : ℕ
f : Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v => Nat.sqrt (f v)
fss : Primrec' fun v => f v - Nat.sqrt (f v) * Nat.sqrt (f v)
⊢ Primrec' fun v => (unpair (f v)).fst
refine' (if_lt fss s fss s).of_eq fun v => _
n : ℕ
f : Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v => Nat.sqrt (f v)
fss : Primrec' fun v => f v - Nat.sqrt (f v) * Nat.sqrt (f v)
v : Vector ℕ n
⊢ (if f v - Nat.sqrt (f v) * Nat.sqrt (f v) < Nat.sqrt (f v) then f v - Nat.sqrt (f v) * Nat.sqrt (f v)
    else Nat.sqrt (f v)) =
    (if f v - Nat.sqrt (f v) * Nat.sqrt (f v) < Nat.sqrt (f v) then
        (f v - Nat.sqrt (f v) * Nat.sqrt (f v), Nat.sqrt (f v))
      else (Nat.sqrt (f v), f v - Nat.sqrt (f v) * Nat.sqrt (f v) - Nat.sqrt (f v))).fst
n : ℕ
f : Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v => Nat.sqrt (f v)
fss : Primrec' fun v => f v - Nat.sqrt (f v) * Nat.sqrt (f v)
v : Vector ℕ n
⊢ (if f v - Nat.sqrt (f v) * Nat.sqrt (f v) < Nat.sqrt (f v) then f v - Nat.sqrt (f v) * Nat.sqrt (f v)
    else Nat.sqrt (f v)) =
    (unpair (f v)).fst
simp [Nat.unpair]
no goals
n : ℕ
f : Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v => Nat.sqrt (f v)
fss : Primrec' fun v => f v - Nat.sqrt (f v) * Nat.sqrt (f v)
v : Vector ℕ n
⊢ (if f v - Nat.sqrt (f v) * Nat.sqrt (f v) < Nat.sqrt (f v) then f v - Nat.sqrt (f v) * Nat.sqrt (f v)
    else Nat.sqrt (f v)) =
    (if f v - Nat.sqrt (f v) * Nat.sqrt (f v) < Nat.sqrt (f v) then
        (f v - Nat.sqrt (f v) * Nat.sqrt (f v), Nat.sqrt (f v))
      else (Nat.sqrt (f v), f v - Nat.sqrt (f v) * Nat.sqrt (f v) - Nat.sqrt (f v))).fst
split_ifs <;> rfl