awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
m n : ℕ
g : Fin n → List.Vector ℕ m →. ℕ
hg : ∀ (i : Fin n), ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> g i v
⊢ ∃ (c : Code),
    ∀ (v : List.Vector ℕ m),
      c.eval (↑v : List ℕ) =
        Functor.map (α := { l : List ℕ // l.length = n }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = n))
          (Vector.mOfFn fun (i : Fin n) ↦ g i v)
have zero : ∀ {g : Fin 0 → List.Vector ℕ m →. ℕ}
  (hg : ∀ (i : Fin 0), ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> g i v),
  ∃ (c : Code),
    ∀ (v : List.Vector ℕ m),
      c.eval (↑v : List ℕ) =
        Functor.map (α := { l : List ℕ // l.length = 0 }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = 0))
          (Vector.mOfFn fun (i : Fin 0) ↦ g i v)
Tactic: induction n with
  | zero => exact ⟨nil, fun v => by simp [Vector.mOfFn]; rfl⟩
  | succ n IH =>
    obtain ⟨cg, hg₁⟩ := hg 0
    obtain ⟨cl, hl⟩ := IH fun i => hg i.succ
    exact
      ⟨cons cg cl, fun v => by
        simp [Vector.mOfFn, hg₁, hl]
        rfl⟩
Cleared hypotheses: n, g, hg
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
m n : ℕ
g : Fin n → List.Vector ℕ m →. ℕ
hg : ∀ (i : Fin n), ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> g i v
zero :
  ∀ {g : Fin 0 → List.Vector ℕ m →. ℕ}
    (hg : ∀ (i : Fin 0), ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> g i v),
    ∃ (c : Code),
      ∀ (v : List.Vector ℕ m),
        c.eval (↑v : List ℕ) =
          Functor.map (α := { l : List ℕ // l.length = 0 }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = 0))
            (Vector.mOfFn fun (i : Fin 0) ↦ g i v)
⊢ ∃ (c : Code),
    ∀ (v : List.Vector ℕ m),
      c.eval (↑v : List ℕ) =
        Functor.map (α := { l : List ℕ // l.length = n }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = n))
          (Vector.mOfFn fun (i : Fin n) ↦ g i v)
have succ : ∀ (n : ℕ)
  (IH :
    ∀ {g : Fin n → List.Vector ℕ m →. ℕ}
      (hg : ∀ (i : Fin n), ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> g i v),
      ∃ (c : Code),
        ∀ (v : List.Vector ℕ m),
          c.eval (↑v : List ℕ) =
            Functor.map (α := { l : List ℕ // l.length = n }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = n))
              (Vector.mOfFn fun (i : Fin n) ↦ g i v))
  {g : Fin (n + 1) → List.Vector ℕ m →. ℕ}
  (hg : ∀ (i : Fin (n + 1)), ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> g i v),
  ∃ (c : Code),
    ∀ (v : List.Vector ℕ m),
      c.eval (↑v : List ℕ) =
        Functor.map (α := { l : List ℕ // l.length = n + 1 }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = n + 1))
          (Vector.mOfFn fun (i : Fin (n + 1)) ↦ g i v)
Tactic: induction n with
  | zero => exact ⟨nil, fun v => by simp [Vector.mOfFn]; rfl⟩
  | succ n IH =>
    obtain ⟨cg, hg₁⟩ := hg 0
    obtain ⟨cl, hl⟩ := IH fun i => hg i.succ
    exact
      ⟨cons cg cl, fun v => by
        simp [Vector.mOfFn, hg₁, hl]
        rfl⟩
Cleared hypotheses: n, g, hg
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
n : ℕ
f : List.Vector ℕ n →. ℕ
n_1 : ℕ
f_1 : List.Vector ℕ n_1 → ℕ
n_2 : ℕ
i : Fin n_2
⊢ ∃ (c : Code),
    ∀ (v : List.Vector ℕ n_2),
      c.eval (↑v : List ℕ) = pure <$> (↑fun (v : List.Vector ℕ n_2) ↦ v.get i : List.Vector ℕ n_2 →. ℕ) v
have prim : ∀ (n : ℕ),
  ∃ (c : Code),
    ∀ (v : List.Vector ℕ n.succ),
      c.eval (↑v : List ℕ) = pure <$> (↑fun (v : List.Vector ℕ n.succ) ↦ v.get 0 : List.Vector ℕ n.succ →. ℕ) v
Tactic: refine Fin.succRec (fun n => ?_) (fun n i IH => ?_) i
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
n : ℕ
f : List.Vector ℕ n →. ℕ
n_1 : ℕ
f_1 : List.Vector ℕ n_1 → ℕ
n_2 : ℕ
i : Fin n_2
prim :
  ∀ (n : ℕ),
    ∃ (c : Code),
      ∀ (v : List.Vector ℕ n.succ),
        c.eval (↑v : List ℕ) = pure <$> (↑fun (v : List.Vector ℕ n.succ) ↦ v.get 0 : List.Vector ℕ n.succ →. ℕ) v
⊢ ∃ (c : Code),
    ∀ (v : List.Vector ℕ n_2),
      c.eval (↑v : List ℕ) = pure <$> (↑fun (v : List.Vector ℕ n_2) ↦ v.get i : List.Vector ℕ n_2 →. ℕ) v
have prim₁ : ∀ (n : ℕ) (i : Fin n)
  (IH :
    ∃ (c : Code),
      ∀ (v : List.Vector ℕ n),
        c.eval (↑v : List ℕ) = pure <$> (↑fun (v : List.Vector ℕ n) ↦ v.get i : List.Vector ℕ n →. ℕ) v),
  ∃ (c : Code),
    ∀ (v : List.Vector ℕ n.succ),
      c.eval (↑v : List ℕ) = pure <$> (↑fun (v : List.Vector ℕ n.succ) ↦ v.get i.succ : List.Vector ℕ n.succ →. ℕ) v
Tactic: refine Fin.succRec (fun n => ?_) (fun n i IH => ?_) i
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
n_1 : ℕ
f : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f_1 : List.Vector ℕ n_2 → ℕ
n_3 : ℕ
i : Fin n_3
n : ℕ
x : List.Vector ℕ n.succ
a : ℕ
as : List ℕ
property : (a :: as).length = n.succ
⊢ head.eval (↑(Subtype.mk (p := fun (l : List ℕ) ↦ l.length = n.succ) (a :: as) property) : List ℕ) =
    pure <$>
      (↑fun (v : List.Vector ℕ n.succ) ↦ v.get 0 : List.Vector ℕ n.succ →. ℕ)
        (Subtype.mk (p := fun (l : List ℕ) ↦ l.length = n.succ) (a :: as) property)
have simp : Part.some [a] =
  pure <$>
    Part.some (List.Vector.head (n := n) (Subtype.mk (p := fun (l : List ℕ) ↦ l.length = n + 1) (a :: as) property))
Tactic: simp
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
n_1 : ℕ
f : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f_1 : List.Vector ℕ n_2 → ℕ
n_3 : ℕ
i_1 : Fin n_3
n : ℕ
i : Fin n
IH :
  ∃ (c : Code),
    ∀ (v : List.Vector ℕ n),
      c.eval (↑v : List ℕ) = pure <$> (↑fun (v : List.Vector ℕ n) ↦ v.get i : List.Vector ℕ n →. ℕ) v
⊢ ∃ (c : Code),
    ∀ (v : List.Vector ℕ n.succ),
      c.eval (↑v : List ℕ) = pure <$> (↑fun (v : List.Vector ℕ n.succ) ↦ v.get i.succ : List.Vector ℕ n.succ →. ℕ) v
have prim : ∀ (c : Code)
  (h :
    ∀ (v : List.Vector ℕ n),
      c.eval (↑v : List ℕ) = pure <$> (↑fun (v : List.Vector ℕ n) ↦ v.get i : List.Vector ℕ n →. ℕ) v),
  ∃ (c : Code),
    ∀ (v : List.Vector ℕ n.succ),
      c.eval (↑v : List ℕ) = pure <$> (↑fun (v : List.Vector ℕ n.succ) ↦ v.get i.succ : List.Vector ℕ n.succ →. ℕ) v
Tactic: obtain ⟨c, h⟩ := IH
Cleared hypotheses: IH
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f_2 : List.Vector ℕ n_2 → ℕ
n : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ (n + 2) → ℕ
h : Nat.Primrec' f
h_1 : Nat.Primrec' g
IHf : ∃ (c : Code), ∀ (v : List.Vector ℕ n), c.eval (↑v : List ℕ) = pure <$> (↑f : List.Vector ℕ n →. ℕ) v
IHg : ∃ (c : Code), ∀ (v : List.Vector ℕ (n + 2)), c.eval (↑v : List ℕ) = pure <$> (↑g : List.Vector ℕ (n + 2) →. ℕ) v
⊢ ∃ (c : Code),
    ∀ (v : List.Vector ℕ (n + 1)),
      c.eval (↑v : List ℕ) =
        pure <$>
          (↑fun (v : List.Vector ℕ (n + 1)) ↦
                Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) v.head :
              List.Vector ℕ (n + 1) →. ℕ)
            v
have prim : ∀ (cf : Code) (hf : ∀ (v : List.Vector ℕ n), cf.eval (↑v : List ℕ) = pure <$> (↑f : List.Vector ℕ n →. ℕ) v),
  ∃ (c : Code),
    ∀ (v : List.Vector ℕ (n + 1)),
      c.eval (↑v : List ℕ) =
        pure <$>
          (↑fun (v : List.Vector ℕ (n + 1)) ↦
                Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) v.head :
              List.Vector ℕ (n + 1) →. ℕ)
            v
Tactic: obtain ⟨cf, hf⟩ := IHf
Cleared hypotheses: IHf
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f_2 : List.Vector ℕ n_2 → ℕ
n : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ (n + 2) → ℕ
h : Nat.Primrec' f
h_1 : Nat.Primrec' g
IHg : ∃ (c : Code), ∀ (v : List.Vector ℕ (n + 2)), c.eval (↑v : List ℕ) = pure <$> (↑g : List.Vector ℕ (n + 2) →. ℕ) v
cf : Code
hf : ∀ (v : List.Vector ℕ n), cf.eval (↑v : List ℕ) = pure <$> (↑f : List.Vector ℕ n →. ℕ) v
⊢ ∃ (c : Code),
    ∀ (v : List.Vector ℕ (n + 1)),
      c.eval (↑v : List ℕ) =
        pure <$>
          (↑fun (v : List.Vector ℕ (n + 1)) ↦
                Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) v.head :
              List.Vector ℕ (n + 1) →. ℕ)
            v
have prim : ∀ (cg : Code)
  (hg : ∀ (v : List.Vector ℕ (n + 2)), cg.eval (↑v : List ℕ) = pure <$> (↑g : List.Vector ℕ (n + 2) →. ℕ) v),
  ∃ (c : Code),
    ∀ (v : List.Vector ℕ (n + 1)),
      c.eval (↑v : List ℕ) =
        pure <$>
          (↑fun (v : List.Vector ℕ (n + 1)) ↦
                Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) v.head :
              List.Vector ℕ (n + 1) →. ℕ)
            v
Tactic: obtain ⟨cg, hg⟩ := IHg
Cleared hypotheses: IHg
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (hypothesis)
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f_2 : List.Vector ℕ n_2 → ℕ
n : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ (n + 2) → ℕ
h : Nat.Primrec' f
h_1 : Nat.Primrec' g
cf : Code
hf : ∀ (v : List.Vector ℕ n), cf.eval (↑v : List ℕ) = pure <$> (↑f : List.Vector ℕ n →. ℕ) v
cg : Code
hg : ∀ (v : List.Vector ℕ (n + 2)), cg.eval (↑v : List ℕ) = pure <$> (↑g : List.Vector ℕ (n + 2) →. ℕ) v
⊢ ∃ (c : Code),
    ∀ (v : List.Vector ℕ (n + 1)),
      c.eval (↑v : List ℕ) =
        pure <$>
          (↑fun (v : List.Vector ℕ (n + 1)) ↦
                Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) v.head :
              List.Vector ℕ (n + 1) →. ℕ)
            v
have hf₁ : ∀ (v : List.Vector ℕ n), cf.eval (↑v : List ℕ) = Part.some (pure (f v))
Tactic: simp only [Part.map_eq_map, Part.map_some, PFun.coe_val] at hf hg
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (hypothesis)
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f_2 : List.Vector ℕ n_2 → ℕ
n : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ (n + 2) → ℕ
h : Nat.Primrec' f
h_1 : Nat.Primrec' g
cf : Code
hf : ∀ (v : List.Vector ℕ n), cf.eval (↑v : List ℕ) = pure <$> (↑f : List.Vector ℕ n →. ℕ) v
cg : Code
hg : ∀ (v : List.Vector ℕ (n + 2)), cg.eval (↑v : List ℕ) = pure <$> (↑g : List.Vector ℕ (n + 2) →. ℕ) v
hf₁ : ∀ (v : List.Vector ℕ n), cf.eval (↑v : List ℕ) = Part.some (pure (f v))
⊢ ∃ (c : Code),
    ∀ (v : List.Vector ℕ (n + 1)),
      c.eval (↑v : List ℕ) =
        pure <$>
          (↑fun (v : List.Vector ℕ (n + 1)) ↦
                Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) v.head :
              List.Vector ℕ (n + 1) →. ℕ)
            v
have hg₁ : ∀ (v : List.Vector ℕ (n + 2)), cg.eval (↑v : List ℕ) = Part.some (pure (g v))
Tactic: simp only [Part.map_eq_map, Part.map_some, PFun.coe_val] at hf hg
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f_2 : List.Vector ℕ n_2 → ℕ
n : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ (n + 2) → ℕ
h : Nat.Primrec' f
h_1 : Nat.Primrec' g
cf cg : Code
hf : ∀ (v : List.Vector ℕ n), cf.eval (↑v : List ℕ) = Part.some (pure (f v))
hg : ∀ (v : List.Vector ℕ (n + 2)), cg.eval (↑v : List ℕ) = Part.some (pure (g v))
⊢ ∃ (c : Code),
    ∀ (v : List.Vector ℕ (n + 1)),
      c.eval (↑v : List ℕ) =
        pure <$>
          (↑fun (v : List.Vector ℕ (n + 1)) ↦
                Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) v.head :
              List.Vector ℕ (n + 1) →. ℕ)
            v
have prim : ∀ (v : List.Vector ℕ (n + 1)),
  (cf.prec cg).eval (↑v : List ℕ) =
    pure <$>
      (↑fun (v : List.Vector ℕ (n + 1)) ↦
            Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) v.head :
          List.Vector ℕ (n + 1) →. ℕ)
        v
Tactic: refine ⟨prec cf cg, fun v => ?_⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f_2 : List.Vector ℕ n_2 → ℕ
n : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ (n + 2) → ℕ
h : Nat.Primrec' f
h_1 : Nat.Primrec' g
cf cg : Code
hf : ∀ (v : List.Vector ℕ n), cf.eval (↑v : List ℕ) = Part.some (pure (f v))
hg : ∀ (v : List.Vector ℕ (n + 2)), cg.eval (↑v : List ℕ) = Part.some (pure (g v))
v : List.Vector ℕ (n + 1)
⊢ (cf.prec cg).eval (↑v : List ℕ) =
    pure <$>
      (↑fun (v : List.Vector ℕ (n + 1)) ↦
            Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) v.head :
          List.Vector ℕ (n + 1) →. ℕ)
        v
have prim : (cf.prec cg).eval (↑(v.head ::ᵥ v.tail) : List ℕ) =
  pure <$>
    (↑fun (v : List.Vector ℕ (n + 1)) ↦
          Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) v.head :
        List.Vector ℕ (n + 1) →. ℕ)
      (v.head ::ᵥ v.tail)
Tactic: rw [← v.cons_head_tail]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (hypothesis)
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f_2 : List.Vector ℕ n_2 → ℕ
n : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ (n + 2) → ℕ
h : Nat.Primrec' f
h_1 : Nat.Primrec' g
cf cg : Code
hf : ∀ (v : List.Vector ℕ n), cf.eval (↑v : List ℕ) = Part.some (pure (f v))
hg : ∀ (v : List.Vector ℕ (n + 2)), cg.eval (↑v : List ℕ) = Part.some (pure (g v))
v : List.Vector ℕ (n + 1)
⊢ (cf.prec cg).eval (↑(v.head ::ᵥ v.tail) : List ℕ) =
    pure <$>
      (↑fun (v : List.Vector ℕ (n + 1)) ↦
            Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) v.head :
          List.Vector ℕ (n + 1) →. ℕ)
        (v.head ::ᵥ v.tail)
have hf₁ : cf.eval (↑v.tail : List ℕ) = Part.some (pure (f v.tail))
Tactic: specialize hf v.tail
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (hypothesis)
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f_2 : List.Vector ℕ n_2 → ℕ
n : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ (n + 2) → ℕ
h : Nat.Primrec' f
h_1 : Nat.Primrec' g
cf cg : Code
hg : ∀ (v : List.Vector ℕ (n + 2)), cg.eval (↑v : List ℕ) = Part.some (pure (g v))
v : List.Vector ℕ (n + 1)
hf : cf.eval (↑v.tail : List ℕ) = Part.some (pure (f v.tail))
⊢ (cf.prec cg).eval (↑(v.head ::ᵥ v.tail) : List ℕ) =
    pure <$>
      (↑fun (v : List.Vector ℕ (n + 1)) ↦
            Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) v.head :
          List.Vector ℕ (n + 1) →. ℕ)
        (v.head ::ᵥ v.tail)
