awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
a : PosNum
⊢ ∀ (l₁ : List Γ'),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum a) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
            (elim (trPosNum a.succ ++ Γ'.cons :: trList v) l₁ c d))
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q₂)) s' (elim (l₂' ++ Γ'.cons :: trList v) l₁' c d))
have cons : ∀ (s : Option Γ') (l₁ : List Γ'),
  ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
    l₁.reverseAux (trPosNum PosNum.one) = l₁'.reverseAux l₂' ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
          (elim (trPosNum PosNum.one.succ ++ Γ'.cons :: trList v) l₁ c d))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q₂)) s' (elim (l₂' ++ Γ'.cons :: trList v) l₁' c d))
Tactic: induction a generalizing s with intro l₁
  | one =>
    refine ⟨Γ'.bit1::l₁, [], some Γ'.cons, rfl, TransGen.head rfl (TransGen.single ?_)⟩
    simp [trPosNum, show PosNum.one.succ = PosNum.one.bit0 from rfl]
  | bit1 m IH =>
    obtain ⟨l₁', l₂', s', e, h⟩ := IH (some Γ'.bit0) (Γ'.bit1 :: l₁)
    refine ⟨l₁', l₂', s', e, TransGen.head ?_ h⟩
    simp
    rfl
  | bit0 m IH =>
    obtain ⟨a, l, e, h⟩ : ∃ a l, (trPosNum m = a::l) ∧ natEnd a = false := by
      cases m <;> refine ⟨_, _, rfl, rfl⟩
    refine ⟨Γ'.bit0 :: l₁, _, some a, rfl, TransGen.single ?_⟩
    simp [trPosNum, PosNum.succ, e, h, show some Γ'.bit1 ≠ some Γ'.bit0 by decide,
      Option.getD, -natEnd]
    rfl
Cleared hypotheses: s, a
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
a : PosNum
cons cons₁ :
  ∀ (s : Option Γ') (l₁ : List Γ'),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum PosNum.one) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
            (elim (trPosNum PosNum.one.succ ++ Γ'.cons :: trList v) l₁ c d))
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q₂)) s' (elim (l₂' ++ Γ'.cons :: trList v) l₁' c d))
⊢ ∀ (l₁ : List Γ'),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum a) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
            (elim (trPosNum a.succ ++ Γ'.cons :: trList v) l₁ c d))
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q₂)) s' (elim (l₂' ++ Γ'.cons :: trList v) l₁' c d))
have cons₂ : ∀ (m : PosNum)
  (IH :
    ∀ (s : Option Γ') (l₁ : List Γ'),
      ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
        l₁.reverseAux (trPosNum m) = l₁'.reverseAux l₂' ∧
          Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
            (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
              (elim (trPosNum m.succ ++ Γ'.cons :: trList v) l₁ c d))
            (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q₂)) s' (elim (l₂' ++ Γ'.cons :: trList v) l₁' c d)))
  (s : Option Γ') (l₁ : List Γ'),
  ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
    l₁.reverseAux (trPosNum m.bit1) = l₁'.reverseAux l₂' ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
          (elim (trPosNum m.bit1.succ ++ Γ'.cons :: trList v) l₁ c d))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q₂)) s' (elim (l₂' ++ Γ'.cons :: trList v) l₁' c d))
Tactic: induction a generalizing s with intro l₁
  | one =>
    refine ⟨Γ'.bit1::l₁, [], some Γ'.cons, rfl, TransGen.head rfl (TransGen.single ?_)⟩
    simp [trPosNum, show PosNum.one.succ = PosNum.one.bit0 from rfl]
  | bit1 m IH =>
    obtain ⟨l₁', l₂', s', e, h⟩ := IH (some Γ'.bit0) (Γ'.bit1 :: l₁)
    refine ⟨l₁', l₂', s', e, TransGen.head ?_ h⟩
    simp
    rfl
  | bit0 m IH =>
    obtain ⟨a, l, e, h⟩ : ∃ a l, (trPosNum m = a::l) ∧ natEnd a = false := by
      cases m <;> refine ⟨_, _, rfl, rfl⟩
    refine ⟨Γ'.bit0 :: l₁, _, some a, rfl, TransGen.single ?_⟩
    simp [trPosNum, PosNum.succ, e, h, show some Γ'.bit1 ≠ some Γ'.bit0 by decide,
      Option.getD, -natEnd]
    rfl
Cleared hypotheses: s, a
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
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₂
have zero' : TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont k))) s (elim (trList (0 :: v)) [] [] (trContStack k)) ∈
  TM2.step (Γ := fun (x : K') ↦ Γ') tr
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal Code.zero' (trCont k))) s
      (elim (trList v) [] [] (trContStack k)))
Tactic: refine ⟨_, ⟨s, rfl⟩, TransGen.single ?_⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
k : Cont
v : List ℕ
s : Option Γ'
o : Option Γ' := List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') v none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons
⊢ ∃ (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₂
have tail : 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)))
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont k))) o (elim (trList v.tail) [] [] (trContStack k)))
Tactic: refine ⟨_, ⟨o, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
k : Cont
v : List ℕ
s : Option Γ'
o : Option Γ' := List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') v none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons
⊢ 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)))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont k))) o (elim (trList v.tail) [] [] (trContStack k)))
have h : elim (trList v.tail) [] [] (trContStack k) =
  update (β := fun (k : K') ↦ List Γ') (elim (trList v) [] [] (trContStack k)) main (trList v.tail)
Tactic: convert! clear_ok _ using 2
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
k : Cont
v : List ℕ
s : Option Γ'
o : Option Γ' := List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') v none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons
h :
  elim (trList v.tail) [] [] (trContStack k) =
    update (β := fun (k : K') ↦ List Γ') (elim (trList v) [] [] (trContStack k)) main (trList v.tail)
⊢ 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)))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont k))) o (elim (trList v.tail) [] [] (trContStack k)))
have tail : List Γ'
Tactic: convert! clear_ok _ using 2
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
k : Cont
v : List ℕ
s : Option Γ'
o : Option Γ' := List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') v none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons
h :
  elim (trList v.tail) [] [] (trContStack k) =
    update (β := fun (k : K') ↦ List Γ') (elim (trList v) [] [] (trContStack k)) main (trList v.tail)
tail tail₁ : List Γ'
⊢ 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)))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont k))) o (elim (trList v.tail) [] [] (trContStack k)))
have tail₂ : splitAtPred natEnd (elim (trList v) [] [] (trContStack k) main) = (trNat v.headI, o, trList v.tail)
Tactic: convert! clear_ok _ using 2
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
k : Cont
v : List ℕ
s : Option Γ'
o : Option Γ' := List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') v none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons
⊢ elim (trList v.tail) [] [] (trContStack k) =
    update (β := fun (k : K') ↦ List Γ') (elim (trList v) [] [] (trContStack k)) main (trList v.tail)
have h : elim (trList v.tail) [] [] (trContStack k) = elim (trList v.tail) [] [] (trContStack k)
Tactic: simp
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
k : Cont
v : List ℕ
s : Option Γ'
o : Option Γ' := List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') v none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons
⊢ Option.elim' (elim (trList v) [] [] (trContStack k) main = trNat v.headI ∧ trList v.tail = [])
    (fun (a : Γ') ↦ natEnd a = true ∧ elim (trList v) [] [] (trContStack k) main = trNat v.headI ++ a :: trList v.tail)
    o
have tail : let o : Option Γ' :=
  List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') [] none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons;
Option.elim' (elim (trList []) [] [] (trContStack k) main = trNat (List.headI []) ∧ trList (List.tail []) = [])
  (fun (a : Γ') ↦
    natEnd a = true ∧ elim (trList []) [] [] (trContStack k) main = trNat (List.headI []) ++ a :: trList (List.tail []))
  o
Tactic: cases v
Cleared hypotheses: v, o
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
k : Cont
v : List ℕ
s : Option Γ'
o : Option Γ' := List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') v none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons
tail :
  let o : Option Γ' :=
    List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') [] none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons;
  Option.elim' (elim (trList []) [] [] (trContStack k) main = trNat (List.headI []) ∧ trList (List.tail []) = [])
    (fun (a : Γ') ↦
      natEnd a = true ∧
        elim (trList []) [] [] (trContStack k) main = trNat (List.headI []) ++ a :: trList (List.tail []))
    o
⊢ Option.elim' (elim (trList v) [] [] (trContStack k) main = trNat v.headI ∧ trList v.tail = [])
    (fun (a : Γ') ↦ natEnd a = true ∧ elim (trList v) [] [] (trContStack k) main = trNat v.headI ++ a :: trList v.tail)
    o
have tail₁ : ∀ (head : ℕ) (tail : List ℕ),
  let o : Option Γ' :=
    List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') (head :: tail) none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons;
  Option.elim'
    (elim (trList (head :: tail)) [] [] (trContStack k) main = trNat (head :: tail).headI ∧
      trList (head :: tail).tail = [])
    (fun (a : Γ') ↦
      natEnd a = true ∧
        elim (trList (head :: tail)) [] [] (trContStack k) main =
          trNat (head :: tail).headI ++ a :: trList (head :: tail).tail)
    o
Tactic: cases v
Cleared hypotheses: v, o
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
f fs : 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₂
a_ih :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal fs k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal fs (trCont k))) s
            (elim (trList v) [] [] (trContStack k)))
          b₂
k : Cont
v : List ℕ
s : Option Γ'
⊢ ∃ (b₂ : Cfg'),
    TrCfg (stepNormal (f.cons fs) k v) b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal (f.cons fs) (trCont k))) s
          (elim (trList v) [] [] (trContStack k)))
        b₂
have cons : ∀ (c : Cfg') (h₁ : TrCfg (stepNormal f (Cont.cons₁ fs v k) v) c)
  (h₂ :
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont (Cont.cons₁ fs v k)))) none
        (elim (trList v) [] [] (trContStack (Cont.cons₁ fs v k))))
      c),
  ∃ (b₂ : Cfg'),
    TrCfg (stepNormal (f.cons fs) k v) b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal (f.cons fs) (trCont k))) s
          (elim (trList v) [] [] (trContStack k)))
        b₂
