awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Code
k : Cont
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 Γ'
this :
  if v.headI = 0 then natEnd ((trList v).head?.getD default) = true ∧ (trList v).tail = trList v.tail
  else
    natEnd ((trList v).head?.getD default) = false ∧ (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail
h : v.headI = 0
pos :
  ∀ (this : natEnd ((trList v).head?.getD default) = true ∧ (trList v).tail = trList v.tail),
    ∃ (b₂ : Cfg'),
      TrCfg (stepRet k v.tail) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont (Cont.fix f k)))) s
            (elim (trList v) [] [] (trContStack (Cont.fix f k))))
          b₂
⊢ ∃ (b₂ : Cfg'),
    TrCfg (if v.headI = 0 then stepRet k v.tail else stepNormal f (Cont.fix f k) v.tail) b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont (Cont.fix f k)))) s
          (elim (trList v) [] [] (trContStack (Cont.fix f k))))
        b₂

Tactic:
simp only [h, ite_true, ite_false] at this ⊢

Premises used: ite_false, ite_true
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Code
k : Cont
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 Γ'
this :
  if v.headI = 0 then natEnd ((trList v).head?.getD default) = true ∧ (trList v).tail = trList v.tail
  else
    natEnd ((trList v).head?.getD default) = false ∧ (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail
h : ¬v.headI = 0
neg :
  ∀
    (this :
      natEnd ((trList v).head?.getD default) = false ∧
        (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal f (Cont.fix f k) v.tail) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont (Cont.fix f k)))) s
            (elim (trList v) [] [] (trContStack (Cont.fix f k))))
          b₂
⊢ ∃ (b₂ : Cfg'),
    TrCfg (if v.headI = 0 then stepRet k v.tail else stepNormal f (Cont.fix f k) v.tail) b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont (Cont.fix f k)))) s
          (elim (trList v) [] [] (trContStack (Cont.fix f k))))
        b₂

Tactic:
simp only [h, ite_true, ite_false] at this ⊢

Premises used: ite_false, ite_true
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Code
k : Cont
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 Γ'
h : v.headI = 0
this : natEnd ((trList v).head?.getD default) = true ∧ (trList v).tail = trList v.tail
pos :
  ∀ (c : Cfg') (h₁ : TrCfg (stepRet k v.tail) c)
    (h₂ :
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont k))) (trList v).head?
          (elim (trList v.tail) [] [] (trContStack k)))
        c),
    ∃ (b₂ : Cfg'),
      TrCfg (stepRet k v.tail) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont (Cont.fix f k)))) s
            (elim (trList v) [] [] (trContStack (Cont.fix f k))))
          b₂
⊢ ∃ (b₂ : Cfg'),
    TrCfg (stepRet k v.tail) b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont (Cont.fix f k)))) s
          (elim (trList v) [] [] (trContStack (Cont.fix f k))))
        b₂

Tactic:
obtain ⟨c, h₁, h₂⟩ := IH v.tail (trList v).head?

Premises used: List.head?, Turing.PartrecToTM2.trList, List.tail
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Code
k : Cont
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 Γ'
h : v.headI = 0
this : natEnd ((trList v).head?.getD default) = true ∧ (trList v).tail = trList v.tail
c : Cfg'
h₁ : TrCfg (stepRet k v.tail) c
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont k))) (trList v).head?
      (elim (trList v.tail) [] [] (trContStack k)))
    c
⊢ ∃ (b₂ : Cfg'),
    TrCfg (stepRet k v.tail) b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont (Cont.fix f k)))) s
          (elim (trList v) [] [] (trContStack (Cont.fix f k))))
        b₂

Tactic:
⟨c, h₁, TransGen.head rfl ?_⟩

Premises used: Relation.TransGen.head, And.intro, Exists.intro, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Code
k : Cont
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 Γ'
h : v.headI = 0
this : natEnd ((trList v).head?.getD default) = true ∧ (trList v).tail = trList v.tail
c : Cfg'
h₁ : TrCfg (stepRet k v.tail) c
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont k))) (trList v).head?
      (elim (trList v.tail) [] [] (trContStack k)))
    c
pos :
  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.fix f k)))) s
      (elim (trList v) [] [] (trContStack (Cont.fix f k))))
    c
