awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
⊢ (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 prim : ∀ (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)
Tactic: suffices ∀ a b, a + b = n →
        (n.succ :: 0 ::
          g (n ::ᵥ Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ v.tail) ::
              v.val.tail : List ℕ) ∈
          PFun.fix
            (fun v : List ℕ => Part.bind (cg.eval (v.headI :: v.tail.tail))
              (fun x => Part.some (if v.tail.headI = 0
                then Sum.inl
                  (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail : List ℕ)
                else Sum.inr
                  (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail))))
            (a :: b :: Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a :: v.val.tail) by
        have := Part.eq_some_iff.mpr (this _ _ (zero_add _))
        simp_all
-- 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))
b : ℕ
IH :
  ∀ (a : ℕ) (e : 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)
a : ℕ
e : a + (b + 1) = n
⊢ a + 1 + b = n
have rwa : a + b + 1 = n
Tactic: rwa [add_right_comm]
-- 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))
a b : ℕ
e : 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)
have prim : ∀ (a : ℕ) (e : a + 0 = 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 ::
        0 ::
          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)
Tactic: induction b generalizing a with
      | zero =>
        refine PFun.mem_fix_iff.2 (Or.inl <| Part.eq_some_iff.1 ?_)
        simp only [hg, ← e, Part.bind_some, List.tail_cons, pure]
        rfl
      | succ b IH =>
        refine PFun.mem_fix_iff.2 (Or.inr ⟨_, ?_, IH (a + 1) (by rwa [add_right_comm])⟩)
        simp only [hg, Part.bind_some, List.tail_cons, pure]
        exact Part.mem_some_iff.2 rfl
Cleared hypotheses: a, b, e
-- 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 = pure (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (a :: b :: (↑v : List ℕ).tail) = pure (pure (g (a ::ᵥ b ::ᵥ v.tail)))
⊢ (cf.prec cg).eval (v.head :: (↑v : List ℕ).tail) =
    pure (pure (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) v.head))
have prim : ∀ (x : ℕ),
  (cf.prec cg).eval (x :: (↑v : List ℕ).tail) =
    pure (pure (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) x))
Tactic: induction v.head with
        simp [prec, hf, Part.bind_assoc, ← Part.bind_some_eq_map, Part.bind_some, Bind.bind]
      | succ n _ =>
      suffices ∀ a b, a + b = n →
        (n.succ :: 0 ::
          g (n ::ᵥ Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ v.tail) ::
              v.val.tail : List ℕ) ∈
          PFun.fix
            (fun v : List ℕ => Part.bind (cg.eval (v.headI :: v.tail.tail))
              (fun x => Part.some (if v.tail.headI = 0
                then Sum.inl
                  (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail : List ℕ)
                else Sum.inr
                  (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail))))
            (a :: b :: Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a :: v.val.tail) by
        have := Part.eq_some_iff.mpr (this _ _ (zero_add _))
        simp_all
      intro a b e
      induction b generalizing a with
      | zero =>
        refine PFun.mem_fix_iff.2 (Or.inl <| Part.eq_some_iff.1 ?_)
        simp only [hg, ← e, Part.bind_some, List.tail_cons, pure]
        rfl
      | succ b IH =>
        refine PFun.mem_fix_iff.2 (Or.inr ⟨_, ?_, IH (a + 1) (by rwa [add_right_comm])⟩)
        simp only [hg, Part.bind_some, List.tail_cons, pure]
        exact Part.mem_some_iff.2 rfl
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
n : ℕ
f : List.Vector ℕ n →. ℕ
n_1 : ℕ
f_1 : List.Vector ℕ n_1 → ℕ
hf : Nat.Primrec' f_1
⊢ ∃ (c : Code), ∀ (v : List.Vector ℕ n_1), c.eval (↑v : List ℕ) = pure <$> (↑f_1 : List.Vector ℕ n_1 →. ℕ) v
have prim : ∃ (c : Code),
  ∀ (v : List.Vector ℕ 0), c.eval (↑v : List ℕ) = pure <$> (↑fun (x : List.Vector ℕ 0) ↦ 0 : List.Vector ℕ 0 →. ℕ) v
