awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.Primrec.List
Goal:
v : List.Vector ℕ (Nat.succ 0 + 1)
simp : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) v.tail.head (fun (y IH : ℕ) ↦ IH - 1) v.head = v.tail.head - v.head
⊢ Eq (α := ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) v.tail.head (fun (y IH : ℕ) ↦ (y ::ᵥ IH ::ᵥ v.tail).tail.head.pred) v.head : ℕ)
    ((fun (a b : ℕ) ↦ b - a) v.head v.tail.head : ℕ)

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.List
Goal:
v : List.Vector ℕ (Nat.succ 0 + 1)
zero : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) v.tail.head (fun (y IH : ℕ) ↦ IH - 1) 0 = v.tail.head - 0
succ :
  ∀ (n : ℕ),
    Nat.rec (motive := fun (x : ℕ) ↦ ℕ) v.tail.head (fun (y IH : ℕ) ↦ IH - 1) n = v.tail.head - n →
      Nat.rec (motive := fun (x : ℕ) ↦ ℕ) v.tail.head (fun (y IH : ℕ) ↦ IH - 1) (n + 1) = v.tail.head - (n + 1)
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) v.tail.head (fun (y IH : ℕ) ↦ IH - 1) v.head = v.tail.head - v.head

Tactic:
induction v.head

Premises used: List.Vector.head
-- Module: Mathlib.Computability.Primrec.List
Goal:
v : List.Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) v.tail.head (fun (y IH : ℕ) ↦ IH - 1) 0 = v.tail.head - 0

Tactic:
simp [*, Nat.sub_add_eq]

Premises used: Nat.sub_add_eq
-- Module: Mathlib.Computability.Primrec.List
Goal:
v : List.Vector ℕ (Nat.succ 0 + 1)
n : ℕ
h : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) v.tail.head (fun (y IH : ℕ) ↦ IH - 1) n = v.tail.head - n
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) v.tail.head (fun (y IH : ℕ) ↦ IH - 1) (n + 1) = v.tail.head - (n + 1)

Tactic:
simp [*, Nat.sub_add_eq]

Premises used: Nat.sub_add_eq
-- Module: Mathlib.Computability.Primrec.List
Goal:
⊢ Primrec' (n := 2) fun (v : List.Vector ℕ 2) ↦ (fun (a b : ℕ) ↦ b - a) v.head v.tail.head

Tactic:
have : @Primrec' 2 fun v ↦ (fun a b ↦ b - a) v.head v.tail.head := by
    refine (prec head (pred.comp₁ _ (tail head))).of_eq fun v => ?_
    simp; induction v.head <;> simp [*, Nat.sub_add_eq]
-- Module: Mathlib.Computability.Primrec.List
Goal:
this : Primrec' (n := 2) fun (v : List.Vector ℕ 2) ↦ (fun (a b : ℕ) ↦ b - a) v.head v.tail.head
⊢ Primrec' (n := 2) fun (v : List.Vector ℕ 2) ↦ v.head - v.tail.head

Tactic:
simpa using comp₂ (fun a b => b - a) this (tail head) head

Premises used: Nat.Primrec'.head, HSub.hSub, Nat.Primrec'.comp₂, Nat.Primrec'.tail
-- Module: Mathlib.Computability.Primrec.List
Goal:
v : List.Vector ℕ (Nat.succ 0 + 1)
simp : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (y IH : ℕ) ↦ v.tail.head + IH) v.head = v.head * v.tail.head
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0
      (fun (y IH : ℕ) ↦ (y ::ᵥ IH ::ᵥ v.tail).tail.tail.head + (y ::ᵥ IH ::ᵥ v.tail).tail.head) v.head =
    v.head * v.tail.head

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.List
Goal:
v : List.Vector ℕ (Nat.succ 0 + 1)
zero : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (y IH : ℕ) ↦ v.tail.head + IH) 0 = 0 * v.tail.head
succ :
  ∀ (n : ℕ),
    Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (y IH : ℕ) ↦ v.tail.head + IH) n = n * v.tail.head →
      Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (y IH : ℕ) ↦ v.tail.head + IH) (n + 1) = (n + 1) * v.tail.head
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (y IH : ℕ) ↦ v.tail.head + IH) v.head = v.head * v.tail.head

