awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
v : List.Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (y IH : ℕ) ↦ v.tail.head + IH) v.head = v.head * v.tail.head
have zero : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (y IH : ℕ) ↦ v.tail.head + IH) 0 = 0 * v.tail.head
Tactic: induction v.head
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
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
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (y IH : ℕ) ↦ v.tail.head + IH) v.head = v.head * v.tail.head
have 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
Tactic: induction v.head
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
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
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (y IH : ℕ) ↦ v.tail.head + IH) (n + 1) = (n + 1) * v.tail.head
have succ : v.tail.head + n * v.tail.head = n * v.tail.head + v.tail.head
Tactic: simp [*, Nat.succ_mul]
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
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
⊢ v.tail.head + n * v.tail.head = n * v.tail.head + v.tail.head
have succ : n * v.tail.head + v.tail.head = n * v.tail.head + v.tail.head
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
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
⊢ 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
have 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
Tactic: cases e : b v - a v
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
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
⊢ 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
have 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
Tactic: cases e : b v - a v
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
v : List.Vector ℕ 0
⊢ 0 = encode v
have rw : 0 = encode (α := List.Vector ℕ 0) nil
Tactic: rw [v.eq_nil]
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
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 := 1) fun (v : List.Vector ℕ 1) ↦ v.head.sqrt
have 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
Tactic: simp only [H, succ_eq_add_one]
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
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 have : (x : ℕ) → ℕ
Tactic: have x := v.head
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
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 have : (y : ℕ) → ℕ
Tactic: have y := v.tail.head
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
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 := 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
have 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
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) ?_
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
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
⊢ 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
have 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
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) ?_
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (hypothesis)
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 := 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
have x1 : Primrec' (n := 3) fun (v : List.Vector ℕ 3) ↦ v.head.succ
Tactic: have x1 : @Primrec' 3 fun v => v.head.succ := succ.comp₁ _ head
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (hypothesis)
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 := 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
have y1 : 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)
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
⊢ Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ v.head.sqrt
have 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
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
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
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
have 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
Tactic: symm
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
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
⊢ (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
have succ : (if n + 1 < (n.sqrt + 1) * (n.sqrt + 1) then n.sqrt else n.sqrt + 1) = (n + 1).sqrt
Tactic: rw [IH]
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
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
⊢ (if n + 1 < (n.sqrt + 1) * (n.sqrt + 1) then n.sqrt else n.sqrt + 1) = (n + 1).sqrt
have pos : ∀ (h : n + 1 < (n.sqrt + 1) * (n.sqrt + 1)), n.sqrt = (n + 1).sqrt
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
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
⊢ (if n + 1 < (n.sqrt + 1) * (n.sqrt + 1) then n.sqrt else n.sqrt + 1) = (n + 1).sqrt
have neg : ∀ (h : ¬n + 1 < (n.sqrt + 1) * (n.sqrt + 1)), n.sqrt + 1 = (n + 1).sqrt
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
n : ℕ
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (x y : ℕ) ↦ if x.succ < y.succ * y.succ then y else y.succ) n = n.sqrt
have 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
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 _⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
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
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (x y : ℕ) ↦ if x.succ < y.succ * y.succ then y else y.succ) n = n.sqrt
have 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
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 _⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (hypothesis)
Goal:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
⊢ Primrec' (n := n) fun (v : List.Vector ℕ n) ↦ (unpair (f v)).1
have s : Primrec' (n := n) fun (v : List.Vector ℕ n) ↦ (f v).sqrt
Tactic: have s := sqrt.comp₁ _ hf
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (hypothesis)
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) ↦ (unpair (f v)).1
have fss : 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)
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
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
have 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
Tactic: refine (if_lt fss s fss s).of_eq fun v => ?_
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
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
⊢ (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
have 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
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
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
⊢ (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
have 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
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (hypothesis)
Goal:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
⊢ Primrec' (n := n) fun (v : List.Vector ℕ n) ↦ (unpair (f v)).2
have s : Primrec' (n := n) fun (v : List.Vector ℕ n) ↦ (f v).sqrt
Tactic: have s := sqrt.comp₁ _ hf
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (hypothesis)
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) ↦ (unpair (f v)).2
have fss : 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)
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
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
have 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
Tactic: refine (if_lt fss s s (sub.comp₂ _ fss s)).of_eq fun v => ?_
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
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
⊢ (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) =
    (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)).2
have pos : f v - (f v).sqrt * (f v).sqrt < (f v).sqrt → (f v).sqrt = (f v - (f v).sqrt * (f v).sqrt, (f v).sqrt).2
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
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).sqrt = (f v - (f v).sqrt * (f v).sqrt, (f v).sqrt).2
⊢ (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) =
    (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)).2