Tactic: induction hf with
    | zero => exact ⟨zero', fun ⟨[], _⟩ => rfl⟩
    | succ => exact ⟨succ, fun ⟨[v], _⟩ => rfl⟩
    | get i =>
      refine Fin.succRec (fun n => ?_) (fun n i IH => ?_) i
      · exact ⟨head, fun ⟨List.cons a as, _⟩ => by simp; rfl⟩
      · obtain ⟨c, h⟩ := IH
        exact ⟨c.comp tail, fun v => by simpa [← Vector.get_tail, Bind.bind] using h v.tail⟩
    | comp g hf hg IHf IHg =>
      simpa [Part.bind_eq_bind] using exists_code.comp IHf IHg
    | @prec n f g _ _ IHf IHg =>
      obtain ⟨cf, hf⟩ := IHf
      obtain ⟨cg, hg⟩ := IHg
      simp only [Part.map_eq_map, Part.map_some, PFun.coe_val] at hf hg
      refine ⟨prec cf cg, fun v => ?_⟩
      rw [← v.cons_head_tail]
      specialize hf v.tail
      replace hg := fun a b => hg (a ::ᵥ b ::ᵥ v.tail)
      simp only [Vector.cons_val, Vector.tail_val] at hf hg
      simp only [Part.map_eq_map, Part.map_some, Vector.cons_val, Vector.tail_cons,
        Vector.head_cons, PFun.coe_val, Vector.tail_val]
      simp only [← Part.pure_eq_some] at hf hg ⊢
      induction v.head with
        simp [prec, hf, Part.bind_assoc, ← Part.bind_some_eq_map, Part.bind_some, Bind.bind]
      | succ n _ =>
      suffices ∀ a b, a + b = n →
        (n.succ :: 0 ::
          g (n ::ᵥ Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ v.tail) ::
              v.val.tail : List ℕ) ∈
          PFun.fix
            (fun v : List ℕ => Part.bind (cg.eval (v.headI :: v.tail.tail))
              (fun x => Part.some (if v.tail.headI = 0
                then Sum.inl
                  (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail : List ℕ)
                else Sum.inr
                  (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail))))
            (a :: b :: Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a :: v.val.tail) by
        have := Part.eq_some_iff.mpr (this _ _ (zero_add _))
        simp_all
      intro a b e
      induction b generalizing a with
      | zero =>
        refine PFun.mem_fix_iff.2 (Or.inl <| Part.eq_some_iff.1 ?_)
        simp only [hg, ← e, Part.bind_some, List.tail_cons, pure]
        rfl
      | succ b IH =>
        refine PFun.mem_fix_iff.2 (Or.inr ⟨_, ?_, IH (a + 1) (by rwa [add_right_comm])⟩)
        simp only [hg, Part.bind_some, List.tail_cons, pure]
        exact Part.mem_some_iff.2 rfl
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
n : ℕ
f : List.Vector ℕ n →. ℕ
n_1 : ℕ
f_1 : List.Vector ℕ n_1 → ℕ
hf : Nat.Primrec' f_1
prim :
  ∃ (c : Code),
    ∀ (v : List.Vector ℕ 0), c.eval (↑v : List ℕ) = pure <$> (↑fun (x : List.Vector ℕ 0) ↦ 0 : List.Vector ℕ 0 →. ℕ) v
⊢ ∃ (c : Code), ∀ (v : List.Vector ℕ n_1), c.eval (↑v : List ℕ) = pure <$> (↑f_1 : List.Vector ℕ n_1 →. ℕ) v
have prim₁ : ∃ (c : Code),
  ∀ (v : List.Vector ℕ 1),
    c.eval (↑v : List ℕ) = pure <$> (↑fun (v : List.Vector ℕ 1) ↦ v.head.succ : List.Vector ℕ 1 →. ℕ) v