Tactic:
induction v.head

Premises used: List.Vector.head
-- Module: Mathlib.Computability.Primrec.List
Goal:
v : List.Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (y IH : ℕ) ↦ v.tail.head + IH) 0 = 0 * v.tail.head

Tactic:
simp [*, Nat.succ_mul]

Premises used: Nat.succ_mul
-- Module: Mathlib.Computability.Primrec.List
Goal:
v : List.Vector ℕ (Nat.succ 0 + 1)
n : ℕ
h : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (y IH : ℕ) ↦ v.tail.head + IH) n = n * v.tail.head
succ : v.tail.head + n * v.tail.head = n * v.tail.head + v.tail.head
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (y IH : ℕ) ↦ v.tail.head + IH) (n + 1) = (n + 1) * v.tail.head

Tactic:
simp [*, Nat.succ_mul]

Premises used: Nat.succ_mul
-- Module: Mathlib.Computability.Primrec.List
Goal:
v : List.Vector ℕ (Nat.succ 0 + 1)
n : ℕ
h : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (y IH : ℕ) ↦ v.tail.head + IH) n = n * v.tail.head
succ succ₁ : n * v.tail.head + v.tail.head = n * v.tail.head + v.tail.head
⊢ v.tail.head + n * v.tail.head = n * v.tail.head + v.tail.head

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
a b f g : List.Vector ℕ n → ℕ
ha : Primrec' a
hb : Primrec' b
hf : Primrec' f
hg : Primrec' g
v : List.Vector ℕ n
zero :
  ∀ (e : b v - a v = 0),
    Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (g v) (fun (y IH : ℕ) ↦ f (y ::ᵥ IH ::ᵥ v).tail.tail) 0 =
      if a v < b v then f v else g v
succ :
  ∀ (n_1 : ℕ) (e : b v - a v = n_1 + 1),
    Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (g v) (fun (y IH : ℕ) ↦ f (y ::ᵥ IH ::ᵥ v).tail.tail) (n_1 + 1) =
      if a v < b v then f v else g v
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (g v) (fun (y IH : ℕ) ↦ f (y ::ᵥ IH ::ᵥ v).tail.tail) (b v - a v) =
    if a v < b v then f v else g v

Tactic:
cases e : b v - a v
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
a b f g : List.Vector ℕ n → ℕ
ha : Primrec' a
hb : Primrec' b
hf : Primrec' f
hg : Primrec' g
v : List.Vector ℕ n
e : b v - a v = 0
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (g v) (fun (y IH : ℕ) ↦ f (y ::ᵥ IH ::ᵥ v).tail.tail) 0 =
    if a v < b v then f v else g v

Tactic:
simp [not_lt.2 (Nat.sub_eq_zero_iff_le.mp e)]

Premises used: Iff.mpr, Nat.sub_eq_zero_iff_le, not_lt, Iff.mp
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
a b f g : List.Vector ℕ n → ℕ
ha : Primrec' a
hb : Primrec' b
hf : Primrec' f
hg : Primrec' g
v : List.Vector ℕ n
n_1 : ℕ
e : b v - a v = n_1 + 1
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (g v) (fun (y IH : ℕ) ↦ f (y ::ᵥ IH ::ᵥ v).tail.tail) (n_1 + 1) =
    if a v < b v then f v else g v

Tactic:
simp [Nat.lt_of_sub_eq_succ e]

Premises used: Nat.lt_of_sub_eq_succ
-- Module: Mathlib.Computability.Primrec.List
Goal:
⊢ Primrec' (n := 2) fun (v : List.Vector ℕ 2) ↦ pair v.head v.tail.head

Tactic:
if_lt head (tail head) (add.comp₂ _ (tail <| mul.comp₂ _ head head) head)
    (add.comp₂ _ (add.comp₂ _ (mul.comp₂ _ head head) head) (tail head))

