H : ∀ (n : ℕ), Nat.sqrt n = Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n
⊢ Primrec' fun v => Nat.sqrt (Vector.head v)

case H

⊢ ∀ (n : ℕ), Nat.sqrt n = Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n
⊢ Primrec' fun v => Nat.sqrt (Vector.head v)
suffices H : ∀ n : ℕ, n.sqrt = n.rec 0 fun x y => if x.succ < y.succ * y.succ then y else y.succ
case H
n : ℕ
⊢ Nat.sqrt n = Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n
case H

⊢ ∀ (n : ℕ), Nat.sqrt n = Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n
introv
case H
n : ℕ
⊢ Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n = Nat.sqrt n
case H
n : ℕ
⊢ Nat.sqrt n = Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n
symm
case H.zero

⊢ Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) Nat.zero = Nat.sqrt Nat.zero

case H.succ
n : ℕ
IH : Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n = Nat.sqrt n
⊢ Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) (Nat.succ n) =
    Nat.sqrt (Nat.succ n)
case H
n : ℕ
⊢ Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n = Nat.sqrt n
induction' n with n IH
case H.succ
n : ℕ
IH : Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n = Nat.sqrt n
⊢ (if
        Nat.succ n <
          Nat.succ (Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n) *
            Nat.succ (Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n) then
      Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n
    else Nat.succ (Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n)) =
    Nat.sqrt (Nat.succ n)
case H.succ
n : ℕ
IH : Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n = Nat.sqrt n
⊢ Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) (Nat.succ n) =
    Nat.sqrt (Nat.succ n)
dsimp
case H.succ
n : ℕ
IH : Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n = Nat.sqrt n
⊢ (if Nat.succ n < Nat.succ (Nat.sqrt n) * Nat.succ (Nat.sqrt n) then Nat.sqrt n else Nat.succ (Nat.sqrt n)) =
    Nat.sqrt (Nat.succ n)
case H.succ
n : ℕ
IH : Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n = Nat.sqrt n
⊢ (if
        Nat.succ n <
          Nat.succ (Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n) *
            Nat.succ (Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n) then
      Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n
    else Nat.succ (Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n)) =
    Nat.sqrt (Nat.succ n)
rw [IH]
case H.succ.inl
n : ℕ
IH : Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n = Nat.sqrt n
h : Nat.succ n < Nat.succ (Nat.sqrt n) * Nat.succ (Nat.sqrt n)
⊢ Nat.sqrt n = Nat.sqrt (Nat.succ n)

case H.succ.inr
n : ℕ
IH : Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n = Nat.sqrt n
h : ¬Nat.succ n < Nat.succ (Nat.sqrt n) * Nat.succ (Nat.sqrt n)
⊢ Nat.succ (Nat.sqrt n) = Nat.sqrt (Nat.succ n)
case H.succ
n : ℕ
IH : Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n = Nat.sqrt n
⊢ (if Nat.succ n < Nat.succ (Nat.sqrt n) * Nat.succ (Nat.sqrt n) then Nat.sqrt n else Nat.succ (Nat.sqrt n)) =
    Nat.sqrt (Nat.succ n)
split_ifs with h
H : ∀ (n : ℕ), Nat.sqrt n = Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n
⊢ Primrec' fun v =>
    Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) (Vector.head v)
H : ∀ (n : ℕ), Nat.sqrt n = Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n
⊢ Primrec' fun v => Nat.sqrt (Vector.head v)
simp [H]
case refine_2
H : ∀ (n : ℕ), Nat.sqrt n = Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n
this :
  Primrec' fun v =>
    Nat.rec 0
      (fun y IH =>
        (fun v =>
            let_fun x := Vector.head v;
            let_fun y := Vector.head (Vector.tail v);
            if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y)
          (y ::ᵥ IH ::ᵥ v))
      (Vector.head v)
⊢ Primrec' fun v =>
    Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) (Vector.head v)

case refine_1
H : ∀ (n : ℕ), Nat.sqrt n = Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n
⊢ Primrec' fun v =>
    let_fun x := Vector.head v;
    let_fun y := Vector.head (Vector.tail v);
    if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y
H : ∀ (n : ℕ), Nat.sqrt n = Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n
⊢ Primrec' fun v =>
    Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) (Vector.head v)
have :=
  @prec' 1 _ _
    (fun v => by
      have x := v.head; have y := v.tail.head;
        exact if x.succ < y.succ * y.succ then y else y.succ)
    head (const 0) ?_
