awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
⊢ ∃ (s' : Option Γ'),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s (elim (trList ((n + 1) :: v)) [] c d))
      (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) s' (elim (trList ((n + 1) :: v).tail) [] c d))
        (fun (n_1 : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
          TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) s' (elim (trList (n_1 :: ((n + 1) :: v).tail)) [] c d))
        ((n + 1) :: v).headI)

Tactic:
⟨none, ?_⟩

Premises used: Option.none, Exists.intro
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
cons :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s (elim (trList ((n + 1) :: v)) [] c d))
    (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) none (elim (trList ((n + 1) :: v).tail) [] c d))
      (fun (n_1 : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
        TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) none (elim (trList (n_1 :: ((n + 1) :: v).tail)) [] c d))
      ((n + 1) :: v).headI)
⊢ ∃ (s' : Option Γ'),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s (elim (trList ((n + 1) :: v)) [] c d))
      (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) s' (elim (trList ((n + 1) :: v).tail) [] c d))
        (fun (n_1 : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
          TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) s' (elim (trList (n_1 :: ((n + 1) :: v).tail)) [] c d))
        ((n + 1) :: v).headI)

Tactic:
refine ⟨none, ?_⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
cons :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
      (elim (trPosNum (Num.succ' (↑n : Num)) ++ Γ'.cons :: trList v) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) none
      (elim
        (HAppend.hAppend (α := List Γ')
          (match (motive := Num → List Γ') (↑n : Num) with
            | Num.zero => []
            | Num.pos n => trPosNum n :
            List Γ')
          (Γ'.cons :: trList v))
        [] c d))
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s (elim (trList ((n + 1) :: v)) [] c d))
    (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) none (elim (trList ((n + 1) :: v).tail) [] c d))
      (fun (n_1 : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
        TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) none (elim (trList (n_1 :: ((n + 1) :: v).tail)) [] c d))
      ((n + 1) :: v).headI)

Tactic:
simp only [trList, trNat.eq_1, trNum, Nat.cast_succ, Num.add_one, Num.succ,
    List.tail_cons, List.headI_cons]

Premises used: Nat.cast_succ, Turing.PartrecToTM2.trNat.eq_1, Turing.PartrecToTM2.trList, Num.add_one, Num.succ, List.tail_cons, List.headI_cons, Turing.PartrecToTM2.trNum
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
cons :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
      (elim (trPosNum Num.zero.succ' ++ Γ'.cons :: trList v) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) none
      (elim
        (HAppend.hAppend (α := List Γ')
          (match (motive := Num → List Γ') Num.zero with
            | Num.zero => []
            | Num.pos n => trPosNum n :
            List Γ')
          (Γ'.cons :: trList v))
        [] c d))
cons₁ :
  ∀ (a : PosNum),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
        (elim (trPosNum (Num.pos a).succ' ++ Γ'.cons :: trList v) [] c d))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) none
        (elim
          (HAppend.hAppend (α := List Γ')
            (match (motive := Num → List Γ') Num.pos a with
              | Num.zero => []
              | Num.pos n => trPosNum n :
              List Γ')
            (Γ'.cons :: trList v))
          [] c d))
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
      (elim (trPosNum (Num.succ' (↑n : Num)) ++ Γ'.cons :: trList v) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) none
      (elim
        (HAppend.hAppend (α := List Γ')
          (match (motive := Num → List Γ') (↑n : Num) with
            | Num.zero => []
            | Num.pos n => trPosNum n :
            List Γ')
          (Γ'.cons :: trList v))
        [] c d))

Tactic:
rcases (n : Num) with - | a

Premises used: Nat.cast
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) none (elim (Γ'.cons :: trList v) [] c d))

Tactic:
TransGen.head rfl ?_

Premises used: Relation.TransGen.head, StateTransition.Reaches₁, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
cons :
  TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
    (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr (q₁.pred q₂)) s (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) none (elim (Γ'.cons :: trList v) [] c d))
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) none (elim (Γ'.cons :: trList v) [] c d))

Tactic:
refine TransGen.head rfl ?_

Premises used: Relation.TransGen.head, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
a : PosNum
this :
  ∀ (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))
obtain :
  ∀ (l₁' l₂' : List Γ') (s' : Option Γ') (e : List.reverseAux [] (trPosNum a) = l₁'.reverseAux l₂')
    (h :
      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) [] c d))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q₂)) s' (elim (l₂' ++ Γ'.cons :: trList v) l₁' c d))),
    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) [] c d))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) none (elim (trPosNum a ++ Γ'.cons :: trList v) [] c d))
⊢ 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) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) none (elim (trPosNum a ++ Γ'.cons :: trList v) [] c d))

Tactic:
obtain ⟨l₁', l₂', s', e, h⟩ := this []

Premises used: List.nil
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
a : PosNum
this :
  ∀ (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))
l₁' l₂' : List Γ'
s' : Option Γ'
e : trPosNum a = l₁'.reverseAux l₂'
h :
  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) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q₂)) s' (elim (l₂' ++ Γ'.cons :: trList v) l₁' c d))
⊢ 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) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) none (elim (trPosNum a ++ Γ'.cons :: trList v) [] c d))

Tactic:
h.trans ?_

Premises used: Relation.TransGen.trans, StateTransition.Reaches₁
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
a : PosNum
this :
  ∀ (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))
l₁' l₂' : List Γ'
s' : Option Γ'
e : trPosNum a = l₁'.reverseAux l₂'
h :
  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) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q₂)) s' (elim (l₂' ++ Γ'.cons :: trList v) l₁' c d))
