awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
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₁ l₁' l₂' : List Γ'
s' : Option Γ'
e : (Γ'.bit1 :: l₁).reverseAux (trPosNum m) = l₁'.reverseAux l₂'
h :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) (some Γ'.bit0)
      (elim (trPosNum m.succ ++ Γ'.cons :: trList v) (Γ'.bit1 :: l₁) c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q₂)) s' (elim (l₂' ++ Γ'.cons :: trList v) l₁' c d))
cons :
  TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) (some Γ'.bit0)
      (elim (trPosNum m.succ ++ Γ'.cons :: trList v) (Γ'.bit1 :: l₁) c d) ∈
    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))
⊢ ∃ (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:
refine ⟨l₁', l₂', s', e, TransGen.head ?_ h⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
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₁ l₁' l₂' : List Γ'
s' : Option Γ'
e : (Γ'.bit1 :: l₁).reverseAux (trPosNum m) = l₁'.reverseAux l₂'
h :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) (some Γ'.bit0)
      (elim (trPosNum m.succ ++ Γ'.cons :: trList v) (Γ'.bit1 :: l₁) c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q₂)) s' (elim (l₂' ++ Γ'.cons :: trList v) l₁' c d))
cons :
  (bif decide ((trPosNum m.bit1.succ).head?.getD Γ'.cons = Γ'.bit0) then
      TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) (some ((trPosNum m.bit1.succ).head?.getD Γ'.cons))
        (elim (trPosNum m.bit1.succ ++ Γ'.cons :: trList v).tail (Γ'.bit1 :: l₁) c d)
    else
      bif
          match (motive := Γ' → Bool) (trPosNum m.bit1.succ).head?.getD Γ'.cons with
          | Γ'.consₗ => true
          | Γ'.cons => true
          | x => false then
        TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) (some ((trPosNum m.bit1.succ).head?.getD Γ'.cons))
          (elim (trPosNum m.bit1.succ ++ Γ'.cons :: trList v).tail l₁ c d)
      else
        bif
            match (motive := Γ' → Bool)
              (getElem? (valid := fun (as : List Γ') (i : ℕ) ↦ i < as.length)
                    (trPosNum m.bit1.succ ++ Γ'.cons :: trList v) 1).getD
                Γ'.consₗ with
            | Γ'.consₗ => true
            | Γ'.cons => true
            | x => false then
          TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q₂))
            (getElem? (valid := fun (as : List Γ') (i : ℕ) ↦ i < as.length)
              (trPosNum m.bit1.succ ++ Γ'.cons :: trList v) 1)
            (elim (trPosNum m.bit1.succ ++ Γ'.cons :: trList v).tail l₁ c d)
        else
          TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q₂))
            (getElem? (valid := fun (as : List Γ') (i : ℕ) ↦ i < as.length)
              (trPosNum m.bit1.succ ++ Γ'.cons :: trList v) 1)
            (elim (trPosNum m.bit1.succ ++ Γ'.cons :: trList v).tail (Γ'.bit0 :: l₁) c d)) =
    TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) (some Γ'.bit0)
      (elim (trPosNum m.succ ++ Γ'.cons :: trList v) (Γ'.bit1 :: l₁) c d)
⊢ TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) (some Γ'.bit0)
      (elim (trPosNum m.succ ++ Γ'.cons :: trList v) (Γ'.bit1 :: l₁) c d) ∈
    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))

Tactic:
simp
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
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₁ l₁' l₂' : List Γ'
s' : Option Γ'
e : (Γ'.bit1 :: l₁).reverseAux (trPosNum m) = l₁'.reverseAux l₂'
h :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) (some Γ'.bit0)
      (elim (trPosNum m.succ ++ Γ'.cons :: trList v) (Γ'.bit1 :: l₁) c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q₂)) s' (elim (l₂' ++ Γ'.cons :: trList v) l₁' c d))
⊢ (bif decide ((trPosNum m.bit1.succ).head?.getD Γ'.cons = Γ'.bit0) then
      TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) (some ((trPosNum m.bit1.succ).head?.getD Γ'.cons))
        (elim (trPosNum m.bit1.succ ++ Γ'.cons :: trList v).tail (Γ'.bit1 :: l₁) c d)
    else
      bif
          match (motive := Γ' → Bool) (trPosNum m.bit1.succ).head?.getD Γ'.cons with
          | Γ'.consₗ => true
          | Γ'.cons => true
          | x => false then
        TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) (some ((trPosNum m.bit1.succ).head?.getD Γ'.cons))
          (elim (trPosNum m.bit1.succ ++ Γ'.cons :: trList v).tail l₁ c d)
      else
        bif
            match (motive := Γ' → Bool)
              (getElem? (valid := fun (as : List Γ') (i : ℕ) ↦ i < as.length)
                    (trPosNum m.bit1.succ ++ Γ'.cons :: trList v) 1).getD
                Γ'.consₗ with
            | Γ'.consₗ => true
            | Γ'.cons => true
            | x => false then
          TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q₂))
            (getElem? (valid := fun (as : List Γ') (i : ℕ) ↦ i < as.length)
              (trPosNum m.bit1.succ ++ Γ'.cons :: trList v) 1)
            (elim (trPosNum m.bit1.succ ++ Γ'.cons :: trList v).tail l₁ c d)
        else
          TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q₂))
            (getElem? (valid := fun (as : List Γ') (i : ℕ) ↦ i < as.length)
              (trPosNum m.bit1.succ ++ Γ'.cons :: trList v) 1)
            (elim (trPosNum m.bit1.succ ++ Γ'.cons :: trList v).tail (Γ'.bit0 :: l₁) c d)) =
    TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) (some Γ'.bit0)
      (elim (trPosNum m.succ ++ Γ'.cons :: trList v) (Γ'.bit1 :: l₁) c d)

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
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 Γ'
one :
  ∀
    (IH :
      ∀ (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))),
    ∃ (a : Γ') (l : List Γ'), trPosNum PosNum.one = a :: l ∧ natEnd a = false
bit1 :
  ∀ (a : PosNum)
    (IH :
      ∀ (s : Option Γ') (l₁ : List Γ'),
        ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
          l₁.reverseAux (trPosNum a.bit1) = l₁'.reverseAux l₂' ∧
            Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
              (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
                (elim (trPosNum a.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))),
    ∃ (a_1 : Γ') (l : List Γ'), trPosNum a.bit1 = a_1 :: l ∧ natEnd a_1 = false
bit0 :
  ∀ (a : PosNum)
    (IH :
      ∀ (s : Option Γ') (l₁ : List Γ'),
        ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
          l₁.reverseAux (trPosNum a.bit0) = l₁'.reverseAux l₂' ∧
            Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
              (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
                (elim (trPosNum a.bit0.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))),
    ∃ (a_1 : Γ') (l : List Γ'), trPosNum a.bit0 = a_1 :: l ∧ natEnd a_1 = false
⊢ ∃ (a : Γ') (l : List Γ'), trPosNum m = a :: l ∧ natEnd a = false

Tactic:
cases m
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
s : Option Γ'
l₁ : List Γ'
IH :
  ∀ (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))
⊢ ∃ (a : Γ') (l : List Γ'), trPosNum PosNum.one = a :: l ∧ natEnd a = false

Tactic:
⟨_, _, rfl, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
s : Option Γ'
l₁ : List Γ'
IH :
  ∀ (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))
⊢ ∃ (a : Γ') (l : List Γ'), trPosNum PosNum.one = a :: l ∧ natEnd a = false

Tactic:
refine ⟨_, _, rfl, rfl⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
s : Option Γ'
l₁ : List Γ'
a : PosNum
IH :
  ∀ (s : Option Γ') (l₁ : List Γ'),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum a.bit1) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
            (elim (trPosNum a.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))
⊢ ∃ (a_1 : Γ') (l : List Γ'), trPosNum a.bit1 = a_1 :: l ∧ natEnd a_1 = false

Tactic:
⟨_, _, rfl, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
s : Option Γ'
l₁ : List Γ'
a : PosNum
IH :
  ∀ (s : Option Γ') (l₁ : List Γ'),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum a.bit1) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
            (elim (trPosNum a.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))
⊢ ∃ (a_1 : Γ') (l : List Γ'), trPosNum a.bit1 = a_1 :: l ∧ natEnd a_1 = false

Tactic:
refine ⟨_, _, rfl, rfl⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
s : Option Γ'
l₁ : List Γ'
a : PosNum
IH :
  ∀ (s : Option Γ') (l₁ : List Γ'),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum a.bit0) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
            (elim (trPosNum a.bit0.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))
⊢ ∃ (a_1 : Γ') (l : List Γ'), trPosNum a.bit0 = a_1 :: l ∧ natEnd a_1 = false

Tactic:
⟨_, _, rfl, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
s : Option Γ'
l₁ : List Γ'
a : PosNum
IH :
  ∀ (s : Option Γ') (l₁ : List Γ'),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum a.bit0) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
            (elim (trPosNum a.bit0.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))
⊢ ∃ (a_1 : Γ') (l : List Γ'), trPosNum a.bit0 = a_1 :: l ∧ natEnd a_1 = false

Tactic:
refine ⟨_, _, rfl, rfl⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
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 Γ'
cons :
  ∀ (a : Γ') (l : List Γ') (e : trPosNum m = a :: l) (h : natEnd a = false),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum m.bit0) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
            (elim (trPosNum m.bit0.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 Γ') (s' : Option Γ'),
    l₁.reverseAux (trPosNum m.bit0) = l₁'.reverseAux l₂' ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
          (elim (trPosNum m.bit0.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:
obtain ⟨a, l, e, h⟩ : ∃ a l, (trPosNum m = a::l) ∧ natEnd a = false := by
      cases m <;> refine ⟨_, _, rfl, rfl⟩

Premises used: Bool.false
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
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 Γ'
a : Γ'
l : List Γ'
e : trPosNum m = a :: l
h : natEnd a = false
⊢ ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
    l₁.reverseAux (trPosNum m.bit0) = l₁'.reverseAux l₂' ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
          (elim (trPosNum m.bit0.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:
⟨Γ'.bit0 :: l₁, _, some a, rfl, TransGen.single ?_⟩

Premises used: Option.some, List.cons, Turing.PartrecToTM2.Γ'.bit0, Relation.TransGen.single, And.intro, Exists.intro, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
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 Γ'
a : Γ'
l : List Γ'
e : trPosNum m = a :: l
h : natEnd a = false
cons :
  TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q₂)) (some a)
      (elim (trPosNum m ++ Γ'.cons :: trList v) (Γ'.bit0 :: l₁) c d) ∈
    TM2.step (Γ := fun (x : K') ↦ Γ') tr
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
        (elim (trPosNum m.bit0.succ ++ Γ'.cons :: trList v) l₁ c d))
⊢ ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
    l₁.reverseAux (trPosNum m.bit0) = l₁'.reverseAux l₂' ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
          (elim (trPosNum m.bit0.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:
refine ⟨Γ'.bit0 :: l₁, _, some a, rfl, TransGen.single ?_⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
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 Γ'
a : Γ'
l : List Γ'
e : trPosNum m = a :: l
h : natEnd a = false
⊢ some Γ'.bit1 ≠ some Γ'.bit0

Tactic:
decide
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
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 Γ'
a : Γ'
l : List Γ'
e : trPosNum m = a :: l
h : natEnd a = false
cons :
  (bif natEnd Γ'.bit1 then
      TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) (some Γ'.bit1) (elim (a :: (l ++ Γ'.cons :: trList v)) l₁ c d)
    else
      TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q₂)) (some a)
        (elim (a :: (l ++ Γ'.cons :: trList v)) (Γ'.bit0 :: l₁) c d)) =
    TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q₂)) (some a)
      (elim (a :: (l ++ Γ'.cons :: trList v)) (Γ'.bit0 :: l₁) c d)
⊢ TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q₂)) (some a)
      (elim (trPosNum m ++ Γ'.cons :: trList v) (Γ'.bit0 :: l₁) c d) ∈
    TM2.step (Γ := fun (x : K') ↦ Γ') tr
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
        (elim (trPosNum m.bit0.succ ++ Γ'.cons :: trList v) l₁ c d))

Tactic:
simp [trPosNum, PosNum.succ, e, h, show some Γ'.bit1 ≠ some Γ'.bit0 by decide,
      Option.getD, -natEnd]

Premises used: Option.getD, Turing.PartrecToTM2.trPosNum, Turing.PartrecToTM2.natEnd, PosNum.succ
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
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 Γ'
a : Γ'
l : List Γ'
e : trPosNum m = a :: l
h : natEnd a = false
⊢ (bif natEnd Γ'.bit1 then
      TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) (some Γ'.bit1) (elim (a :: (l ++ Γ'.cons :: trList v)) l₁ c d)
    else
      TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q₂)) (some a)
        (elim (a :: (l ++ Γ'.cons :: trList v)) (Γ'.bit0 :: l₁) c d)) =
    TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q₂)) (some a)
      (elim (a :: (l ++ Γ'.cons :: trList v)) (Γ'.bit0 :: l₁) c d)

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
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₂

Tactic:
⟨_, ⟨s, rfl⟩, TransGen.single ?_⟩

Premises used: Relation.TransGen.single, And.intro, Exists.intro, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont
v : List ℕ
s : Option Γ'
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)))
⊢ ∃ (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:
refine ⟨_, ⟨s, rfl⟩, TransGen.single ?_⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont
v : List ℕ
s : Option Γ'
⊢ 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:
simp