Tactic: induction hf with
    | zero => exact ⟨zero', fun ⟨[], _⟩ => rfl⟩
    | succ => exact ⟨succ, fun ⟨[v], _⟩ => rfl⟩
    | get i =>
      refine Fin.succRec (fun n => ?_) (fun n i IH => ?_) i
      · exact ⟨head, fun ⟨List.cons a as, _⟩ => by simp; rfl⟩
      · obtain ⟨c, h⟩ := IH
        exact ⟨c.comp tail, fun v => by simpa [← Vector.get_tail, Bind.bind] using h v.tail⟩
    | comp g hf hg IHf IHg =>
      simpa [Part.bind_eq_bind] using exists_code.comp IHf IHg
    | @prec n f g _ _ IHf IHg =>
      obtain ⟨cf, hf⟩ := IHf
      obtain ⟨cg, hg⟩ := IHg
      simp only [Part.map_eq_map, Part.map_some, PFun.coe_val] at hf hg
      refine ⟨prec cf cg, fun v => ?_⟩
      rw [← v.cons_head_tail]
      specialize hf v.tail
      replace hg := fun a b => hg (a ::ᵥ b ::ᵥ v.tail)
      simp only [Vector.cons_val, Vector.tail_val] at hf hg
      simp only [Part.map_eq_map, Part.map_some, Vector.cons_val, Vector.tail_cons,
        Vector.head_cons, PFun.coe_val, Vector.tail_val]
      simp only [← Part.pure_eq_some] at hf hg ⊢
      induction v.head with
        simp [prec, hf, Part.bind_assoc, ← Part.bind_some_eq_map, Part.bind_some, Bind.bind]
      | succ n _ =>
      suffices ∀ a b, a + b = n →
        (n.succ :: 0 ::
          g (n ::ᵥ Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ v.tail) ::
              v.val.tail : List ℕ) ∈
          PFun.fix
            (fun v : List ℕ => Part.bind (cg.eval (v.headI :: v.tail.tail))
              (fun x => Part.some (if v.tail.headI = 0
                then Sum.inl
                  (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail : List ℕ)
                else Sum.inr
                  (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail))))
            (a :: b :: Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a :: v.val.tail) by
        have := Part.eq_some_iff.mpr (this _ _ (zero_add _))
        simp_all
      intro a b e
      induction b generalizing a with
      | zero =>
        refine PFun.mem_fix_iff.2 (Or.inl <| Part.eq_some_iff.1 ?_)
        simp only [hg, ← e, Part.bind_some, List.tail_cons, pure]
        rfl
      | succ b IH =>
        refine PFun.mem_fix_iff.2 (Or.inr ⟨_, ?_, IH (a + 1) (by rwa [add_right_comm])⟩)
        simp only [hg, Part.bind_some, List.tail_cons, pure]
        exact Part.mem_some_iff.2 rfl
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
n : ℕ
f : List.Vector ℕ n →. ℕ
n_1 : ℕ
f_1 : List.Vector ℕ n_1 → ℕ
hf : Nat.Primrec' f_1
prim :
  ∃ (c : Code),
    ∀ (v : List.Vector ℕ 0), c.eval (↑v : List ℕ) = pure <$> (↑fun (x : List.Vector ℕ 0) ↦ 0 : List.Vector ℕ 0 →. ℕ) v
prim₁ :
  ∃ (c : Code),
    ∀ (v : List.Vector ℕ 1),
      c.eval (↑v : List ℕ) = pure <$> (↑fun (v : List.Vector ℕ 1) ↦ v.head.succ : List.Vector ℕ 1 →. ℕ) v
⊢ ∃ (c : Code), ∀ (v : List.Vector ℕ n_1), c.eval (↑v : List ℕ) = pure <$> (↑f_1 : List.Vector ℕ n_1 →. ℕ) v
have prim₂ : ∀ {n : ℕ} (i : Fin n),
  ∃ (c : Code),
    ∀ (v : List.Vector ℕ n),
      c.eval (↑v : List ℕ) = pure <$> (↑fun (v : List.Vector ℕ n) ↦ v.get i : List.Vector ℕ n →. ℕ) v
