awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
ns : List ℕ
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 Γ'
cons₂ :
  ∀ (c : Cfg') (h₁ : TrCfg (stepRet k (ns.headI :: v)) c)
    (h₂ :
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont k))) none
          (elim (trList (ns.headI :: v)) [] [] (trContStack k)))
        c),
    ∃ (b₂ : Cfg'),
      TrCfg (stepRet (Cont.cons₂ ns k) v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont (Cont.cons₂ ns k)))) s
            (elim (trList v) [] [] (trContStack (Cont.cons₂ ns k))))
          b₂
⊢ ∃ (b₂ : Cfg'),
    TrCfg (stepRet (Cont.cons₂ ns k) v) b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont (Cont.cons₂ ns k)))) s
          (elim (trList v) [] [] (trContStack (Cont.cons₂ ns k))))
        b₂

Tactic:
obtain ⟨c, h₁, h₂⟩ := IH (ns.headI :: v) none

Premises used: List.cons, Option.none, List.headI
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
ns : List ℕ
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 Γ'
c : Cfg'
h₁ : TrCfg (stepRet k (ns.headI :: v)) c
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont k))) none
      (elim (trList (ns.headI :: v)) [] [] (trContStack k)))
    c
⊢ ∃ (b₂ : Cfg'),
    TrCfg (stepRet (Cont.cons₂ ns k) v) b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont (Cont.cons₂ ns k)))) s
          (elim (trList v) [] [] (trContStack (Cont.cons₂ ns k))))
        b₂

Tactic:
⟨c, h₁, TransGen.head rfl <| head_stack_ok.trans h₂⟩

Premises used: Relation.TransGen.head, Turing.PartrecToTM2.head_stack_ok, Relation.TransGen.trans, And.intro, Exists.intro, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
ns : List ℕ
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 Γ'
c : Cfg'
h₁ : TrCfg (stepRet k (ns.headI :: v)) c
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont k))) none
      (elim (trList (ns.headI :: v)) [] [] (trContStack k)))
    c
⊢ ∃ (b₂ : Cfg'),
    TrCfg (stepRet (Cont.cons₂ ns k) v) b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont (Cont.cons₂ ns k)))) s
          (elim (trList v) [] [] (trContStack (Cont.cons₂ ns k))))
        b₂

Tactic:
exact ⟨c, h₁, TransGen.head rfl <| head_stack_ok.trans h₂⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Code
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 Γ'
comp :
  ∀ (s' : Cfg') (h₁ : TrCfg (stepNormal f k v) s')
    (h₂ :
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s (elim (trList v) [] [] (trContStack k)))
        s'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepRet (Cont.comp f k) v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont (Cont.comp f k)))) s
            (elim (trList v) [] [] (trContStack (Cont.comp f k))))
          b₂
⊢ ∃ (b₂ : Cfg'),
    TrCfg (stepRet (Cont.comp f k) v) b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont (Cont.comp f k)))) s
          (elim (trList v) [] [] (trContStack (Cont.comp f k))))
        b₂

Tactic:
obtain ⟨s', h₁, h₂⟩ := trNormal_respects f k v s

Premises used: Turing.PartrecToTM2.trNormal_respects
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Code
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 f k v) s'
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s (elim (trList v) [] [] (trContStack k))) s'
⊢ ∃ (b₂ : Cfg'),
    TrCfg (stepRet (Cont.comp f k) v) b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont (Cont.comp f k)))) s
          (elim (trList v) [] [] (trContStack (Cont.comp f k))))
        b₂

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

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

Tactic:
exact ⟨_, h₁, TransGen.head rfl 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 Γ'
nil :
  if Eq (α := ℕ) (List.headI []) 0 then
    natEnd ((trList []).head?.getD default) = true ∧ (trList []).tail = trList (List.tail [])
  else
    natEnd ((trList []).head?.getD default) = false ∧
      (trList []).tail = (trNat (List.headI [])).tail ++ Γ'.cons :: trList (List.tail [])
cons :
  ∀ (n : ℕ) (tail : List ℕ),
    if (n :: tail).headI = 0 then
      natEnd ((trList (n :: tail)).head?.getD default) = true ∧ (trList (n :: tail)).tail = trList (n :: tail).tail
    else
      natEnd ((trList (n :: tail)).head?.getD default) = false ∧
        (trList (n :: tail)).tail = (trNat (n :: tail).headI).tail ++ Γ'.cons :: trList (n :: tail).tail
