awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
f g : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
IHg :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal g k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal g (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
k : Cont
v : List ℕ
s : Option Γ'
⊢ ∃ (b₂ : Cfg'),
    TrCfg
        (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
          (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) v.headI)
        b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal (f.case g) (trCont k))) s
          (elim (trList v) [] [] (trContStack k)))
        b₂
have case : ∀ (s' : Option Γ')
  (h :
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some ((trNormal f (trCont k)).pred (trNormal g (trCont k)))) s
        (elim (trList v) [] [] (trContStack k)))
      (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s'
          (elim (trList v.tail) [] [] (trContStack k)))
        (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
          TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal g (trCont k))) s'
            (elim (trList (n :: v.tail)) [] [] (trContStack k)))
        v.headI)),
  ∃ (b₂ : Cfg'),
    TrCfg
        (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
          (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) v.headI)
        b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal (f.case g) (trCont k))) s
          (elim (trList v) [] [] (trContStack k)))
        b₂
Tactic: obtain ⟨s', h⟩ := pred_ok _ _ s v _ _
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
f g : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
IHg :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal g k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal g (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
k : Cont
v : List ℕ
s s' : Option Γ'
h :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some ((trNormal f (trCont k)).pred (trNormal g (trCont k)))) s
      (elim (trList v) [] [] (trContStack k)))
    (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s'
        (elim (trList v.tail) [] [] (trContStack k)))
      (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
        TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal g (trCont k))) s'
          (elim (trList (n :: v.tail)) [] [] (trContStack k)))
      v.headI)
⊢ ∃ (b₂ : Cfg'),
    TrCfg
        (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
          (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) v.headI)
        b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal (f.case g) (trCont k))) s
          (elim (trList v) [] [] (trContStack k)))
        b₂
have case : ∀
  (h :
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some ((trNormal f (trCont k)).pred (trNormal g (trCont k)))) s
        (elim (trList v) [] [] (trContStack k)))
      (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s'
          (elim (trList v.tail) [] [] (trContStack k)))
        (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
          TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal g (trCont k))) s'
            (elim (trList (n :: v.tail)) [] [] (trContStack k)))
        v.headI)),
  ∃ (b₂ : Cfg'),
    TrCfg
        (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
          (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) v.headI)
        b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal (f.case g) (trCont k))) s
          (elim (trList v) [] [] (trContStack k)))
        b₂
Tactic: revert h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
f g : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
IHg :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal g k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal g (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
k : Cont
v : List ℕ
s s' : Option Γ'
⊢ ∀
    (h :
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some ((trNormal f (trCont k)).pred (trNormal g (trCont k)))) s
          (elim (trList v) [] [] (trContStack k)))
        (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s'
            (elim (trList v.tail) [] [] (trContStack k)))
          (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
            TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal g (trCont k))) s'
              (elim (trList (n :: v.tail)) [] [] (trContStack k)))
          v.headI)),
    ∃ (b₂ : Cfg'),
      TrCfg
          (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
            (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) v.headI)
          b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal (f.case g) (trCont k))) s
            (elim (trList v) [] [] (trContStack k)))
          b₂
have case : ∀
  (h :
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some ((trNormal f (trCont k)).pred (trNormal g (trCont k)))) s
        (elim (trList v) [] [] (trContStack k)))
      (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s'
          (elim (trList v.tail) [] [] (trContStack k)))
        (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
          TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal g (trCont k))) s'
            (elim (trList (n :: v.tail)) [] [] (trContStack k)))
        0)),
  ∃ (b₂ : Cfg'),
    TrCfg
        (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
          (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) 0)
        b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal (f.case g) (trCont k))) s
          (elim (trList v) [] [] (trContStack k)))
        b₂
Tactic: rcases v.headI with - | n
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
f g : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
IHg :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal g k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal g (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
k : Cont
v : List ℕ
s s' : Option Γ'
h :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some ((trNormal f (trCont k)).pred (trNormal g (trCont k)))) s
      (elim (trList v) [] [] (trContStack k)))
    (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s'
        (elim (trList v.tail) [] [] (trContStack k)))
      (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
        TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal g (trCont k))) s'
          (elim (trList (n :: v.tail)) [] [] (trContStack k)))
      0)