⊢ ∃ (b₂ : Cfg'),
    TrCfg (stepRet k v.tail) b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont (Cont.fix f k)))) s
          (elim (trList v) [] [] (trContStack (Cont.fix f k))))
        b₂

Tactic:
refine ⟨c, h₁, TransGen.head rfl ?_⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Code
k : Cont
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 Γ'
h : v.headI = 0
this : natEnd ((trList v).head?.getD default) = true ∧ (trList v).tail = trList v.tail
c : Cfg'
h₁ : TrCfg (stepRet k v.tail) c
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont k))) (trList v).head?
      (elim (trList v.tail) [] [] (trContStack k)))
    c
pos :
  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 (bif true then Λ'.ret (trCont k) else Λ'.clear natEnd main (trNormal f (Cont'.fix f (trCont k)))))
      (trList v).head? (elim (trList v.tail) [] [] (trContStack (Cont.fix f k))))
    c
⊢ TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
    (TM2.stepAux (Γ := fun (x : K') ↦ Γ')
      (pop' main
        (goto (Γ := fun (x : K') ↦ Γ') fun (s : Option Γ') ↦
          bif natEnd (s.getD default) then Λ'.ret (trCont k)
          else Λ'.clear natEnd main (trNormal f (Cont'.fix f (trCont k)))))
      s (elim (trList v) [] [] (trContStack (Cont.fix f k))))
    c

Tactic:
simp only [pop', TM2.stepAux, elim_main, this, elim_update_main]

Premises used: Turing.TM2.stepAux, Turing.PartrecToTM2.K'.elim_update_main, Turing.PartrecToTM2.K'.elim_main, Turing.PartrecToTM2.pop'
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Code
k : Cont
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 Γ'
h : v.headI = 0
this : natEnd ((trList v).head?.getD default) = true ∧ (trList v).tail = trList v.tail
c : Cfg'
h₁ : TrCfg (stepRet k v.tail) c
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont k))) (trList v).head?
      (elim (trList v.tail) [] [] (trContStack 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 (bif true then Λ'.ret (trCont k) else Λ'.clear natEnd main (trNormal f (Cont'.fix f (trCont k)))))
      (trList v).head? (elim (trList v.tail) [] [] (trContStack (Cont.fix f k))))
    c

Tactic:
h₂

Premises used: cond, Turing.PartrecToTM2.trContStack, Turing.PartrecToTM2.contStack, StateTransition.Reaches₁
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Code
k : Cont
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 Γ'
h : v.headI = 0
this : natEnd ((trList v).head?.getD default) = true ∧ (trList v).tail = trList v.tail
c : Cfg'
h₁ : TrCfg (stepRet k v.tail) c
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont k))) (trList v).head?
      (elim (trList v.tail) [] [] (trContStack 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 (bif true then Λ'.ret (trCont k) else Λ'.clear natEnd main (trNormal f (Cont'.fix f (trCont k)))))
      (trList v).head? (elim (trList v.tail) [] [] (trContStack (Cont.fix f k))))
    c

Tactic:
exact h₂
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Code
k : Cont
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 Γ'
h : ¬v.headI = 0
this :
  natEnd ((trList v).head?.getD default) = false ∧ (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail
neg :
  ∀ (s' : Cfg') (h₁ : TrCfg (stepNormal f (Cont.fix f k) v.tail) s')
    (h₂ :
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont (Cont.fix f k)))) (some Γ'.cons)
          (elim (trList v.tail) [] [] (trContStack (Cont.fix f k))))
        s'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal f (Cont.fix f k) v.tail) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont (Cont.fix f k)))) s
            (elim (trList v) [] [] (trContStack (Cont.fix f k))))
          b₂
⊢ ∃ (b₂ : Cfg'),
    TrCfg (stepNormal f (Cont.fix f k) v.tail) b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont (Cont.fix f k)))) s
          (elim (trList v) [] [] (trContStack (Cont.fix f k))))
        b₂

Tactic:
obtain ⟨s', h₁, h₂⟩ := trNormal_respects f (Cont.fix f k) v.tail (some Γ'.cons)

Premises used: Turing.PartrecToTM2.Γ'.cons, Option.some, Turing.ToPartrec.Cont.fix, List.tail, Turing.PartrecToTM2.trNormal_respects
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Code
k : Cont
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 Γ'
h : ¬v.headI = 0
this :
  natEnd ((trList v).head?.getD default) = false ∧ (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail
s' : Cfg'
h₁ : TrCfg (stepNormal f (Cont.fix f k) v.tail) s'
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont (Cont.fix f k)))) (some Γ'.cons)
      (elim (trList v.tail) [] [] (trContStack (Cont.fix f k))))
    s'