have neg : ¬f v - (f v).sqrt * (f v).sqrt < (f v).sqrt →
  f v - (f v).sqrt * (f v).sqrt - (f v).sqrt = ((f v).sqrt, f v - (f v).sqrt * (f v).sqrt - (f v).sqrt).2
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
n : ℕ
f_1 : List.Vector ℕ n → ℕ
f : ℕ → ℕ
hf : Nat.Primrec f
⊢ Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ f v.head
have zero : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ (fun (x : ℕ) ↦ (0 : ℕ)) v.head
Tactic: induction hf with
  | zero => exact const 0
  | succ => exact succ
  | left => exact unpair₁ head
  | right => exact unpair₂ head
  | pair _ _ hf hg => exact natPair.comp₂ _ hf hg
  | comp _ _ hf hg => exact hf.comp₁ _ hg
  | prec _ _ hf hg =>
    simpa using
      prec' (unpair₂ head) (hf.comp₁ _ (unpair₁ head))
        (hg.comp₁ _ <|
          natPair.comp₂ _ (unpair₁ <| tail <| tail head) (natPair.comp₂ _ head (tail head)))
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
n : ℕ
f_1 : List.Vector ℕ n → ℕ
f : ℕ → ℕ
hf : Nat.Primrec f
zero : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ (fun (x : ℕ) ↦ (0 : ℕ)) v.head
⊢ Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ f v.head
have succ : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ v.head.succ
Tactic: induction hf with
  | zero => exact const 0
  | succ => exact succ
  | left => exact unpair₁ head
  | right => exact unpair₂ head
  | pair _ _ hf hg => exact natPair.comp₂ _ hf hg
  | comp _ _ hf hg => exact hf.comp₁ _ hg
  | prec _ _ hf hg =>
    simpa using
      prec' (unpair₂ head) (hf.comp₁ _ (unpair₁ head))
        (hg.comp₁ _ <|
          natPair.comp₂ _ (unpair₁ <| tail <| tail head) (natPair.comp₂ _ head (tail head)))
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
n : ℕ
f_1 : List.Vector ℕ n → ℕ
f : ℕ → ℕ
hf : Nat.Primrec f
zero : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ (fun (x : ℕ) ↦ (0 : ℕ)) v.head
succ : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ v.head.succ
⊢ Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ f v.head
have left : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ (fun (n : ℕ) ↦ (unpair n).1) v.head
Tactic: induction hf with
  | zero => exact const 0
  | succ => exact succ
  | left => exact unpair₁ head
  | right => exact unpair₂ head
  | pair _ _ hf hg => exact natPair.comp₂ _ hf hg
  | comp _ _ hf hg => exact hf.comp₁ _ hg
  | prec _ _ hf hg =>
    simpa using
      prec' (unpair₂ head) (hf.comp₁ _ (unpair₁ head))
        (hg.comp₁ _ <|
          natPair.comp₂ _ (unpair₁ <| tail <| tail head) (natPair.comp₂ _ head (tail head)))
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
n : ℕ
f_1 : List.Vector ℕ n → ℕ
f : ℕ → ℕ
hf : Nat.Primrec f
zero : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ (fun (x : ℕ) ↦ (0 : ℕ)) v.head
succ : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ v.head.succ
left : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ (fun (n : ℕ) ↦ (unpair n).1) v.head
⊢ Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ f v.head
have right : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ (fun (n : ℕ) ↦ (unpair n).2) v.head
Tactic: induction hf with
  | zero => exact const 0
  | succ => exact succ
  | left => exact unpair₁ head
  | right => exact unpair₂ head
  | pair _ _ hf hg => exact natPair.comp₂ _ hf hg
  | comp _ _ hf hg => exact hf.comp₁ _ hg
  | prec _ _ hf hg =>
    simpa using
      prec' (unpair₂ head) (hf.comp₁ _ (unpair₁ head))
        (hg.comp₁ _ <|
          natPair.comp₂ _ (unpair₁ <| tail <| tail head) (natPair.comp₂ _ head (tail head)))
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
n : ℕ
f_1 : List.Vector ℕ n → ℕ
f : ℕ → ℕ
hf : Nat.Primrec f
zero : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ (fun (x : ℕ) ↦ (0 : ℕ)) v.head
succ : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ v.head.succ
left : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ (fun (n : ℕ) ↦ (unpair n).1) v.head
right : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ (fun (n : ℕ) ↦ (unpair n).2) v.head
⊢ Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ f v.head
have pair : ∀ {f g : ℕ → ℕ},
  Nat.Primrec f →
    Nat.Primrec g →
      ∀ (hf : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ f v.head)
        (hg : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ g v.head),
        Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ (fun (n : ℕ) ↦ pair (f n) (g n)) v.head
Tactic: induction hf with
  | zero => exact const 0
  | succ => exact succ
  | left => exact unpair₁ head
  | right => exact unpair₂ head
  | pair _ _ hf hg => exact natPair.comp₂ _ hf hg
  | comp _ _ hf hg => exact hf.comp₁ _ hg
  | prec _ _ hf hg =>
    simpa using
      prec' (unpair₂ head) (hf.comp₁ _ (unpair₁ head))
        (hg.comp₁ _ <|
          natPair.comp₂ _ (unpair₁ <| tail <| tail head) (natPair.comp₂ _ head (tail head)))
Cleared hypotheses: hf