⊢ ∃ (b₂ : Cfg'),
    TrCfg
        (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
          (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) 0)
        b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal (f.case g) (trCont k))) s
          (elim (trList v) [] [] (trContStack k)))
        b₂
have case : ∀ (c : Cfg') (h₁ : TrCfg (stepNormal f k v.tail) c)
  (h₂ :
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s'
        (elim (trList v.tail) [] [] (trContStack k)))
      c),
  ∃ (b₂ : Cfg'),
    TrCfg
        (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
          (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) 0)
        b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal (f.case g) (trCont k))) s
          (elim (trList v) [] [] (trContStack k)))
        b₂
Tactic: obtain ⟨c, h₁, h₂⟩ := IHf k _ s'
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
f g : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
IHg :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal g k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal g (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
k : Cont
v : List ℕ
s s' : Option Γ'
n : ℕ
h :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some ((trNormal f (trCont k)).pred (trNormal g (trCont k)))) s
      (elim (trList v) [] [] (trContStack k)))
    (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s'
        (elim (trList v.tail) [] [] (trContStack k)))
      (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
        TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal g (trCont k))) s'
          (elim (trList (n :: v.tail)) [] [] (trContStack k)))
      (n + 1))
⊢ ∃ (b₂ : Cfg'),
    TrCfg
        (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
          (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) (n + 1))
        b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal (f.case g) (trCont k))) s
          (elim (trList v) [] [] (trContStack k)))
        b₂
have case : ∀ (c : Cfg') (h₁ : TrCfg (stepNormal g k (n :: v.tail)) c)
  (h₂ :
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal g (trCont k))) s'
        (elim (trList (n :: v.tail)) [] [] (trContStack k)))
      c),
  ∃ (b₂ : Cfg'),
    TrCfg
        (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
          (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) (n + 1))
        b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal (f.case g) (trCont k))) s
          (elim (trList v) [] [] (trContStack k)))
        b₂
Tactic: obtain ⟨c, h₁, h₂⟩ := IHg k _ s'
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
c : Code
k : Cont
v : List ℕ
s : Option Γ'
⊢ ∃ (b₂ : Cfg'),
    TrCfg (stepNormal c k v) b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal c (trCont k))) s (elim (trList v) [] [] (trContStack k)))
        b₂
have zero' : ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
  ∃ (b₂ : Cfg'),
    TrCfg (stepNormal Code.zero' k v) b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal Code.zero' (trCont k))) s
          (elim (trList v) [] [] (trContStack k)))
        b₂
Tactic: induction c generalizing k v s with
  | zero' => refine ⟨_, ⟨s, rfl⟩, TransGen.single ?_⟩; simp
  | succ => refine ⟨_, ⟨none, rfl⟩, head_main_ok.trans succ_ok⟩
  | tail =>
    let o : Option Γ' := List.casesOn v none fun _ _ => some Γ'.cons
    refine ⟨_, ⟨o, rfl⟩, ?_⟩; convert! clear_ok _ using 2
    · simp; rfl
    swap
    refine splitAtPred_eq _ _ (trNat v.headI) _ _ (trNat_natEnd _) ?_
    cases v <;> simp [o]
  | cons f fs IHf _ =>
    obtain ⟨c, h₁, h₂⟩ := IHf (Cont.cons₁ fs v k) v none
    refine ⟨c, h₁, TransGen.head rfl <| (move_ok (by decide) (splitAtPred_false _)).trans ?_⟩
    simp only [TM2.step, Option.mem_def, elim_stack, elim_update_stack, elim_update_main,
      elim_main, elim_rev, elim_update_rev]
    refine (copy_ok _ none [] (trList v).reverse _ _).trans ?_
    convert! h₂ using 2
    simp [List.reverseAux_eq, trContStack]
  | comp f _ _ IHg => exact IHg (Cont.comp f k) v s
  | case f g IHf IHg =>
    rw [stepNormal]
    simp only
    obtain ⟨s', h⟩ := pred_ok _ _ s v _ _
    revert h; rcases v.headI with - | n <;> intro h
    · obtain ⟨c, h₁, h₂⟩ := IHf k _ s'
      exact ⟨_, h₁, h.trans h₂⟩
    · obtain ⟨c, h₁, h₂⟩ := IHg k _ s'
      exact ⟨_, h₁, h.trans h₂⟩
  | fix f IH => apply IH
