-- Mathlib/Computability/Primrec.lean
theorem sqrt : @Primrec' 1 fun v => v.head.sqrt

Proof state:
H : ∀ (n : ℕ), n.sqrt = Nat.rec 0 (fun x y => if x.succ < y.succ * y.succ then y else y.succ) n
v : List.Vector ℕ (1 + 2)
x : ℕ
⊢ ℕ

Tactic:
have y := v.tail.head

Result:
H : ∀ (n : ℕ), n.sqrt = Nat.rec 0 (fun x y => if x.succ < y.succ * y.succ then y else y.succ) n
v : List.Vector ℕ (1 + 2)
x y : ℕ
⊢ ℕ

Proof state:
H : ∀ (n : ℕ), n.sqrt = Nat.rec 0 (fun x y => if x.succ < y.succ * y.succ then y else y.succ) n
v : List.Vector ℕ (1 + 2)
⊢ ℕ

Tactic:
have x := v.head

Result:
H : ∀ (n : ℕ), n.sqrt = Nat.rec 0 (fun x y => if x.succ < y.succ * y.succ then y else y.succ) n
v : List.Vector ℕ (1 + 2)
x : ℕ
⊢ ℕ

Proof state:
n : ℕ
⊢ Nat.rec 0 (fun x y => if x.succ < y.succ * y.succ then y else y.succ) n = n.sqrt

Tactic:
induction' n with n IH

Result:
case zero

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

case succ
n : ℕ
IH : Nat.rec 0 (fun x y => if x.succ < y.succ * y.succ then y else y.succ) n = n.sqrt
⊢ Nat.rec 0 (fun x y => if x.succ < y.succ * y.succ then y else y.succ) (n + 1) = (n + 1).sqrt

Proof state:
⊢ ∀ (n : ℕ), n.sqrt = Nat.rec 0 (fun x y => if x.succ < y.succ * y.succ then y else y.succ) n

Tactic:
introv

Result:
n : ℕ
⊢ n.sqrt = Nat.rec 0 (fun x y => if x.succ < y.succ * y.succ then y else y.succ) n

Proof state:
case zero

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

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
⊢ n.sqrt = Nat.rec 0 (fun x y => if x.succ < y.succ * y.succ then y else y.succ) n

Tactic:
symm

Result:
n : ℕ
⊢ Nat.rec 0 (fun x y => if x.succ < y.succ * y.succ then y else y.succ) n = n.sqrt

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

Tactic:
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) ?_

Result:
case refine_2
H : ∀ (n : ℕ), n.sqrt = Nat.rec 0 (fun x y => if x.succ < y.succ * y.succ then y else y.succ) n
this :
  Primrec' fun v =>
    Nat.rec 0
      (fun y IH =>
        (fun v =>
            let_fun x := v.head;
            let_fun y := v.tail.head;
            if x.succ < y.succ * y.succ then y else y.succ)
          (y ::ᵥ IH ::ᵥ v))
      v.head
⊢ Primrec' fun v => Nat.rec 0 (fun x y => if x + 1 < (y + 1) * (y + 1) then y else y + 1) v.head

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

Proof state:
H : ∀ (n : ℕ), n.sqrt = Nat.rec 0 (fun x y => if x.succ < y.succ * y.succ then y else y.succ) n
v : List.Vector ℕ (1 + 2)
x y : ℕ
⊢ ℕ

Tactic:
exact if x.succ < y.succ * y.succ then y else y.succ

Result:
no goals

Proof state:
case refine_2
H : ∀ (n : ℕ), n.sqrt = Nat.rec 0 (fun x y => if x.succ < y.succ * y.succ then y else y.succ) n
this :
  Primrec' fun v =>
    Nat.rec 0
      (fun y IH =>
        (fun v =>
            let_fun x := v.head;
            let_fun y := v.tail.head;
            if x.succ < y.succ * y.succ then y else y.succ)
          (y ::ᵥ IH ::ᵥ v))
      v.head
⊢ Primrec' fun v => Nat.rec 0 (fun x y => if x + 1 < (y + 1) * (y + 1) then y else y + 1) v.head

Tactic:
exact this

Result:
no goals

Proof state:
case succ
n : ℕ
IH : Nat.rec 0 (fun x y => if x.succ < y.succ * y.succ then y else y.succ) n = n.sqrt
⊢ Nat.rec 0 (fun x y => if x.succ < y.succ * y.succ then y else y.succ) (n + 1) = (n + 1).sqrt

Tactic:
dsimp

Result:
case succ
n : ℕ
IH : Nat.rec 0 (fun x y => if x.succ < y.succ * y.succ then y else y.succ) n = n.sqrt
⊢ (if
        n + 1 <
          (Nat.rec 0 (fun x y => if x + 1 < (y + 1) * (y + 1) then y else y + 1) n + 1) *
            (Nat.rec 0 (fun x y => if x + 1 < (y + 1) * (y + 1) then y else y + 1) n + 1) then
      Nat.rec 0 (fun x y => if x + 1 < (y + 1) * (y + 1) then y else y + 1) n
    else Nat.rec 0 (fun x y => if x + 1 < (y + 1) * (y + 1) then y else y + 1) n + 1) =
    (n + 1).sqrt