Premises used: Nat.Primrec'.if_lt, Nat.Primrec'.head, Nat.Primrec'.add, Nat.pair, Nat.Primrec'.comp₂, Nat.Primrec'.tail, Nat.Primrec'.mul
-- Module: Mathlib.Computability.Primrec.List
Goal:
v : List.Vector ℕ 0
rw : 0 = encode (α := List.Vector ℕ 0) nil
⊢ 0 = encode v

Tactic:
rw [v.eq_nil]

Premises used: List.Vector.eq_nil
-- Module: Mathlib.Computability.Primrec.List
Goal:
v : List.Vector ℕ 0
⊢ 0 = encode (α := List.Vector ℕ 0) nil

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.List
Goal:
H :
  ∀ (n : ℕ),
    n.sqrt = Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (x y : ℕ) ↦ if x.succ < y.succ * y.succ then y else y.succ) n
simp :
  Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (x y : ℕ) ↦ if x + 1 < (y + 1) * (y + 1) then y else y + 1) v.head
⊢ Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ v.head.sqrt

Tactic:
simp only [H, succ_eq_add_one]

Premises used: Nat.succ_eq_add_one
-- Module: Mathlib.Computability.Primrec.List
Goal:
H :
  ∀ (n : ℕ),
    n.sqrt = Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (x y : ℕ) ↦ if x.succ < y.succ * y.succ then y else y.succ) n
v : List.Vector ℕ (HAdd.hAdd (α := ℕ) 1 2)
have : (x : ℕ) → ℕ
⊢ ℕ

Tactic:
have x := v.head
-- Module: Mathlib.Computability.Primrec.List
Goal:
H :
  ∀ (n : ℕ),
    n.sqrt = Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (x y : ℕ) ↦ if x.succ < y.succ * y.succ then y else y.succ) n
v : List.Vector ℕ (HAdd.hAdd (α := ℕ) 1 2)
x : ℕ
have : (y : ℕ) → ℕ
⊢ ℕ

Tactic:
have y := v.tail.head
-- Module: Mathlib.Computability.Primrec.List
Goal:
H :
  ∀ (n : ℕ),
    n.sqrt = Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (x y : ℕ) ↦ if x.succ < y.succ * y.succ then y else y.succ) n
v : List.Vector ℕ (HAdd.hAdd (α := ℕ) 1 2)
x y : ℕ
⊢ ℕ

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

Premises used: Nat.succ
-- Module: Mathlib.Computability.Primrec.List
Goal:
H :
  ∀ (n : ℕ),
    n.sqrt = Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (x y : ℕ) ↦ if x.succ < y.succ * y.succ then y else y.succ) n
refine_2 :
  ∀
    (this :
      Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦
        Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0
          (fun (y IH : ℕ) ↦
            (fun (v : List.Vector ℕ (HAdd.hAdd (α := ℕ) 1 2)) ↦
                have x := v.head;
                have y := v.tail.head;
                if x.succ < y.succ * y.succ then y else y.succ)
              (y ::ᵥ IH ::ᵥ v))
          v.head),
    Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦
      Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (x y : ℕ) ↦ if x + 1 < (y + 1) * (y + 1) then y else y + 1) v.head
refine_1 :
  Primrec' (n := HAdd.hAdd (α := ℕ) 1 2) fun (v : List.Vector ℕ (HAdd.hAdd (α := ℕ) 1 2)) ↦
    have x := v.head;
    have y := v.tail.head;
    if x.succ < y.succ * y.succ then y else y.succ
⊢ Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 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) ?_
-- Module: Mathlib.Computability.Primrec.List
Goal:
H :
  ∀ (n : ℕ),
    n.sqrt = Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (x y : ℕ) ↦ if x.succ < y.succ * y.succ then y else y.succ) n
this :
  Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0
      (fun (y IH : ℕ) ↦
        (fun (v : List.Vector ℕ (HAdd.hAdd (α := ℕ) 1 2)) ↦
            have x := v.head;
            have y := v.tail.head;
            if x.succ < y.succ * y.succ then y else y.succ)
          (y ::ᵥ IH ::ᵥ v))
      v.head