Cleared hypotheses: c, k, v, s
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
c : Code
k : Cont
v : List ℕ
s : Option Γ'
zero' :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal Code.zero' k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal Code.zero' (trCont k))) s
            (elim (trList v) [] [] (trContStack k)))
          b₂
⊢ ∃ (b₂ : Cfg'),
    TrCfg (stepNormal c k v) b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal c (trCont k))) s (elim (trList v) [] [] (trContStack k)))
        b₂
have succ : ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
  ∃ (b₂ : Cfg'),
    TrCfg (stepNormal Code.succ k v) b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal Code.succ (trCont k))) s
          (elim (trList v) [] [] (trContStack k)))
        b₂
Tactic: induction c generalizing k v s with
  | zero' => refine ⟨_, ⟨s, rfl⟩, TransGen.single ?_⟩; simp
  | succ => refine ⟨_, ⟨none, rfl⟩, head_main_ok.trans succ_ok⟩
  | tail =>
    let o : Option Γ' := List.casesOn v none fun _ _ => some Γ'.cons
    refine ⟨_, ⟨o, rfl⟩, ?_⟩; convert! clear_ok _ using 2
    · simp; rfl
    swap
    refine splitAtPred_eq _ _ (trNat v.headI) _ _ (trNat_natEnd _) ?_
    cases v <;> simp [o]
  | cons f fs IHf _ =>
    obtain ⟨c, h₁, h₂⟩ := IHf (Cont.cons₁ fs v k) v none
    refine ⟨c, h₁, TransGen.head rfl <| (move_ok (by decide) (splitAtPred_false _)).trans ?_⟩
    simp only [TM2.step, Option.mem_def, elim_stack, elim_update_stack, elim_update_main,
      elim_main, elim_rev, elim_update_rev]
    refine (copy_ok _ none [] (trList v).reverse _ _).trans ?_
    convert! h₂ using 2
    simp [List.reverseAux_eq, trContStack]
  | comp f _ _ IHg => exact IHg (Cont.comp f k) v s
  | case f g IHf IHg =>
    rw [stepNormal]
    simp only
    obtain ⟨s', h⟩ := pred_ok _ _ s v _ _
    revert h; rcases v.headI with - | n <;> intro h
    · obtain ⟨c, h₁, h₂⟩ := IHf k _ s'
      exact ⟨_, h₁, h.trans h₂⟩
    · obtain ⟨c, h₁, h₂⟩ := IHg k _ s'
      exact ⟨_, h₁, h.trans h₂⟩
  | fix f IH => apply IH
Cleared hypotheses: c, k, v, s
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
c : Code
k : Cont
v : List ℕ
s : Option Γ'
zero' :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal Code.zero' k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal Code.zero' (trCont k))) s
            (elim (trList v) [] [] (trContStack k)))
          b₂
succ :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal Code.succ k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal Code.succ (trCont k))) s
            (elim (trList v) [] [] (trContStack k)))
          b₂
⊢ ∃ (b₂ : Cfg'),
    TrCfg (stepNormal c k v) b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal c (trCont k))) s (elim (trList v) [] [] (trContStack k)))
        b₂
have tail : ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
  ∃ (b₂ : Cfg'),
    TrCfg (stepNormal Code.tail k v) b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal Code.tail (trCont k))) s
          (elim (trList v) [] [] (trContStack k)))
        b₂