⊢ 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

Tactic:
obtain - | n := v
-- 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₂
s : Option Γ'
⊢ if Eq (α := ℕ) (List.headI []) 0 then
    natEnd ((trList []).head?.getD default) = true ∧ (trList []).tail = trList (List.tail [])
  else
    natEnd ((trList []).head?.getD default) = false ∧
      (trList []).tail = (trNat (List.headI [])).tail ++ Γ'.cons :: trList (List.tail [])

Tactic:
⟨rfl, rfl⟩

Premises used: And.intro, rfl, ite
-- 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₂
s : Option Γ'
⊢ if Eq (α := ℕ) (List.headI []) 0 then
    natEnd ((trList []).head?.getD default) = true ∧ (trList []).tail = trList (List.tail [])
  else
    natEnd ((trList []).head?.getD default) = false ∧
      (trList []).tail = (trNat (List.headI [])).tail ++ Γ'.cons :: trList (List.tail [])

Tactic:
exact ⟨rfl, 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₂
s : Option Γ'
n : ℕ
tail : List ℕ
cons :
  if (0 :: tail).headI = 0 then
    natEnd ((trList (0 :: tail)).head?.getD default) = true ∧ (trList (0 :: tail)).tail = trList (0 :: tail).tail
  else
    natEnd ((trList (0 :: tail)).head?.getD default) = false ∧
      (trList (0 :: tail)).tail = (trNat (0 :: tail).headI).tail ++ Γ'.cons :: trList (0 :: tail).tail
cons₁ :
  ∀ (n : ℕ),
    if ((n + 1) :: tail).headI = 0 then
      natEnd ((trList ((n + 1) :: tail)).head?.getD default) = true ∧
        (trList ((n + 1) :: tail)).tail = trList ((n + 1) :: tail).tail
    else
      natEnd ((trList ((n + 1) :: tail)).head?.getD default) = false ∧
        (trList ((n + 1) :: tail)).tail =
          (trNat ((n + 1) :: tail).headI).tail ++ Γ'.cons :: trList ((n + 1) :: tail).tail
⊢ if (n :: tail).headI = 0 then
    natEnd ((trList (n :: tail)).head?.getD default) = true ∧ (trList (n :: tail)).tail = trList (n :: tail).tail
  else
    natEnd ((trList (n :: tail)).head?.getD default) = false ∧
      (trList (n :: tail)).tail = (trNat (n :: tail).headI).tail ++ Γ'.cons :: trList (n :: tail).tail

Tactic:
rcases n with - | n
-- 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₂
s : Option Γ'
tail : List ℕ
⊢ if (0 :: tail).headI = 0 then
    natEnd ((trList (0 :: tail)).head?.getD default) = true ∧ (trList (0 :: tail)).tail = trList (0 :: tail).tail
  else
    natEnd ((trList (0 :: tail)).head?.getD default) = false ∧
      (trList (0 :: tail)).tail = (trNat (0 :: tail).headI).tail ++ Γ'.cons :: trList (0 :: tail).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₂