Tactic: obtain ⟨c, h₁, h₂⟩ := IHf (Cont.cons₁ fs v k) v none
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
f fs : 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₂
a_ih :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal fs k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal fs (trCont k))) s
            (elim (trList v) [] [] (trContStack k)))
          b₂
k : Cont
v : List ℕ
s : Option Γ'
c : Cfg'
h₁ : TrCfg (stepNormal f (Cont.cons₁ fs v k) v) c
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont (Cont.cons₁ fs v k)))) none
      (elim (trList v) [] [] (trContStack (Cont.cons₁ fs v k))))
    c
⊢ ∃ (b₂ : Cfg'),
    TrCfg (stepNormal (f.cons fs) k v) b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal (f.cons fs) (trCont k))) s
          (elim (trList v) [] [] (trContStack k)))
        b₂
have cons : TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (Cont'.cons₁ fs (trCont k))).copy) none
    (update (β := fun (k : K') ↦ List Γ')
      (update (β := fun (a : K') ↦ List Γ')
        (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trList v) [] [] (trContStack k)) stack
          ((fun (s : Option Γ') ↦ (Option.getD ((fun (x : Option Γ') ↦ some Γ'.consₗ) s) default : Γ')) s ::
            elim (trList v) [] [] (trContStack k) stack))
        main [])
      rev
      ((update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trList v) [] [] (trContStack k)) stack
            ((fun (s : Option Γ') ↦ (Option.getD ((fun (x : Option Γ') ↦ some Γ'.consₗ) s) default : Γ')) s ::
              elim (trList v) [] [] (trContStack k) stack)
            main).reverseAux
        (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trList v) [] [] (trContStack k)) stack
          ((fun (s : Option Γ') ↦ (Option.getD ((fun (x : Option Γ') ↦ some Γ'.consₗ) s) default : Γ')) s ::
            elim (trList v) [] [] (trContStack k) stack)
          rev))))
  c