⊢ Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (x y : ℕ) ↦ if x + 1 < (y + 1) * (y + 1) then y else y + 1) v.head

Tactic:
this

Premises used: List.Vector.head
-- Module: Mathlib.Computability.Primrec.List
Goal:
H :
  ∀ (n : ℕ),
    n.sqrt = Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (x y : ℕ) ↦ if x.succ < y.succ * y.succ then y else y.succ) n
this :
  Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0
      (fun (y IH : ℕ) ↦
        (fun (v : List.Vector ℕ (HAdd.hAdd (α := ℕ) 1 2)) ↦
            have x := v.head;
            have y := v.tail.head;
            if x.succ < y.succ * y.succ then y else y.succ)
          (y ::ᵥ IH ::ᵥ v))
      v.head
⊢ Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (x y : ℕ) ↦ if x + 1 < (y + 1) * (y + 1) then y else y + 1) v.head

Tactic:
exact this
-- Module: Mathlib.Computability.Primrec.List
Goal:
H :
  ∀ (n : ℕ),
    n.sqrt = Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (x y : ℕ) ↦ if x.succ < y.succ * y.succ then y else y.succ) n
⊢ Primrec' (n := 3) fun (v : List.Vector ℕ 3) ↦ v.head.succ

Tactic:
have x1 : @Primrec' 3 fun v => v.head.succ := succ.comp₁ _ head
-- Module: Mathlib.Computability.Primrec.List
Goal:
H :
  ∀ (n : ℕ),
    n.sqrt = Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (x y : ℕ) ↦ if x.succ < y.succ * y.succ then y else y.succ) n
x1 : Primrec' (n := 3) fun (v : List.Vector ℕ 3) ↦ v.head.succ
⊢ Primrec' (n := 3) fun (v : List.Vector ℕ 3) ↦ v.tail.head.succ

Tactic:
have y1 : @Primrec' 3 fun v => v.tail.head.succ := succ.comp₁ _ (tail head)
-- Module: Mathlib.Computability.Primrec.List
Goal:
H :
  ∀ (n : ℕ),
    n.sqrt = Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (x y : ℕ) ↦ if x.succ < y.succ * y.succ then y else y.succ) n
x1 : Primrec' (n := 3) fun (v : List.Vector ℕ 3) ↦ v.head.succ
y1 : Primrec' (n := 3) fun (v : List.Vector ℕ 3) ↦ v.tail.head.succ
⊢ Primrec' (n := HAdd.hAdd (α := ℕ) 1 2) fun (v : List.Vector ℕ (HAdd.hAdd (α := ℕ) 1 2)) ↦
    have x := v.head;
    have y := v.tail.head;
    if x.succ < y.succ * y.succ then y else y.succ

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

Premises used: Nat.Primrec'.if_lt, Nat.Primrec'.head, Nat.Primrec'.comp₂, Nat.Primrec'.tail, Nat.Primrec'.mul
-- Module: Mathlib.Computability.Primrec.List
Goal:
H :
  ∀ (n : ℕ),
    n.sqrt = Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (x y : ℕ) ↦ if x.succ < y.succ * y.succ then y else y.succ) n
x1 : Primrec' (n := 3) fun (v : List.Vector ℕ 3) ↦ v.head.succ
y1 : Primrec' (n := 3) fun (v : List.Vector ℕ 3) ↦ v.tail.head.succ
⊢ Primrec' (n := HAdd.hAdd (α := ℕ) 1 2) fun (v : List.Vector ℕ (HAdd.hAdd (α := ℕ) 1 2)) ↦
    have x := v.head;
    have 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

Premises used: Nat.Primrec'.if_lt, Nat.Primrec'.head, Nat.Primrec'.comp₂, Nat.Primrec'.tail, Nat.Primrec'.mul
-- Module: Mathlib.Computability.Primrec.List
Goal:
suffices :
  ∀ (n : ℕ),
    n.sqrt = Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (x y : ℕ) ↦ if x.succ < y.succ * y.succ then y else y.succ) n