Tactic: induction hf with
    | zero => exact ⟨zero', fun ⟨[], _⟩ => rfl⟩
    | succ => exact ⟨succ, fun ⟨[v], _⟩ => rfl⟩
    | get i =>
      refine Fin.succRec (fun n => ?_) (fun n i IH => ?_) i
      · exact ⟨head, fun ⟨List.cons a as, _⟩ => by simp; rfl⟩
      · obtain ⟨c, h⟩ := IH
        exact ⟨c.comp tail, fun v => by simpa [← Vector.get_tail, Bind.bind] using h v.tail⟩
    | comp g hf hg IHf IHg =>
      simpa [Part.bind_eq_bind] using exists_code.comp IHf IHg
    | @prec n f g _ _ IHf IHg =>
      obtain ⟨cf, hf⟩ := IHf
      obtain ⟨cg, hg⟩ := IHg
      simp only [Part.map_eq_map, Part.map_some, PFun.coe_val] at hf hg
      refine ⟨prec cf cg, fun v => ?_⟩
      rw [← v.cons_head_tail]
      specialize hf v.tail
      replace hg := fun a b => hg (a ::ᵥ b ::ᵥ v.tail)
      simp only [Vector.cons_val, Vector.tail_val] at hf hg
      simp only [Part.map_eq_map, Part.map_some, Vector.cons_val, Vector.tail_cons,
        Vector.head_cons, PFun.coe_val, Vector.tail_val]
      simp only [← Part.pure_eq_some] at hf hg ⊢
      induction v.head with
        simp [prec, hf, Part.bind_assoc, ← Part.bind_some_eq_map, Part.bind_some, Bind.bind]
      | succ n _ =>
      suffices ∀ a b, a + b = n →
        (n.succ :: 0 ::
          g (n ::ᵥ Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ v.tail) ::
              v.val.tail : List ℕ) ∈
          PFun.fix
            (fun v : List ℕ => Part.bind (cg.eval (v.headI :: v.tail.tail))
              (fun x => Part.some (if v.tail.headI = 0
                then Sum.inl
                  (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail : List ℕ)
                else Sum.inr
                  (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail))))
            (a :: b :: Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a :: v.val.tail) by
        have := Part.eq_some_iff.mpr (this _ _ (zero_add _))
        simp_all
      intro a b e
      induction b generalizing a with
      | zero =>
        refine PFun.mem_fix_iff.2 (Or.inl <| Part.eq_some_iff.1 ?_)
        simp only [hg, ← e, Part.bind_some, List.tail_cons, pure]
        rfl
      | succ b IH =>
        refine PFun.mem_fix_iff.2 (Or.inr ⟨_, ?_, IH (a + 1) (by rwa [add_right_comm])⟩)
        simp only [hg, Part.bind_some, List.tail_cons, pure]
        exact Part.mem_some_iff.2 rfl
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
h : Nat.Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ)
IHf : ∃ (c : Code), ∀ (v : List.Vector ℕ (n + 1)), c.eval (↑v : List ℕ) = pure <$> (↑f : List.Vector ℕ (n + 1) →. ℕ) v
⊢ ∃ (c : Code),
    ∀ (v : List.Vector ℕ n),
      c.eval (↑v : List ℕ) =
        pure <$> (fun (v : List.Vector ℕ n) ↦ Nat.rfind fun (n_2 : ℕ) ↦ Part.some (decide (f (n_2 ::ᵥ v) = 0))) v
have rfind : ∀ (cf : Code)
  (hf : ∀ (v : List.Vector ℕ (n + 1)), cf.eval (↑v : List ℕ) = pure <$> (↑f : List.Vector ℕ (n + 1) →. ℕ) v),
  ∃ (c : Code),
    ∀ (v : List.Vector ℕ n),
      c.eval (↑v : List ℕ) =
        pure <$> (fun (v : List.Vector ℕ n) ↦ Nat.rfind fun (n_2 : ℕ) ↦ Part.some (decide (f (n_2 ::ᵥ v) = 0))) 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 : ℕ
f : List.Vector ℕ (n + 1) → ℕ
h : Nat.Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ)
cf : Code
hf : ∀ (v : List.Vector ℕ (n + 1)), cf.eval (↑v : List ℕ) = pure <$> (↑f : List.Vector ℕ (n + 1) →. ℕ) v
⊢ ∃ (c : Code),
    ∀ (v : List.Vector ℕ n),
      c.eval (↑v : List ℕ) =
        pure <$> (fun (v : List.Vector ℕ n) ↦ Nat.rfind fun (n_2 : ℕ) ↦ Part.some (decide (f (n_2 ::ᵥ v) = 0))) v
have rfind : ∀ (v : List.Vector ℕ n),
  cf.rfind.eval (↑v : List ℕ) =
    pure <$> (fun (v : List.Vector ℕ n) ↦ Nat.rfind fun (n_2 : ℕ) ↦ Part.some (decide (f (n_2 ::ᵥ v) = 0))) v
Tactic: refine ⟨rfind cf, fun v => ?_⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (hypothesis)
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
h : Nat.Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ)
cf : Code
hf : ∀ (v : List.Vector ℕ (n + 1)), cf.eval (↑v : List ℕ) = pure <$> (↑f : List.Vector ℕ (n + 1) →. ℕ) v
v : List.Vector ℕ n
⊢ cf.rfind.eval (↑v : List ℕ) =
    pure <$> (fun (v : List.Vector ℕ n) ↦ Nat.rfind fun (n_2 : ℕ) ↦ Part.some (decide (f (n_2 ::ᵥ v) = 0))) v