Tactic: induction c generalizing k v s with
  | zero' => refine ⟨_, ⟨s, rfl⟩, TransGen.single ?_⟩; simp
  | succ => refine ⟨_, ⟨none, rfl⟩, head_main_ok.trans succ_ok⟩
  | tail =>
    let o : Option Γ' := List.casesOn v none fun _ _ => some Γ'.cons
    refine ⟨_, ⟨o, rfl⟩, ?_⟩; convert! clear_ok _ using 2
    · simp; rfl
    swap
    refine splitAtPred_eq _ _ (trNat v.headI) _ _ (trNat_natEnd _) ?_
    cases v <;> simp [o]
  | cons f fs IHf _ =>
    obtain ⟨c, h₁, h₂⟩ := IHf (Cont.cons₁ fs v k) v none
    refine ⟨c, h₁, TransGen.head rfl <| (move_ok (by decide) (splitAtPred_false _)).trans ?_⟩
    simp only [TM2.step, Option.mem_def, elim_stack, elim_update_stack, elim_update_main,
      elim_main, elim_rev, elim_update_rev]
    refine (copy_ok _ none [] (trList v).reverse _ _).trans ?_
    convert! h₂ using 2
    simp [List.reverseAux_eq, trContStack]
  | comp f _ _ IHg => exact IHg (Cont.comp f k) v s
  | case f g IHf IHg =>
    rw [stepNormal]
    simp only
    obtain ⟨s', h⟩ := pred_ok _ _ s v _ _
    revert h; rcases v.headI with - | n <;> intro h
    · obtain ⟨c, h₁, h₂⟩ := IHf k _ s'
      exact ⟨_, h₁, h.trans h₂⟩
    · obtain ⟨c, h₁, h₂⟩ := IHg k _ s'
      exact ⟨_, h₁, h.trans h₂⟩
  | fix f IH => apply IH
Cleared hypotheses: c, k, v, s
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
fs : Code
as : List ℕ
k : Cont
a_ih :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont k))) s (elim (trList v) [] [] (trContStack k))) b₂
v : List ℕ
s : Option Γ'
⊢ ∃ (b₂ : Cfg'),
    TrCfg (stepRet (Cont.cons₁ fs as k) v) b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont (Cont.cons₁ fs as k)))) s
          (elim (trList v) [] [] (trContStack (Cont.cons₁ fs as k))))
        b₂
have cons₁ : ∀ (s' : Cfg') (h₁ : TrCfg (stepNormal fs (Cont.cons₂ v k) as) s')
  (h₂ :
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal fs (trCont (Cont.cons₂ v k)))) none
        (elim (trList as) [] [] (trContStack (Cont.cons₂ v k))))
      s'),
  ∃ (b₂ : Cfg'),
    TrCfg (stepRet (Cont.cons₁ fs as k) v) b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont (Cont.cons₁ fs as k)))) s
          (elim (trList v) [] [] (trContStack (Cont.cons₁ fs as k))))
        b₂
Tactic: obtain ⟨s', h₁, h₂⟩ := trNormal_respects fs (Cont.cons₂ v k) as none
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
fs : Code
as : List ℕ
k : Cont
a_ih :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont k))) s (elim (trList v) [] [] (trContStack k))) b₂
v : List ℕ
s : Option Γ'
s' : Cfg'
h₁ : TrCfg (stepNormal fs (Cont.cons₂ v k) as) s'
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal fs (trCont (Cont.cons₂ v k)))) none
      (elim (trList as) [] [] (trContStack (Cont.cons₂ v k))))
    s'
⊢ ∃ (b₂ : Cfg'),
    TrCfg (stepRet (Cont.cons₁ fs as k) v) b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont (Cont.cons₁ fs as k)))) s
          (elim (trList v) [] [] (trContStack (Cont.cons₁ fs as k))))
        b₂
have cons₁ : TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
  (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr (Λ'.ret (trCont (Cont.cons₁ fs as k)))) s
    (elim (trList v) [] [] (trContStack (Cont.cons₁ fs as k))))
  s'
Tactic: refine ⟨s', h₁, TransGen.head rfl ?_⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
fs : Code
as : List ℕ
k : Cont
a_ih :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont k))) s (elim (trList v) [] [] (trContStack k))) b₂
v : List ℕ
s : Option Γ'
s' : Cfg'
h₁ : TrCfg (stepNormal fs (Cont.cons₂ v k) as) s'
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal fs (trCont (Cont.cons₂ v k)))) none
      (elim (trList as) [] [] (trContStack (Cont.cons₂ v k))))
    s'
⊢ TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ TM2.step (Γ := fun (x : K') ↦ Γ') tr a = some b)
    (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr (Λ'.ret (trCont (Cont.cons₁ fs as k)))) s
      (elim (trList v) [] [] (trContStack (Cont.cons₁ fs as k))))
    s'
have cons₁ : elim (trList v) [] [] (trContStack (Cont.cons₁ fs as k)) rev = []
Tactic: refine (move₂_ok (by decide) ?_ (splitAtPred_false _)).trans ?_