refine :
  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 (unrev q₂)) s' (elim (l₂' ++ Γ'.cons :: trList v) l₁' c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) none (elim (trPosNum a ++ Γ'.cons :: trList v) [] c d))
⊢ 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) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) none (elim (trPosNum a ++ Γ'.cons :: trList v) [] c d))

Tactic:
refine h.trans ?_

Premises used: Relation.TransGen.trans
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
a : PosNum
this :
  ∀ (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))
l₁' l₂' : List Γ'
s' : Option Γ'
e : trPosNum a = l₁'.reverseAux l₂'
h :
  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) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q₂)) s' (elim (l₂' ++ Γ'.cons :: trList v) l₁' c d))
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q₂)) s' (elim (l₂' ++ Γ'.cons :: trList v) l₁' c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) none
      (update (β := fun (k : K') ↦ List Γ')
        (update (β := fun (a : K') ↦ List Γ') (elim (l₂' ++ Γ'.cons :: trList v) l₁' c d) rev []) main
        ((elim (l₂' ++ Γ'.cons :: trList v) l₁' c d rev).reverseAux (elim (l₂' ++ Γ'.cons :: trList v) l₁' c d main))))

Tactic:
unrev_ok

Premises used: Turing.PartrecToTM2.unrev_ok
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
a : PosNum
this :
  ∀ (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))
l₁' l₂' : List Γ'
s' : Option Γ'
e : trPosNum a = l₁'.reverseAux l₂'
h :
  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) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q₂)) s' (elim (l₂' ++ Γ'.cons :: trList v) l₁' c d))
h₁ :
  elim (trPosNum a ++ Γ'.cons :: trList v) [] c d =
    update (β := fun (k : K') ↦ List Γ')
      (update (β := fun (a : K') ↦ List Γ') (elim (l₂' ++ Γ'.cons :: trList v) l₁' c d) rev []) main
      ((elim (l₂' ++ Γ'.cons :: trList v) l₁' c d rev).reverseAux (elim (l₂' ++ Γ'.cons :: trList v) l₁' c d main))
⊢ 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 (unrev q₂)) s' (elim (l₂' ++ Γ'.cons :: trList v) l₁' c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) none (elim (trPosNum a ++ Γ'.cons :: trList v) [] c d))

Tactic:
convert! unrev_ok using 2

Premises used: Turing.PartrecToTM2.unrev_ok
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
a : PosNum
this :
  ∀ (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))
l₁' l₂' : List Γ'
s' : Option Γ'
e : trPosNum a = l₁'.reverseAux l₂'
h :
  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) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q₂)) s' (elim (l₂' ++ Γ'.cons :: trList v) l₁' c d))
⊢ elim (trPosNum a ++ Γ'.cons :: trList v) [] c d =
    update (β := fun (k : K') ↦ List Γ')
      (update (β := fun (a : K') ↦ List Γ') (elim (l₂' ++ Γ'.cons :: trList v) l₁' c d) rev []) main
      ((elim (l₂' ++ Γ'.cons :: trList v) l₁' c d rev).reverseAux (elim (l₂' ++ Γ'.cons :: trList v) l₁' c d main))

Tactic:
simp [e, List.reverseAux_eq]

Premises used: List.reverseAux_eq
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
a : PosNum
cons :
  ∀ (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))
⊢ 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) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) none (elim (trPosNum a ++ Γ'.cons :: trList v) [] c d))

Tactic:
suffices ∀ l₁, ∃ l₁' l₂' s',
    List.reverseAux l₁ (trPosNum a) = List.reverseAux l₁' l₂' ∧
      Reaches₁ (TM2.step tr)
        ⟨some (q₁.pred q₂), s, K'.elim (trPosNum a.succ ++ Γ'.cons :: trList v) l₁ c d⟩
        ⟨some (unrev q₂), s', K'.elim (l₂' ++ Γ'.cons :: trList v) l₁' c d⟩ by
    obtain ⟨l₁', l₂', s', e, h⟩ := this []
    simp only [List.reverseAux] at e
    refine h.trans ?_
    convert! unrev_ok using 2
    simp [e, List.reverseAux_eq]
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
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:
⟨Γ'.bit1::l₁, [], some Γ'.cons, rfl, TransGen.head rfl (TransGen.single ?_)⟩

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

Tactic:
simp [trPosNum, show PosNum.one.succ = PosNum.one.bit0 from rfl]

Premises used: Turing.PartrecToTM2.trPosNum, 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 :
  ∀ (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))),
    ∃ (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))
⊢ ∃ (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:
obtain ⟨l₁', l₂', s', e, h⟩ := IH (some Γ'.bit0) (Γ'.bit1 :: l₁)

Premises used: Option.some, Turing.PartrecToTM2.Γ'.bit1, List.cons, Turing.PartrecToTM2.Γ'.bit0
-- 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))
⊢ ∃ (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:
⟨l₁', l₂', s', e, TransGen.head ?_ h⟩

Premises used: Relation.TransGen.head, And.intro, Exists.intro