⊢ ∃ (b₂ : Cfg'),
    TrCfg (stepNormal f (Cont.fix f k) v.tail) b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont (Cont.fix f k)))) s
          (elim (trList v) [] [] (trContStack (Cont.fix f k))))
        b₂

Tactic:
⟨_, h₁, TransGen.head rfl <| TransGen.trans ?_ h₂⟩

Premises used: Relation.TransGen.head, Relation.TransGen.trans, And.intro, Exists.intro, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Code
k : Cont
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 Γ'
h : ¬v.headI = 0
this :
  natEnd ((trList v).head?.getD default) = false ∧ (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail
s' : Cfg'
h₁ : TrCfg (stepNormal f (Cont.fix f k) v.tail) s'
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont (Cont.fix f k)))) (some Γ'.cons)
      (elim (trList v.tail) [] [] (trContStack (Cont.fix f k))))
    s'
neg :
  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.fix f k)))) s
      (elim (trList v) [] [] (trContStack (Cont.fix f k))))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont (Cont.fix f k)))) (some Γ'.cons)
      (elim (trList v.tail) [] [] (trContStack (Cont.fix f k))))
⊢ ∃ (b₂ : Cfg'),
    TrCfg (stepNormal f (Cont.fix f k) v.tail) b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont (Cont.fix f k)))) s
          (elim (trList v) [] [] (trContStack (Cont.fix f k))))
        b₂

Tactic:
refine ⟨_, h₁, TransGen.head rfl <| TransGen.trans ?_ h₂⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Code
k : Cont
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 Γ'
h : ¬v.headI = 0
this :
  natEnd ((trList v).head?.getD default) = false ∧ (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail
s' : Cfg'
h₁ : TrCfg (stepNormal f (Cont.fix f k) v.tail) s'
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont (Cont.fix f k)))) (some Γ'.cons)
      (elim (trList v.tail) [] [] (trContStack (Cont.fix f k))))
    s'