⊢ Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ v.head.sqrt

Tactic:
suffices H : ∀ n : ℕ, n.sqrt =
      n.rec 0 fun x y => if x.succ < y.succ * y.succ then y else y.succ by
    simp only [H, succ_eq_add_one]
    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) ?_
    · exact this
    have x1 : @Primrec' 3 fun v => v.head.succ := succ.comp₁ _ head
    have y1 : @Primrec' 3 fun v => v.tail.head.succ := succ.comp₁ _ (tail head)
    exact if_lt x1 (mul.comp₂ _ y1 y1) (tail head) y1
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
symm : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (x y : ℕ) ↦ if x.succ < y.succ * y.succ then y else y.succ) n = n.sqrt
⊢ n.sqrt = Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (x y : ℕ) ↦ if x.succ < y.succ * y.succ then y else y.succ) n

Tactic:
symm
-- Module: Mathlib.Computability.Primrec.List
Goal:
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (x y : ℕ) ↦ if x.succ < y.succ * y.succ then y else y.succ) 0 = Nat.sqrt 0

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
IH : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (x y : ℕ) ↦ if x.succ < y.succ * y.succ then y else y.succ) n = n.sqrt
succ :
  (if
        n + 1 <
          HAdd.hAdd (α := ℕ) (β := ℕ)
              (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (x y : ℕ) ↦ if x + 1 < (y + 1) * (y + 1) then y else y + 1)
                  n :
                ℕ)
              (1 : ℕ) *
            HAdd.hAdd (α := ℕ) (β := ℕ)
              (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (x y : ℕ) ↦ if x + 1 < (y + 1) * (y + 1) then y else y + 1)
                  n :
                ℕ)
              (1 : ℕ) then
      Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (x y : ℕ) ↦ if x + 1 < (y + 1) * (y + 1) then y else y + 1) n
    else
      HAdd.hAdd (α := ℕ) (β := ℕ)
        (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (x y : ℕ) ↦ if x + 1 < (y + 1) * (y + 1) then y else y + 1) n : ℕ)
        (1 : ℕ)) =
    (n + 1).sqrt
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (x y : ℕ) ↦ if x.succ < y.succ * y.succ then y else y.succ) (n + 1) =
    (n + 1).sqrt

Tactic:
dsimp
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
IH : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (x y : ℕ) ↦ if x.succ < y.succ * y.succ then y else y.succ) n = n.sqrt
succ : (if n + 1 < (n.sqrt + 1) * (n.sqrt + 1) then n.sqrt else n.sqrt + 1) = (n + 1).sqrt
⊢ (if
        n + 1 <
          HAdd.hAdd (α := ℕ) (β := ℕ)
              (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (x y : ℕ) ↦ if x + 1 < (y + 1) * (y + 1) then y else y + 1)
                  n :
                ℕ)
              (1 : ℕ) *
            HAdd.hAdd (α := ℕ) (β := ℕ)
              (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (x y : ℕ) ↦ if x + 1 < (y + 1) * (y + 1) then y else y + 1)
                  n :
                ℕ)
              (1 : ℕ) then
      Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (x y : ℕ) ↦ if x + 1 < (y + 1) * (y + 1) then y else y + 1) n
    else
      HAdd.hAdd (α := ℕ) (β := ℕ)
        (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (x y : ℕ) ↦ if x + 1 < (y + 1) * (y + 1) then y else y + 1) n : ℕ)
        (1 : ℕ)) =
    (n + 1).sqrt

Tactic:
rw [IH]
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
IH : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (x y : ℕ) ↦ if x.succ < y.succ * y.succ then y else y.succ) n = n.sqrt
pos : ∀ (h : n + 1 < (n.sqrt + 1) * (n.sqrt + 1)), n.sqrt = (n + 1).sqrt
neg : ∀ (h : ¬n + 1 < (n.sqrt + 1) * (n.sqrt + 1)), n.sqrt + 1 = (n + 1).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
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
IH : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 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:
le_antisymm (Nat.sqrt_le_sqrt (Nat.le_succ _)) (Nat.lt_succ_iff.1 <| Nat.sqrt_lt.2 h)