Proof state:
case pos
n : ℕ
IH : Nat.rec 0 (fun x y => if x.succ < y.succ * y.succ then y else y.succ) n = n.sqrt
h : n + 1 < (n.sqrt + 1) * (n.sqrt + 1)
⊢ n.sqrt = (n + 1).sqrt

Tactic:
exact le_antisymm (Nat.sqrt_le_sqrt (Nat.le_succ _)) (Nat.lt_succ_iff.1 <| Nat.sqrt_lt.2 h)

Result:
no goals

Proof state:
case refine_1
H : ∀ (n : ℕ), n.sqrt = Nat.rec 0 (fun x y => if x.succ < y.succ * y.succ then y else y.succ) n
x1 : Primrec' fun v => v.head.succ
y1 : Primrec' fun v => v.tail.head.succ
⊢ Primrec' fun v =>
    let_fun x := v.head;
    let_fun y := v.tail.head;
    if x.succ < y.succ * y.succ then y else y.succ

Tactic:
exact if_lt x1 (mul.comp₂ _ y1 y1) (tail head) y1

Result:
no goals

Proof state:
case succ
n : ℕ
IH : Nat.rec 0 (fun x y => if x.succ < y.succ * y.succ then y else y.succ) n = n.sqrt
⊢ (if n + 1 < (n.sqrt + 1) * (n.sqrt + 1) then n.sqrt else n.sqrt + 1) = (n + 1).sqrt

Tactic:
split_ifs with h

Result:
case pos
n : ℕ
IH : Nat.rec 0 (fun x y => if x.succ < y.succ * y.succ then y else y.succ) n = n.sqrt
h : n + 1 < (n.sqrt + 1) * (n.sqrt + 1)
⊢ n.sqrt = (n + 1).sqrt

case neg
n : ℕ
IH : Nat.rec 0 (fun x y => if x.succ < y.succ * y.succ then y else y.succ) n = n.sqrt
h : ¬n + 1 < (n.sqrt + 1) * (n.sqrt + 1)
⊢ n.sqrt + 1 = (n + 1).sqrt

Proof state:
case refine_1
H : ∀ (n : ℕ), n.sqrt = Nat.rec 0 (fun x y => if x.succ < y.succ * y.succ then y else y.succ) n
x1 : Primrec' fun v => v.head.succ
⊢ Primrec' fun v =>
    let_fun x := v.head;
    let_fun y := v.tail.head;
    if x.succ < y.succ * y.succ then y else y.succ

Tactic:
have y1 : @Primrec' 3 fun v => v.tail.head.succ := succ.comp₁ _ (tail head)

Result:
case refine_1
H : ∀ (n : ℕ), n.sqrt = Nat.rec 0 (fun x y => if x.succ < y.succ * y.succ then y else y.succ) n
x1 : Primrec' fun v => v.head.succ
y1 : Primrec' fun v => v.tail.head.succ
⊢ Primrec' fun v =>
    let_fun x := v.head;
    let_fun y := v.tail.head;
    if x.succ < y.succ * y.succ then y else y.succ

Proof state:
case succ
n : ℕ
IH : Nat.rec 0 (fun x y => if x.succ < y.succ * y.succ then y else y.succ) n = n.sqrt
⊢ (if
        n + 1 <
          (Nat.rec 0 (fun x y => if x + 1 < (y + 1) * (y + 1) then y else y + 1) n + 1) *
            (Nat.rec 0 (fun x y => if x + 1 < (y + 1) * (y + 1) then y else y + 1) n + 1) then
      Nat.rec 0 (fun x y => if x + 1 < (y + 1) * (y + 1) then y else y + 1) n
    else Nat.rec 0 (fun x y => if x + 1 < (y + 1) * (y + 1) then y else y + 1) n + 1) =
    (n + 1).sqrt

Tactic:
rw [IH]

Result:
case succ
n : ℕ
IH : Nat.rec 0 (fun x y => if x.succ < y.succ * y.succ then y else y.succ) n = n.sqrt
⊢ (if n + 1 < (n.sqrt + 1) * (n.sqrt + 1) then n.sqrt else n.sqrt + 1) = (n + 1).sqrt

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

Tactic:
simp only [H, succ_eq_add_one]

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

Proof state:
case refine_1
H : ∀ (n : ℕ), n.sqrt = Nat.rec 0 (fun x y => if x.succ < y.succ * y.succ then y else y.succ) n
⊢ Primrec' fun v =>
    let_fun x := v.head;
    let_fun y := v.tail.head;
    if x.succ < y.succ * y.succ then y else y.succ

Tactic:
have x1 : @Primrec' 3 fun v => v.head.succ := succ.comp₁ _ head

Result:
case refine_1
H : ∀ (n : ℕ), n.sqrt = Nat.rec 0 (fun x y => if x.succ < y.succ * y.succ then y else y.succ) n
x1 : Primrec' fun v => v.head.succ
⊢ Primrec' fun v =>
    let_fun x := v.head;
    let_fun y := v.tail.head;
    if x.succ < y.succ * y.succ then y else y.succ