neg :
  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 (bif false then Λ'.ret (trCont k) else Λ'.clear natEnd main (trNormal f (Cont'.fix f (trCont k)))))
      (trList v).head?
      (update (β := fun (k : K') ↦ List Γ') (elim (trList v) [] [] (trContStack (Cont.fix f k))) main (trList v).tail))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (Cont'.fix f (trCont k)))) (some Γ'.cons)
      (elim (trList v.tail) [] [] (trContStack (Cont.fix f k))))
⊢ TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
    (TM2.stepAux (Γ := fun (x : K') ↦ Γ')
      (pop' main
        (goto (Γ := fun (x : K') ↦ Γ') fun (s : Option Γ') ↦
          bif natEnd (s.getD default) then Λ'.ret (trCont k)
          else Λ'.clear natEnd main (trNormal f (Cont'.fix f (trCont k)))))
      s (elim (trList v) [] [] (trContStack (Cont.fix f k))))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (Cont'.fix f (trCont k)))) (some Γ'.cons)
      (elim (trList v.tail) [] [] (trContStack (Cont.fix f k))))

Tactic:
simp only [pop', TM2.stepAux, elim_main, this.1]

Premises used: Turing.TM2.stepAux, Turing.PartrecToTM2.K'.elim_main, Turing.PartrecToTM2.pop', And.left
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Code
k : Cont
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 Γ'
h : ¬v.headI = 0
this :
  natEnd ((trList v).head?.getD default) = false ∧ (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail
s' : Cfg'
h₁ : TrCfg (stepNormal f (Cont.fix f k) v.tail) s'
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont (Cont.fix f k)))) (some Γ'.cons)
      (elim (trList v.tail) [] [] (trContStack (Cont.fix f k))))
    s'
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear natEnd main (trNormal f (Cont'.fix f (trCont k)))))
      (trList v).head?
      (update (β := fun (k : K') ↦ List Γ') (elim (trList v) [] [] (trContStack (Cont.fix f k))) main (trList v).tail))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (Cont'.fix f (trCont k)))) (some Γ'.cons)
      (update (β := fun (k : K') ↦ List Γ')
        (update (β := fun (k : K') ↦ List Γ') (elim (trList v) [] [] (trContStack (Cont.fix f k))) main (trList v).tail)
        main (trList v.tail)))

Tactic:
clear_ok (splitAtPred_eq _ _ (trNat v.headI).tail (some Γ'.cons) _ _ _)

Premises used: Turing.PartrecToTM2.Γ'.cons, Option.some, List.tail, Turing.PartrecToTM2.splitAtPred_eq, Turing.PartrecToTM2.clear_ok, List.headI, Turing.PartrecToTM2.trNat
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Code
k : Cont
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 Γ'
h : ¬v.headI = 0
this :
  natEnd ((trList v).head?.getD default) = false ∧ (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail
s' : Cfg'
h₁ : TrCfg (stepNormal f (Cont.fix f k) v.tail) s'
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont (Cont.fix f k)))) (some Γ'.cons)
      (elim (trList v.tail) [] [] (trContStack (Cont.fix f k))))
    s'
h₃ :
  elim (trList v.tail) [] [] (trContStack (Cont.fix f k)) =
    update (β := fun (k : K') ↦ List Γ')
      (update (β := fun (k : K') ↦ List Γ') (elim (trList v) [] [] (trContStack (Cont.fix f k))) main (trList v).tail)
      main (trList v.tail)
neg : List Γ'
neg₁ : ∀ x ∈ (trNat v.headI).tail, natEnd x = false
neg₂ :
  Option.elim'
    (update (β := fun (k : K') ↦ List Γ') (elim (trList v) [] [] (trContStack (Cont.fix f k))) main (trList v).tail
          main =
        (trNat v.headI).tail ∧
      trList v.tail = [])
    (fun (a : Γ') ↦
      natEnd a = true ∧
        update (β := fun (k : K') ↦ List Γ') (elim (trList v) [] [] (trContStack (Cont.fix f k))) main (trList v).tail
            main =
          (trNat v.headI).tail ++ a :: trList v.tail)
    (some Γ'.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 (bif false then Λ'.ret (trCont k) else Λ'.clear natEnd main (trNormal f (Cont'.fix f (trCont k)))))
      (trList v).head?
      (update (β := fun (k : K') ↦ List Γ') (elim (trList v) [] [] (trContStack (Cont.fix f k))) main (trList v).tail))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (Cont'.fix f (trCont k)))) (some Γ'.cons)
      (elim (trList v.tail) [] [] (trContStack (Cont.fix f k))))

Tactic:
convert! clear_ok (splitAtPred_eq _ _ (trNat v.headI).tail (some Γ'.cons) _ _ _) using 2

Premises used: Turing.PartrecToTM2.Γ'.cons, Option.some, List.tail, Turing.PartrecToTM2.splitAtPred_eq, Turing.PartrecToTM2.clear_ok, List.headI, Turing.PartrecToTM2.trNat
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Code
k : Cont
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 Γ'
h : ¬v.headI = 0
this :
  natEnd ((trList v).head?.getD default) = false ∧ (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail
s' : Cfg'
h₁ : TrCfg (stepNormal f (Cont.fix f k) v.tail) s'
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont (Cont.fix f k)))) (some Γ'.cons)
      (elim (trList v.tail) [] [] (trContStack (Cont.fix f k))))
    s'
h₃ : elim (trList v.tail) [] [] (trContStack (Cont.fix f k)) = elim (trList v.tail) [] [] (trContStack (Cont.fix f k))
⊢ elim (trList v.tail) [] [] (trContStack (Cont.fix f k)) =
    update (β := fun (k : K') ↦ List Γ')
      (update (β := fun (k : K') ↦ List Γ') (elim (trList v) [] [] (trContStack (Cont.fix f k))) main (trList v).tail)
      main (trList v.tail)

Tactic:
simp
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Code
k : Cont
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 Γ'
h : ¬v.headI = 0
this :
  natEnd ((trList v).head?.getD default) = false ∧ (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail
s' : Cfg'
h₁ : TrCfg (stepNormal f (Cont.fix f k) v.tail) s'
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont (Cont.fix f k)))) (some Γ'.cons)
      (elim (trList v.tail) [] [] (trContStack (Cont.fix f k))))
    s'
⊢ elim (trList v.tail) [] [] (trContStack (Cont.fix f k)) = elim (trList v.tail) [] [] (trContStack (Cont.fix f k))

Tactic:
rfl

Premises used: rfl