have hf₁ : ∀ (a : ℕ), cf.eval (↑(a ::ᵥ v) : List ℕ) = pure <$> (↑f : List.Vector ℕ (n + 1) →. ℕ) (a ::ᵥ v)
Tactic: replace hf := fun a => hf (a ::ᵥ v)
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (hypothesis)
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
h : Nat.Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ)
cf : Code
v : List.Vector ℕ n
hf : ∀ (a : ℕ), cf.eval (↑(a ::ᵥ v) : List ℕ) = pure <$> (↑f : List.Vector ℕ (n + 1) →. ℕ) (a ::ᵥ v)
⊢ cf.rfind.eval (↑v : List ℕ) =
    pure <$> (fun (v : List.Vector ℕ n) ↦ Nat.rfind fun (n_2 : ℕ) ↦ Part.some (decide (f (n_2 ::ᵥ v) = 0))) v
have hf₁ : ∀ (a : ℕ), cf.eval (a :: (↑v : List ℕ)) = Part.some [f (a ::ᵥ v)]
Tactic: simp only [Part.map_eq_map, Part.map_some, Vector.cons_val, PFun.coe_val,
      show ∀ x, pure x = [x] from fun _ => rfl] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
h : Nat.Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ)
cf : Code
v : List.Vector ℕ n
hf : ∀ (a : ℕ), cf.eval (a :: (↑v : List ℕ)) = Part.some [f (a ::ᵥ v)]
⊢ cf.rfind.eval (↑v : List ℕ) = Part.map pure (Nat.rfind fun (n_2 : ℕ) ↦ Part.some (decide (f (n_2 ::ᵥ v) = 0)))
have rfind : ∀ (x : List ℕ),
  x ∈ cf.rfind.eval (↑v : List ℕ) ↔
    Membership.mem (γ := Part (List ℕ))
      (Part.map pure (Nat.rfind fun (n_2 : ℕ) ↦ Part.some (decide (f (n_2 ::ᵥ v) = 0)))) x
Tactic: refine Part.ext fun x => ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
h : Nat.Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ)
cf : Code
v : List.Vector ℕ n
hf : ∀ (a : ℕ), cf.eval (a :: (↑v : List ℕ)) = Part.some [f (a ::ᵥ v)]
x : List ℕ
⊢ x ∈ cf.rfind.eval (↑v : List ℕ) ↔
    Membership.mem (γ := Part (List ℕ))
      (Part.map pure (Nat.rfind fun (n_2 : ℕ) ↦ Part.some (decide (f (n_2 ::ᵥ v) = 0)))) x
have rfind : (∃ (a : List ℕ),
    Membership.mem (γ := Part (List ℕ))
        (PFun.fix
          (fun (v : List ℕ) ↦
            (cf.eval v).bind fun (y : List ℕ) ↦
              Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
          (0 :: (↑v : List ℕ)))
        a ∧
      x = [a.headI.pred]) ↔
  ∃ (a : ℕ), (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ pure a = x
Tactic: simp only [rfind, Part.bind_eq_bind, Part.pure_eq_some, Part.bind_some,
      cons_eval, comp_eval, fix_eval, tail_eval, succ_eval, zero'_eval,
      List.headI_cons, pred_eval, Part.map_some, false_eq_decide_iff,
      Part.mem_bind_iff, Part.mem_map_iff, Nat.mem_rfind,
      List.tail_cons, true_eq_decide_iff, Part.mem_some_iff, Part.map_bind]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
h : Nat.Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ)
cf : Code
v : List.Vector ℕ n
hf : ∀ (a : ℕ), cf.eval (a :: (↑v : List ℕ)) = Part.some [f (a ::ᵥ v)]
x : List ℕ
⊢ (∃ (a : List ℕ),
      Membership.mem (γ := Part (List ℕ))
          (PFun.fix
            (fun (v : List ℕ) ↦
              (cf.eval v).bind fun (y : List ℕ) ↦
                Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
            (0 :: (↑v : List ℕ)))
          a ∧
        x = [a.headI.pred]) ↔
    ∃ (a : ℕ), (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ pure a = x
have rfind : (∃ (a : List ℕ),
    Membership.mem (γ := Part (List ℕ))
        (PFun.fix
          (fun (v : List ℕ) ↦
            (cf.eval v).bind fun (y : List ℕ) ↦
              Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
          (0 :: (↑v : List ℕ)))
        a ∧
      x = [a.headI.pred]) →
  ∃ (a : ℕ), (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ pure a = x
Tactic: constructor