have hg₁ : ∀ (a b : ℕ), cg.eval (↑(a ::ᵥ b ::ᵥ v.tail) : List ℕ) = Part.some (pure (g (a ::ᵥ b ::ᵥ v.tail)))
Tactic: replace hg := fun a b => hg (a ::ᵥ b ::ᵥ v.tail)
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (hypothesis)
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f_2 : List.Vector ℕ n_2 → ℕ
n : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ (n + 2) → ℕ
h : Nat.Primrec' f
h_1 : Nat.Primrec' g
cf cg : Code
v : List.Vector ℕ (n + 1)
hf : cf.eval (↑v.tail : List ℕ) = Part.some (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (↑(a ::ᵥ b ::ᵥ v.tail) : List ℕ) = Part.some (pure (g (a ::ᵥ b ::ᵥ v.tail)))
⊢ (cf.prec cg).eval (↑(v.head ::ᵥ v.tail) : List ℕ) =
    pure <$>
      (↑fun (v : List.Vector ℕ (n + 1)) ↦
            Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) v.head :
          List.Vector ℕ (n + 1) →. ℕ)
        (v.head ::ᵥ v.tail)
have hf₁ : cf.eval (↑v : List ℕ).tail = Part.some (pure (f v.tail))
Tactic: simp only [Vector.cons_val, Vector.tail_val] at hf hg
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (hypothesis)
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f_2 : List.Vector ℕ n_2 → ℕ
n : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ (n + 2) → ℕ
h : Nat.Primrec' f
h_1 : Nat.Primrec' g
cf cg : Code
v : List.Vector ℕ (n + 1)
hf : cf.eval (↑v.tail : List ℕ) = Part.some (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (↑(a ::ᵥ b ::ᵥ v.tail) : List ℕ) = Part.some (pure (g (a ::ᵥ b ::ᵥ v.tail)))
hf₁ : cf.eval (↑v : List ℕ).tail = Part.some (pure (f v.tail))
⊢ (cf.prec cg).eval (↑(v.head ::ᵥ v.tail) : List ℕ) =
    pure <$>
      (↑fun (v : List.Vector ℕ (n + 1)) ↦
            Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) v.head :
          List.Vector ℕ (n + 1) →. ℕ)
        (v.head ::ᵥ v.tail)