Premises used: Iff.mpr, Nat.sqrt_lt, Nat.le_succ, le_antisymm, Nat.sqrt_le_sqrt, Nat.lt_succ_iff, Iff.mp
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
IH : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 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)

Premises used: Iff.mpr, Nat.sqrt_lt, Nat.le_succ, le_antisymm, Nat.sqrt_le_sqrt, Nat.lt_succ_iff, Iff.mp
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
IH : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 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

Tactic:
Nat.eq_sqrt.2
        ⟨not_lt.1 h, Nat.sqrt_lt.1 <| Nat.lt_succ_iff.2 <| Nat.sqrt_succ_le_succ_sqrt _⟩

Premises used: Iff.mpr, Nat.sqrt_lt, Nat.eq_sqrt, not_lt, Nat.lt_succ_iff, And.intro, Iff.mp, Nat.sqrt_succ_le_succ_sqrt
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
IH : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 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

Tactic:
exact Nat.eq_sqrt.2
        ⟨not_lt.1 h, Nat.sqrt_lt.1 <| Nat.lt_succ_iff.2 <| Nat.sqrt_succ_le_succ_sqrt _⟩

Premises used: Iff.mpr, Nat.sqrt_lt, Nat.eq_sqrt, not_lt, Nat.lt_succ_iff, And.intro, Iff.mp, Nat.sqrt_succ_le_succ_sqrt
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
zero :
  Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (x y : ℕ) ↦ if x.succ < y.succ * y.succ then y else y.succ) 0 = Nat.sqrt 0
succ :
  ∀ (n : ℕ)
    (IH :
      Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (x y : ℕ) ↦ if x.succ < y.succ * y.succ then y else y.succ) n =
        n.sqrt),
    Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (x y : ℕ) ↦ if x.succ < y.succ * y.succ then y else y.succ) (n + 1) =
      (n + 1).sqrt
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (x y : ℕ) ↦ if x.succ < y.succ * y.succ then y else y.succ) n = n.sqrt

Tactic:
induction n with
  | zero => simp
  | succ n IH =>
    dsimp; rw [IH]; split_ifs with h
    · exact le_antisymm (Nat.sqrt_le_sqrt (Nat.le_succ _)) (Nat.lt_succ_iff.1 <| Nat.sqrt_lt.2 h)
    · exact Nat.eq_sqrt.2
        ⟨not_lt.1 h, Nat.sqrt_lt.1 <| Nat.lt_succ_iff.2 <| Nat.sqrt_succ_le_succ_sqrt _⟩

Premises used: Nat.Primrec'.succ, Nat.Primrec'.zero
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
⊢ Primrec' (n := n) fun (v : List.Vector ℕ n) ↦ (f v).sqrt

Tactic:
have s := sqrt.comp₁ _ hf
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' (n := n) fun (v : List.Vector ℕ n) ↦ (f v).sqrt
⊢ Primrec' (n := n) fun (v : List.Vector ℕ n) ↦ f v - (f v).sqrt * (f v).sqrt

Tactic:
have fss := sub.comp₂ _ hf (mul.comp₂ _ s s)
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' (n := n) fun (v : List.Vector ℕ n) ↦ (f v).sqrt
fss : Primrec' (n := n) fun (v : List.Vector ℕ n) ↦ f v - (f v).sqrt * (f v).sqrt
⊢ Primrec' (n := n) fun (v : List.Vector ℕ n) ↦ (unpair (f v)).1

Tactic:
(if_lt fss s fss s).of_eq fun v => ?_

Premises used: Nat.Primrec'.if_lt, Nat.Primrec'.of_eq
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' (n := n) fun (v : List.Vector ℕ n) ↦ (f v).sqrt
fss : Primrec' (n := n) fun (v : List.Vector ℕ n) ↦ f v - (f v).sqrt * (f v).sqrt
refine :
  ∀ (v : List.Vector ℕ n),
    (if f v - (f v).sqrt * (f v).sqrt < (f v).sqrt then f v - (f v).sqrt * (f v).sqrt else (f v).sqrt) =
      (unpair (f v)).1