case refine_1
H : ∀ (n : ℕ), Nat.sqrt n = Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n
x1 : Primrec' fun v => Nat.succ (Vector.head v)
⊢ Primrec' fun v =>
    let_fun x := Vector.head v;
    let_fun y := Vector.head (Vector.tail v);
    if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y
case refine_1
H : ∀ (n : ℕ), Nat.sqrt n = Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n
⊢ Primrec' fun v =>
    let_fun x := Vector.head v;
    let_fun y := Vector.head (Vector.tail v);
    if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y
have x1 : @Primrec' 3 fun v => v.head.succ := succ.comp₁ _ head
case refine_1
H : ∀ (n : ℕ), Nat.sqrt n = Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n
x1 : Primrec' fun v => Nat.succ (Vector.head v)
y1 : Primrec' fun v => Nat.succ (Vector.head (Vector.tail v))
⊢ Primrec' fun v =>
    let_fun x := Vector.head v;
    let_fun y := Vector.head (Vector.tail v);
    if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y
case refine_1
H : ∀ (n : ℕ), Nat.sqrt n = Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n
x1 : Primrec' fun v => Nat.succ (Vector.head v)
⊢ Primrec' fun v =>
    let_fun x := Vector.head v;
    let_fun y := Vector.head (Vector.tail v);
    if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y
have y1 : @Primrec' 3 fun v => v.tail.head.succ := succ.comp₁ _ (tail head)
no goals
case refine_1
H : ∀ (n : ℕ), Nat.sqrt n = Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n
x1 : Primrec' fun v => Nat.succ (Vector.head v)
y1 : Primrec' fun v => Nat.succ (Vector.head (Vector.tail v))
⊢ Primrec' fun v =>
    let_fun x := Vector.head v;
    let_fun y := Vector.head (Vector.tail v);
    if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y
exact if_lt x1 (mul.comp₂ _ y1 y1) (tail head) y1
H : ∀ (n : ℕ), Nat.sqrt n = Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n
v : Vector ℕ (1 + 2)
x : ℕ
⊢ ℕ
H : ∀ (n : ℕ), Nat.sqrt n = Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n
v : Vector ℕ (1 + 2)
⊢ ℕ
have x := v.head
H : ∀ (n : ℕ), Nat.sqrt n = Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n
v : Vector ℕ (1 + 2)
x y : ℕ
⊢ ℕ
H : ∀ (n : ℕ), Nat.sqrt n = Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n
v : Vector ℕ (1 + 2)
x : ℕ
⊢ ℕ
have y := v.tail.head
no goals
H : ∀ (n : ℕ), Nat.sqrt n = Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n
v : Vector ℕ (1 + 2)
x y : ℕ
⊢ ℕ
exact if x.succ < y.succ * y.succ then y else y.succ
no goals
case refine_2
H : ∀ (n : ℕ), Nat.sqrt n = Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n
this :
  Primrec' fun v =>
    Nat.rec 0
      (fun y IH =>
        (fun v =>
            let_fun x := Vector.head v;
            let_fun y := Vector.head (Vector.tail v);
            if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y)
          (y ::ᵥ IH ::ᵥ v))
      (Vector.head v)
⊢ Primrec' fun v =>
    Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) (Vector.head v)
exact this
no goals
case H.zero

⊢ Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) Nat.zero = Nat.sqrt Nat.zero
simp
no goals
case H.succ.inl
n : ℕ
IH : Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n = Nat.sqrt n
h : Nat.succ n < Nat.succ (Nat.sqrt n) * Nat.succ (Nat.sqrt n)
⊢ Nat.sqrt n = Nat.sqrt (Nat.succ n)
exact le_antisymm (Nat.sqrt_le_sqrt (Nat.le_succ _)) (Nat.lt_succ_iff.1 <| Nat.sqrt_lt.2 h)
no goals
case H.succ.inr
n : ℕ
IH : Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n = Nat.sqrt n
h : ¬Nat.succ n < Nat.succ (Nat.sqrt n) * Nat.succ (Nat.sqrt n)
⊢ Nat.succ (Nat.sqrt n) = Nat.sqrt (Nat.succ n)
exact
  Nat.eq_sqrt.2 ⟨not_lt.1 h, Nat.sqrt_lt.1 <| Nat.lt_succ_iff.2 <| Nat.sqrt_succ_le_succ_sqrt _⟩