have hg₁ : ∀ (a b : ℕ), cg.eval (a :: b :: (↑v : List ℕ).tail) = Part.some (pure (g (a ::ᵥ b ::ᵥ v.tail)))
Tactic: simp only [Vector.cons_val, Vector.tail_val] at hf hg
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f_2 : List.Vector ℕ n_2 → ℕ
n : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ (n + 2) → ℕ
h : Nat.Primrec' f
h_1 : Nat.Primrec' g
cf cg : Code
v : List.Vector ℕ (n + 1)
hf : cf.eval (↑v : List ℕ).tail = Part.some (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (a :: b :: (↑v : List ℕ).tail) = Part.some (pure (g (a ::ᵥ b ::ᵥ v.tail)))
⊢ (cf.prec cg).eval (↑(v.head ::ᵥ v.tail) : List ℕ) =
    pure <$>
      (↑fun (v : List.Vector ℕ (n + 1)) ↦
            Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) v.head :
          List.Vector ℕ (n + 1) →. ℕ)
        (v.head ::ᵥ v.tail)
have prim : (cf.prec cg).eval (v.head :: (↑v : List ℕ).tail) =
  Part.some (pure (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) v.head))
Tactic: simp only [Part.map_eq_map, Part.map_some, Vector.cons_val, Vector.tail_cons,
        Vector.head_cons, PFun.coe_val, Vector.tail_val]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f_2 : List.Vector ℕ n_2 → ℕ