⊢ Primrec' (n := n) fun (v : List.Vector ℕ n) ↦ (unpair (f v)).1

Tactic:
refine (if_lt fss s fss s).of_eq fun v => ?_

Premises used: Nat.Primrec'.if_lt, Nat.Primrec'.of_eq
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' (n := n) fun (v : List.Vector ℕ n) ↦ (f v).sqrt
fss : Primrec' (n := n) fun (v : List.Vector ℕ n) ↦ f v - (f v).sqrt * (f v).sqrt
v : List.Vector ℕ n
pos :
  f v - (f v).sqrt * (f v).sqrt < (f v).sqrt →
    f v - (f v).sqrt * (f v).sqrt = (f v - (f v).sqrt * (f v).sqrt, (f v).sqrt).1
neg :
  ¬f v - (f v).sqrt * (f v).sqrt < (f v).sqrt → (f v).sqrt = ((f v).sqrt, f v - (f v).sqrt * (f v).sqrt - (f v).sqrt).1
⊢ (if f v - (f v).sqrt * (f v).sqrt < (f v).sqrt then f v - (f v).sqrt * (f v).sqrt else (f v).sqrt) =
    (if f v - (f v).sqrt * (f v).sqrt < (f v).sqrt then (f v - (f v).sqrt * (f v).sqrt, (f v).sqrt)
      else ((f v).sqrt, f v - (f v).sqrt * (f v).sqrt - (f v).sqrt)).1

Tactic:
split_ifs
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' (n := n) fun (v : List.Vector ℕ n) ↦ (f v).sqrt
fss : Primrec' (n := n) fun (v : List.Vector ℕ n) ↦ f v - (f v).sqrt * (f v).sqrt
v : List.Vector ℕ n
h : f v - (f v).sqrt * (f v).sqrt < (f v).sqrt
⊢ f v - (f v).sqrt * (f v).sqrt = (f v - (f v).sqrt * (f v).sqrt, (f v).sqrt).1

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' (n := n) fun (v : List.Vector ℕ n) ↦ (f v).sqrt
fss : Primrec' (n := n) fun (v : List.Vector ℕ n) ↦ f v - (f v).sqrt * (f v).sqrt
v : List.Vector ℕ n
h : ¬f v - (f v).sqrt * (f v).sqrt < (f v).sqrt
⊢ (f v).sqrt = ((f v).sqrt, f v - (f v).sqrt * (f v).sqrt - (f v).sqrt).1

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' (n := n) fun (v : List.Vector ℕ n) ↦ (f v).sqrt
fss : Primrec' (n := n) fun (v : List.Vector ℕ n) ↦ f v - (f v).sqrt * (f v).sqrt
⊢ Primrec' (n := n) fun (v : List.Vector ℕ n) ↦ (unpair (f v)).2

Tactic:
(if_lt fss s s (sub.comp₂ _ fss s)).of_eq fun v => ?_

Premises used: Nat.Primrec'.sub, Nat.Primrec'.if_lt, Nat.Primrec'.comp₂, Nat.Primrec'.of_eq
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' (n := n) fun (v : List.Vector ℕ n) ↦ (f v).sqrt
fss : Primrec' (n := n) fun (v : List.Vector ℕ n) ↦ f v - (f v).sqrt * (f v).sqrt
refine :
  ∀ (v : List.Vector ℕ n),
    (if f v - (f v).sqrt * (f v).sqrt < (f v).sqrt then (f v).sqrt else f v - (f v).sqrt * (f v).sqrt - (f v).sqrt) =
      (unpair (f v)).2
⊢ Primrec' (n := n) fun (v : List.Vector ℕ n) ↦ (unpair (f v)).2

Tactic:
refine (if_lt fss s s (sub.comp₂ _ fss s)).of_eq fun v => ?_

Premises used: Nat.Primrec'.sub, Nat.Primrec'.if_lt, Nat.Primrec'.comp₂, Nat.Primrec'.of_eq