Tactic: refine ⟨c, h₁, TransGen.head rfl <| (move_ok (by decide) (splitAtPred_false _)).trans ?_⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
f fs : 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₂
a_ih :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal fs k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal fs (trCont k))) s
            (elim (trList v) [] [] (trContStack k)))
          b₂
k : Cont
v : List ℕ
s : Option Γ'
c : Cfg'
h₁ : TrCfg (stepNormal f (Cont.cons₁ fs v k) v) c
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont (Cont.cons₁ fs v k)))) none
      (elim (trList v) [] [] (trContStack (Cont.cons₁ fs v k))))
    c
⊢ TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (Cont'.cons₁ fs (trCont k))).copy) none
      (update (β := fun (k : K') ↦ List Γ')
        (update (β := fun (a : K') ↦ List Γ')
          (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trList v) [] [] (trContStack k)) stack
            ((fun (s : Option Γ') ↦ (Option.getD ((fun (x : Option Γ') ↦ some Γ'.consₗ) s) default : Γ')) s ::
              elim (trList v) [] [] (trContStack k) stack))
          main [])
        rev
        ((update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trList v) [] [] (trContStack k)) stack
              ((fun (s : Option Γ') ↦ (Option.getD ((fun (x : Option Γ') ↦ some Γ'.consₗ) s) default : Γ')) s ::
                elim (trList v) [] [] (trContStack k) stack)
              main).reverseAux
          (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trList v) [] [] (trContStack k)) stack
            ((fun (s : Option Γ') ↦ (Option.getD ((fun (x : Option Γ') ↦ some Γ'.consₗ) s) default : Γ')) s ::
              elim (trList v) [] [] (trContStack k) stack)
            rev))))
    c