s : Option Γ'
tail : List ℕ
n : ℕ
cons :
  if n + 1 = 0 then
    natEnd ((trNum (Num.pos (Num.succ' (↑n : Num))) ++ Γ'.cons :: trList tail).head?.getD default) = true ∧
      (trNum (Num.pos (Num.succ' (↑n : Num))) ++ Γ'.cons :: trList tail).tail = trList tail
  else
    natEnd ((trNum (Num.pos (Num.succ' (↑n : Num))) ++ Γ'.cons :: trList tail).head?.getD default) = false ∧
      (trNum (Num.pos (Num.succ' (↑n : Num))) ++ Γ'.cons :: trList tail).tail =
        (trNum (Num.pos (Num.succ' (↑n : Num)))).tail ++ Γ'.cons :: trList tail
⊢ if ((n + 1) :: tail).headI = 0 then
    natEnd ((trList ((n + 1) :: tail)).head?.getD default) = true ∧
      (trList ((n + 1) :: tail)).tail = trList ((n + 1) :: tail).tail
  else
    natEnd ((trList ((n + 1) :: tail)).head?.getD default) = false ∧
      (trList ((n + 1) :: tail)).tail = (trNat ((n + 1) :: tail).headI).tail ++ Γ'.cons :: trList ((n + 1) :: tail).tail

Tactic:
rw [trList, List.headI, trNat, Nat.cast_succ, Num.add_one, Num.succ, List.tail]

Premises used: Nat.cast_succ, Turing.PartrecToTM2.trList, Num.add_one, Num.succ, List.tail, 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₂
s : Option Γ'
tail : List ℕ
n : ℕ
cons :
  if n + 1 = 0 then
    natEnd ((trNum (Num.pos PosNum.one) ++ Γ'.cons :: trList tail).head?.getD default) = true ∧
      (trNum (Num.pos PosNum.one) ++ Γ'.cons :: trList tail).tail = trList tail
  else
    natEnd ((trNum (Num.pos PosNum.one) ++ Γ'.cons :: trList tail).head?.getD default) = false ∧
      (trNum (Num.pos PosNum.one) ++ Γ'.cons :: trList tail).tail =
        (trNum (Num.pos PosNum.one)).tail ++ Γ'.cons :: trList tail
cons₁ :
  ∀ (a : PosNum),
    if n + 1 = 0 then
      natEnd ((trNum (Num.pos a.bit1) ++ Γ'.cons :: trList tail).head?.getD default) = true ∧
        (trNum (Num.pos a.bit1) ++ Γ'.cons :: trList tail).tail = trList tail
    else
      natEnd ((trNum (Num.pos a.bit1) ++ Γ'.cons :: trList tail).head?.getD default) = false ∧
        (trNum (Num.pos a.bit1) ++ Γ'.cons :: trList tail).tail =
          (trNum (Num.pos a.bit1)).tail ++ Γ'.cons :: trList tail
cons₂ :
  ∀ (a : PosNum),
    if n + 1 = 0 then
      natEnd ((trNum (Num.pos a.bit0) ++ Γ'.cons :: trList tail).head?.getD default) = true ∧
        (trNum (Num.pos a.bit0) ++ Γ'.cons :: trList tail).tail = trList tail
    else
      natEnd ((trNum (Num.pos a.bit0) ++ Γ'.cons :: trList tail).head?.getD default) = false ∧
        (trNum (Num.pos a.bit0) ++ Γ'.cons :: trList tail).tail =
          (trNum (Num.pos a.bit0)).tail ++ Γ'.cons :: trList tail
⊢ if n + 1 = 0 then
    natEnd ((trNum (Num.pos (Num.succ' (↑n : Num))) ++ Γ'.cons :: trList tail).head?.getD default) = true ∧
      (trNum (Num.pos (Num.succ' (↑n : Num))) ++ Γ'.cons :: trList tail).tail = trList tail
  else
    natEnd ((trNum (Num.pos (Num.succ' (↑n : Num))) ++ Γ'.cons :: trList tail).head?.getD default) = false ∧
      (trNum (Num.pos (Num.succ' (↑n : Num))) ++ Γ'.cons :: trList tail).tail =
        (trNum (Num.pos (Num.succ' (↑n : Num)))).tail ++ Γ'.cons :: trList tail

Tactic:
cases (n : Num).succ'

Premises used: Nat.cast, Num.succ'
-- 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₂
s : Option Γ'
tail : List ℕ
n : ℕ
⊢ if n + 1 = 0 then
    natEnd ((trNum (Num.pos PosNum.one) ++ Γ'.cons :: trList tail).head?.getD default) = true ∧
      (trNum (Num.pos PosNum.one) ++ Γ'.cons :: trList tail).tail = trList tail
  else
    natEnd ((trNum (Num.pos PosNum.one) ++ Γ'.cons :: trList tail).head?.getD default) = false ∧
      (trNum (Num.pos PosNum.one) ++ Γ'.cons :: trList tail).tail =
        (trNum (Num.pos PosNum.one)).tail ++ Γ'.cons :: trList tail

Tactic:
⟨rfl, rfl⟩

Premises used: And.intro, rfl, ite
-- 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₂
s : Option Γ'
tail : List ℕ
n : ℕ
⊢ if n + 1 = 0 then
    natEnd ((trNum (Num.pos PosNum.one) ++ Γ'.cons :: trList tail).head?.getD default) = true ∧
      (trNum (Num.pos PosNum.one) ++ Γ'.cons :: trList tail).tail = trList tail
  else
    natEnd ((trNum (Num.pos PosNum.one) ++ Γ'.cons :: trList tail).head?.getD default) = false ∧
      (trNum (Num.pos PosNum.one) ++ Γ'.cons :: trList tail).tail =
        (trNum (Num.pos PosNum.one)).tail ++ Γ'.cons :: trList tail

Tactic:
exact ⟨rfl, 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₂
s : Option Γ'
tail : List ℕ
n : ℕ
a : PosNum
⊢ if n + 1 = 0 then
    natEnd ((trNum (Num.pos a.bit1) ++ Γ'.cons :: trList tail).head?.getD default) = true ∧
      (trNum (Num.pos a.bit1) ++ Γ'.cons :: trList tail).tail = trList tail
  else
    natEnd ((trNum (Num.pos a.bit1) ++ Γ'.cons :: trList tail).head?.getD default) = false ∧
      (trNum (Num.pos a.bit1) ++ Γ'.cons :: trList tail).tail = (trNum (Num.pos a.bit1)).tail ++ Γ'.cons :: trList tail

Tactic:
⟨rfl, rfl⟩

Premises used: And.intro, rfl, ite
-- 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₂
s : Option Γ'
tail : List ℕ
n : ℕ
a : PosNum
⊢ if n + 1 = 0 then
    natEnd ((trNum (Num.pos a.bit1) ++ Γ'.cons :: trList tail).head?.getD default) = true ∧
      (trNum (Num.pos a.bit1) ++ Γ'.cons :: trList tail).tail = trList tail
  else
    natEnd ((trNum (Num.pos a.bit1) ++ Γ'.cons :: trList tail).head?.getD default) = false ∧
      (trNum (Num.pos a.bit1) ++ Γ'.cons :: trList tail).tail = (trNum (Num.pos a.bit1)).tail ++ Γ'.cons :: trList tail

Tactic:
exact ⟨rfl, 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₂
s : Option Γ'
tail : List ℕ
n : ℕ
a : PosNum
⊢ if n + 1 = 0 then
    natEnd ((trNum (Num.pos a.bit0) ++ Γ'.cons :: trList tail).head?.getD default) = true ∧
      (trNum (Num.pos a.bit0) ++ Γ'.cons :: trList tail).tail = trList tail
  else
    natEnd ((trNum (Num.pos a.bit0) ++ Γ'.cons :: trList tail).head?.getD default) = false ∧
      (trNum (Num.pos a.bit0) ++ Γ'.cons :: trList tail).tail = (trNum (Num.pos a.bit0)).tail ++ Γ'.cons :: trList tail

Tactic:
⟨rfl, rfl⟩

Premises used: And.intro, rfl, ite
-- 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₂
s : Option Γ'
tail : List ℕ
n : ℕ
a : PosNum
⊢ if n + 1 = 0 then
    natEnd ((trNum (Num.pos a.bit0) ++ Γ'.cons :: trList tail).head?.getD default) = true ∧
      (trNum (Num.pos a.bit0) ++ Γ'.cons :: trList tail).tail = trList tail
  else
    natEnd ((trNum (Num.pos a.bit0) ++ Γ'.cons :: trList tail).head?.getD default) = false ∧
      (trNum (Num.pos a.bit0) ++ Γ'.cons :: trList tail).tail = (trNum (Num.pos a.bit0)).tail ++ Γ'.cons :: trList tail

Tactic:
exact ⟨rfl, 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 Γ'
⊢ 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

Tactic:
have :
      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 := by
      obtain - | n := v
      · exact ⟨rfl, rfl⟩
      rcases n with - | n
      · simp
      rw [trList, List.headI, trNat, Nat.cast_succ, Num.add_one, Num.succ, List.tail]
      cases (n : Num).succ' <;> exact ⟨rfl, 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 Γ'
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
pos :
  ∀ (h : v.headI = 0),
    ∃ (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₂
neg :
  ∀ (h : ¬v.headI = 0),
    ∃ (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₂
⊢ ∃ (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:
by_cases h : v.headI = 0

Premises used: List.headI