n_3 : ℕ
f : List.Vector ℕ n_3 → ℕ
g : List.Vector ℕ (n_3 + 2) → ℕ
h : Nat.Primrec' f
h_1 : Nat.Primrec' g
cf cg : Code
v : List.Vector ℕ (n_3 + 1)
hf : cf.eval (↑v : List ℕ).tail = pure (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (a :: b :: (↑v : List ℕ).tail) = pure (pure (g (a ::ᵥ b ::ᵥ v.tail)))
n : ℕ
h_2 :
  (cf.prec cg).eval (n :: (↑v : List ℕ).tail) =
    pure (pure (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n))
⊢ (cf.prec cg).eval ((n + 1) :: (↑v : List ℕ).tail) =
    pure (pure (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) (n + 1)))
have prim : (Part.bind
    (PFun.fix
      (fun (v : List ℕ) ↦
        (cg.eval (v.headI :: v.tail.tail)).bind fun (x : List ℕ) ↦
          Part.some
            (if v.tail.headI = 0 then Sum.inl ((v.headI + 1) :: (v.tail.headI - 1) :: x.headI :: v.tail.tail.tail)
            else Sum.inr ((v.headI + 1) :: (v.tail.headI - 1) :: x.headI :: v.tail.tail.tail)))
      (0 :: n :: f v.tail :: (↑v : List ℕ).tail))
    fun (x : List ℕ) ↦ Part.some [x.tail.tail.headI]) =
  Part.some
    [g (n ::ᵥ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ v.tail)]