have cons : TransGen
  (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
    (match (motive := TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ') → Option (TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')))
        a with
      | { l := none, var := var, stk := stk } => none
      | { l := some l, var := v, stk := S } => some (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr l) v S)) =
      some b)
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (Cont'.cons₁ fs (trCont k))).copy) none
    (elim [] ((trList v).reverseAux []) [] ((some Γ'.consₗ).getD default :: trContStack k)))
  c
Tactic: simp only [TM2.step, Option.mem_def, elim_stack, elim_update_stack, elim_update_main,
      elim_main, elim_rev, elim_update_rev]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
f fs : 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₂
a_ih :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal fs k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal fs (trCont k))) s
            (elim (trList v) [] [] (trContStack k)))
          b₂
k : Cont
v : List ℕ
s : Option Γ'
c : Cfg'
h₁ : TrCfg (stepNormal f (Cont.cons₁ fs v k) v) c
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont (Cont.cons₁ fs v k)))) none
      (elim (trList v) [] [] (trContStack (Cont.cons₁ fs v k))))
    c
⊢ TransGen
    (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
      (match (motive :=
          TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ') → Option (TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))) a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr l) v S)) =
        some b)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (Cont'.cons₁ fs (trCont k))).copy) none
      (elim [] ((trList v).reverseAux []) [] ((some Γ'.consₗ).getD default :: trContStack k)))
    c
have cons : TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (Cont'.cons₁ fs (trCont k)))) none
    (elim ((trList v).reverse.reverseAux []) [] []
      ((trList v).reverse.reverseAux ((some Γ'.consₗ).getD default :: trContStack k))))
  c
Tactic: refine (copy_ok _ none [] (trList v).reverse _ _).trans ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
f fs : 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₂
a_ih :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal fs k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal fs (trCont k))) s
            (elim (trList v) [] [] (trContStack k)))
          b₂
k : Cont
v : List ℕ
s : Option Γ'
c : Cfg'
h₁ : TrCfg (stepNormal f (Cont.cons₁ fs v k) v) c
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont (Cont.cons₁ fs v k)))) none
      (elim (trList v) [] [] (trContStack (Cont.cons₁ fs v k))))
    c
⊢ TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (Cont'.cons₁ fs (trCont k)))) none
      (elim ((trList v).reverse.reverseAux []) [] []
        ((trList v).reverse.reverseAux ((some Γ'.consₗ).getD default :: trContStack k))))
    c
have h : elim ((trList v).reverse.reverseAux []) [] []
    ((trList v).reverse.reverseAux ((some Γ'.consₗ).getD default :: trContStack k)) =
  elim (trList v) [] [] (trContStack (Cont.cons₁ fs v k))
Tactic: convert! h₂ using 2
-- 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 (stepNormal (f.case g) k v) 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 : ∃ (b₂ : Cfg'),
  TrCfg
      ((fun (k : Cont) (v : List ℕ) ↦
          (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
              (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) v.headI :
            Cfg))
        k v)
      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: rw [stepNormal]