Tactic: simp [prec, hf, Part.bind_assoc, ← Part.bind_some_eq_map, Part.bind_some, Bind.bind]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (hypothesis)
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f_2 : List.Vector ℕ n_2 → ℕ
n_3 : ℕ
f : List.Vector ℕ n_3 → ℕ
g : List.Vector ℕ (n_3 + 2) → ℕ
h : Nat.Primrec' f
h_1 : Nat.Primrec' g
cf cg : Code
v : List.Vector ℕ (n_3 + 1)
hf : cf.eval (↑v : List ℕ).tail = pure (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (a :: b :: (↑v : List ℕ).tail) = pure (pure (g (a ::ᵥ b ::ᵥ v.tail)))
n : ℕ
h_2 :
  (cf.prec cg).eval (n :: (↑v : List ℕ).tail) =
    pure (pure (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n))
this :
  ∀ (a b : ℕ),
    a + b = n →
      Membership.mem (γ := Part (List ℕ))
        (PFun.fix
          (fun (v : List ℕ) ↦
            (cg.eval (v.headI :: v.tail.tail)).bind fun (x : List ℕ) ↦
              Part.some
                (if v.tail.headI = 0 then Sum.inl (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)
                else Sum.inr (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)))
          (a ::
            b ::
              Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a ::
                (↑v : List ℕ).tail))
        (n.succ ::
          0 ::
            g
                (n ::ᵥ
                  Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ
                    v.tail) ::
              (↑v : List ℕ).tail)
⊢ (Part.bind
      (PFun.fix
        (fun (v : List ℕ) ↦
          (cg.eval (v.headI :: v.tail.tail)).bind fun (x : List ℕ) ↦
            Part.some
              (if v.tail.headI = 0 then Sum.inl ((v.headI + 1) :: (v.tail.headI - 1) :: x.headI :: v.tail.tail.tail)
              else Sum.inr ((v.headI + 1) :: (v.tail.headI - 1) :: x.headI :: v.tail.tail.tail)))
        (0 :: n :: f v.tail :: (↑v : List ℕ).tail))
      fun (x : List ℕ) ↦ Part.some [x.tail.tail.headI]) =
    Part.some
      [g (n ::ᵥ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ v.tail)]
have this₁ : PFun.fix
    (fun (v : List ℕ) ↦
      (cg.eval (v.headI :: v.tail.tail)).bind fun (x : List ℕ) ↦
        Part.some
          (if v.tail.headI = 0 then Sum.inl (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)
          else Sum.inr (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)))
    (0 ::
      n ::
        Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) 0 ::
          (↑v : List ℕ).tail) =
  Part.some
    (n.succ ::
      0 ::
        g
            (n ::ᵥ
              Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ v.tail) ::
          (↑v : List ℕ).tail)
Tactic: have := Part.eq_some_iff.mpr (this _ _ (zero_add _))