awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
c d : List Γ'
o : Option Γ' := List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') [] none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons
⊢ Option.elim' (elim (trList []) [] c d main = trNat (List.headI []) ∧ trList (List.tail []) = [])
    (fun (a : Γ') ↦
      natEnd a = true ∧ elim (trList []) [] c d main = trNat (List.headI []) ++ a :: trList (List.tail []))
    o

Tactic:
simp [o]
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
c d : List Γ'
head : ℕ
tail : List ℕ
o : Option Γ' :=
  List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') (head :: tail) none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons
⊢ Option.elim' (elim (trList (head :: tail)) [] c d main = trNat (head :: tail).headI ∧ trList (head :: tail).tail = [])
    (fun (a : Γ') ↦
      natEnd a = true ∧
        elim (trList (head :: tail)) [] c d main = trNat (head :: tail).headI ++ a :: trList (head :: tail).tail)
    o

Tactic:
simp [o]
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') L none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons
refine_2 :
  TransGen
    (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
      (match (motive :=
          TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ') → Option (TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))) a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr l) v S)) =
        some b)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ')
      (some ((if o = some Γ'.consₗ then id else Λ'.clear (fun (x : Γ') ↦ decide (x = Γ'.consₗ)) main) (unrev q))) o
      (elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNat L.headI ++ [Γ'.cons]) [] c d))
⊢ TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
    (TM2.stepAux (Γ := fun (x : K') ↦ Γ')
      (goto (Γ := fun (x : K') ↦ Γ') fun (s : Option Γ') ↦
        (if s = some Γ'.consₗ then id else Λ'.clear (fun (x : Γ') ↦ decide (x = Γ'.consₗ)) main) (unrev q))
      o
      (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
        (update (β := fun (k : K') ↦ List Γ')
          (update (β := fun (a : K') ↦ List Γ') (elim (trList L) [] c d) main (trList L.tail)) rev
          ((trNat L.headI).reverseAux (elim (trList L) [] c d rev)))
        rev
        ((fun (s : Option Γ') ↦ (Option.getD ((fun (x : Option Γ') ↦ some Γ'.cons) s) default : Γ')) o ::
          update (β := fun (k : K') ↦ List Γ')
            (update (β := fun (a : K') ↦ List Γ') (elim (trList L) [] c d) main (trList L.tail)) rev
            ((trNat L.headI).reverseAux (elim (trList L) [] c d rev)) rev)))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trList [L.headI]) [] c d))

Tactic:
simp only [TM2.step, Option.mem_def, TM2.stepAux, elim_update_main, elim_rev, elim_update_rev,
    Function.update_self, trList]

Premises used: Turing.TM2.stepAux, Turing.PartrecToTM2.trList, Turing.PartrecToTM2.K'.elim_update_main, Turing.PartrecToTM2.K'.elim_rev, Turing.TM2.step, Function.update_self, Turing.PartrecToTM2.K'.elim_update_rev, Option.mem_def
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') L none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons
nil :
  let o : Option Γ' :=
    List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') [] none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons;
  o ≠ some Γ'.consₗ
cons :
  ∀ (head : ℕ) (tail : List ℕ),
    let o : Option Γ' :=
      List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') (head :: tail) none fun (x : ℕ) (x_1 : List ℕ) ↦
        some Γ'.cons;
    o ≠ some Γ'.consₗ
⊢ o ≠ some Γ'.consₗ

Tactic:
cases L
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
c d : List Γ'
o : Option Γ' := List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') [] none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons
⊢ o ≠ some Γ'.consₗ

Tactic:
simp [o]
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
c d : List Γ'
head : ℕ
tail : List ℕ
o : Option Γ' :=
  List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') (head :: tail) none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons
⊢ o ≠ some Γ'.consₗ

Tactic:
simp [o]
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') L none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons
refine_2 :
  TransGen
    (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
      (match (motive :=
          TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ') → Option (TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))) a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr l) v S)) =
        some b)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear (fun (x : Γ') ↦ decide (x = Γ'.consₗ)) main (unrev q))) o
      (elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNat L.headI ++ [Γ'.cons]) [] c d))
⊢ TransGen
    (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
      (match (motive :=
          TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ') → Option (TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))) a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr l) v S)) =
        some b)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ')
      (some ((if o = some Γ'.consₗ then id else Λ'.clear (fun (x : Γ') ↦ decide (x = Γ'.consₗ)) main) (unrev q))) o
      (elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNat L.headI ++ [Γ'.cons]) [] c d))

Tactic:
rw [if_neg (show o ≠ some Γ'.consₗ by cases L <;> simp [o])]

Premises used: if_neg
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') L none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons
⊢ TransGen
    (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
      (match (motive :=
          TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ') → Option (TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))) a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr l) v S)) =
        some b)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear (fun (x : Γ') ↦ decide (x = Γ'.consₗ)) main (unrev q))) o
      (elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNat L.headI ++ [Γ'.cons]) [] c d))

Tactic:
(clear_ok (splitAtPred_eq _ _ _ none [] ?_ ⟨rfl, rfl⟩)).trans ?_

Premises used: Turing.TM2.step, Option.none, Turing.PartrecToTM2.splitAtPred_eq, Relation.TransGen.trans, And.intro, Turing.PartrecToTM2.clear_ok, rfl, List.nil
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') L none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons
refine_2 :
  ∀ x ∈ elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d main,
    decide (x = Γ'.consₗ) = false
refine_2₁ :
  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)) none
      (update (β := fun (k : K') ↦ List Γ')
        (elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d) main []))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNat L.headI ++ [Γ'.cons]) [] c d))
⊢ TransGen
    (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
      (match (motive :=
          TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ') → Option (TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))) a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr l) v S)) =
        some b)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear (fun (x : Γ') ↦ decide (x = Γ'.consₗ)) main (unrev q))) o
      (elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNat L.headI ++ [Γ'.cons]) [] c d))

Tactic:
refine (clear_ok (splitAtPred_eq _ _ _ none [] ?_ ⟨rfl, rfl⟩)).trans ?_

Premises used: Option.none, Turing.PartrecToTM2.splitAtPred_eq, Relation.TransGen.trans, And.intro, Turing.PartrecToTM2.clear_ok, rfl, List.nil
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') L none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons
⊢ ∀ x ∈ elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d main,
    decide (x = Γ'.consₗ) = false

Tactic:
fun x h => Bool.decide_false (trList_ne_consₗ _ _ h)

Premises used: List.tail, Turing.PartrecToTM2.trList_ne_consₗ, Bool.decide_false
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') L none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons
⊢ ∀ x ∈ elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d main,
    decide (x = Γ'.consₗ) = false

Tactic:
exact fun x h => Bool.decide_false (trList_ne_consₗ _ _ h)

Premises used: Turing.PartrecToTM2.trList_ne_consₗ, Bool.decide_false
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') L none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) none
      (update (β := fun (k : K') ↦ List Γ')
        (elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d) main []))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none
      (update (β := fun (k : K') ↦ List Γ')
        (update (β := fun (a : K') ↦ List Γ')
          (update (β := fun (k : K') ↦ List Γ')
            (elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d) main [])
          rev [])
        main
        ((update (β := fun (k : K') ↦ List Γ')
              (elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d) main []
              rev).reverseAux
          (update (β := fun (k : K') ↦ List Γ')
            (elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d) main [] main))))

Tactic:
unrev_ok

Premises used: Turing.PartrecToTM2.unrev_ok
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') L none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons
h :
  elim (trNat L.headI ++ [Γ'.cons]) [] c d =
    update (β := fun (k : K') ↦ List Γ')
      (update (β := fun (a : K') ↦ List Γ')
        (update (β := fun (k : K') ↦ List Γ')
          (elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d) main [])
        rev [])
      main
      ((update (β := fun (k : K') ↦ List Γ')
            (elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d) main []
            rev).reverseAux
        (update (β := fun (k : K') ↦ List Γ')
          (elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d) main [] 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)) none
      (update (β := fun (k : K') ↦ List Γ')
        (elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d) main []))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNat L.headI ++ [Γ'.cons]) [] c d))

Tactic:
convert! unrev_ok using 2

Premises used: Turing.PartrecToTM2.unrev_ok
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') L none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons
⊢ elim (trNat L.headI ++ [Γ'.cons]) [] c d =
    update (β := fun (k : K') ↦ List Γ')
      (update (β := fun (a : K') ↦ List Γ')
        (update (β := fun (k : K') ↦ List Γ')
          (elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d) main [])
        rev [])
      main
      ((update (β := fun (k : K') ↦ List Γ')
            (elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d) main []
            rev).reverseAux
        (update (β := fun (k : K') ↦ List Γ')
          (elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d) main [] main))

Tactic:
simp [List.reverseAux_eq]

Premises used: List.reverseAux_eq
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
L₁ L₂ : List ℕ
L₃ : List Γ'
nil :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (head stack q)) s (elim (trList L₁) [] [] (trList [] ++ Γ'.consₗ :: L₃)))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trList (List.headI [] :: L₁)) [] [] L₃))
cons :
  ∀ (a : ℕ) (L₂ : List ℕ),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (head stack q)) s
        (elim (trList L₁) [] [] (trList (a :: L₂) ++ Γ'.consₗ :: L₃)))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trList ((a :: L₂).headI :: L₁)) [] [] L₃))
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (head stack q)) s (elim (trList L₁) [] [] (trList L₂ ++ Γ'.consₗ :: L₃)))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trList (L₂.headI :: L₁)) [] [] L₃))

Tactic:
rcases L₂ with - | ⟨a, L₂⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
⊢ stack ≠ rev

Tactic:
decide
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
nil :
  TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
    (TM2.stepAux (Γ := fun (x : K') ↦ Γ')
      (tr
        ((fun (x : Option Γ') ↦
            Λ'.read fun (s : Option Γ') ↦
              (if s = some Γ'.consₗ then id else Λ'.clear (fun (x : Γ') ↦ decide (x = Γ'.consₗ)) stack) (unrev q))
          (some Γ'.consₗ)))
      (some Γ'.consₗ)
      (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
        (update (β := fun (k : K') ↦ List Γ')
          (update (β := fun (a : K') ↦ List Γ') (elim (trList L₁) [] [] (trList [] ++ Γ'.consₗ :: L₃)) stack L₃) rev
          (List.reverseAux [] (elim (trList L₁) [] [] (trList [] ++ Γ'.consₗ :: L₃) rev)))
        rev
        ((fun (s : Option Γ') ↦ (Option.getD ((fun (x : Option Γ') ↦ some Γ'.cons) s) default : Γ')) (some Γ'.consₗ) ::
          update (β := fun (k : K') ↦ List Γ')
            (update (β := fun (a : K') ↦ List Γ') (elim (trList L₁) [] [] (trList [] ++ Γ'.consₗ :: L₃)) stack L₃) rev
            (List.reverseAux [] (elim (trList L₁) [] [] (trList [] ++ Γ'.consₗ :: L₃) rev)) rev)))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trList (List.headI [] :: L₁)) [] [] L₃))
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (head stack q)) s (elim (trList L₁) [] [] (trList [] ++ Γ'.consₗ :: L₃)))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trList (List.headI [] :: L₁)) [] [] L₃))

Tactic:
refine
      TransGen.trans
        (move_ok (by decide)
          (splitAtPred_eq _ _ [] (some Γ'.consₗ) L₃ (by rintro _ ⟨⟩) ⟨rfl, rfl⟩))
        (TransGen.head rfl (TransGen.head rfl ?_))

Premises used: Turing.PartrecToTM2.Γ'.consₗ, Relation.TransGen.head, Turing.PartrecToTM2.move_ok, Option.some, Turing.PartrecToTM2.splitAtPred_eq, Relation.TransGen.trans, And.intro, rfl, List.nil
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
nil :
  TransGen
    (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
      (match (motive :=
          TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ') → Option (TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))) a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr l) v S)) =
        some b)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) (some Γ'.consₗ)
      (elim (trList L₁) [(some Γ'.cons).getD default] [] L₃))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (Γ'.cons :: trList L₁) [] [] L₃))
⊢ TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
    (TM2.stepAux (Γ := fun (x : K') ↦ Γ')
      (goto (Γ := fun (x : K') ↦ Γ') fun (s : Option Γ') ↦
        (if s = some Γ'.consₗ then id else Λ'.clear (fun (x : Γ') ↦ decide (x = Γ'.consₗ)) stack) (unrev q))
      (some Γ'.consₗ)
      (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
        (update (β := fun (k : K') ↦ List Γ')
          (update (β := fun (a : K') ↦ List Γ') (elim (trList L₁) [] [] (trList [] ++ Γ'.consₗ :: L₃)) stack L₃) rev
          (List.reverseAux [] (elim (trList L₁) [] [] (trList [] ++ Γ'.consₗ :: L₃) rev)))
        rev
        ((fun (s : Option Γ') ↦ (Option.getD ((fun (x : Option Γ') ↦ some Γ'.cons) s) default : Γ')) (some Γ'.consₗ) ::
          update (β := fun (k : K') ↦ List Γ')
            (update (β := fun (a : K') ↦ List Γ') (elim (trList L₁) [] [] (trList [] ++ Γ'.consₗ :: L₃)) stack L₃) rev
            (List.reverseAux [] (elim (trList L₁) [] [] (trList [] ++ Γ'.consₗ :: L₃) rev)) rev)))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trList (List.headI [] :: L₁)) [] [] L₃))

Tactic:
simp only [TM2.step, Option.mem_def, TM2.stepAux, ite_true, id_eq, trList, List.nil_append,
      elim_update_stack, elim_rev, List.reverseAux_nil, elim_update_rev, Function.update_self,
      List.headI_nil, trNat_default]

Premises used: Turing.TM2.stepAux, Turing.PartrecToTM2.trList, Turing.PartrecToTM2.K'.elim_rev, List.reverseAux_nil, List.headI_nil, ite_true, Turing.TM2.step, Turing.PartrecToTM2.K'.elim_update_stack, Turing.PartrecToTM2.trNat_default, List.nil_append, Function.update_self, id_eq, Turing.PartrecToTM2.K'.elim_update_rev, Option.mem_def
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) (some Γ'.consₗ)
      (elim (trList L₁) [(some Γ'.cons).getD default] [] L₃))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none
      (update (β := fun (k : K') ↦ List Γ')
        (update (β := fun (a : K') ↦ List Γ') (elim (trList L₁) [(some Γ'.cons).getD default] [] L₃) rev []) main
        ((elim (trList L₁) [(some Γ'.cons).getD default] [] L₃ rev).reverseAux
          (elim (trList L₁) [(some Γ'.cons).getD default] [] L₃ main))))

Tactic:
unrev_ok

Premises used: Turing.PartrecToTM2.unrev_ok
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
h :
  elim (Γ'.cons :: trList L₁) [] [] L₃ =
    update (β := fun (k : K') ↦ List Γ')
      (update (β := fun (a : K') ↦ List Γ') (elim (trList L₁) [(some Γ'.cons).getD default] [] L₃) rev []) main
      ((elim (trList L₁) [(some Γ'.cons).getD default] [] L₃ rev).reverseAux
        (elim (trList L₁) [(some Γ'.cons).getD default] [] L₃ main))
⊢ TransGen
    (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
      (match (motive :=
          TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ') → Option (TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))) a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr l) v S)) =
        some b)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) (some Γ'.consₗ)
      (elim (trList L₁) [(some Γ'.cons).getD default] [] L₃))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (Γ'.cons :: trList L₁) [] [] L₃))

Tactic:
convert! unrev_ok using 2

Premises used: Turing.PartrecToTM2.unrev_ok
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
⊢ elim (Γ'.cons :: trList L₁) [] [] L₃ =
    update (β := fun (k : K') ↦ List Γ')
      (update (β := fun (a : K') ↦ List Γ') (elim (trList L₁) [(some Γ'.cons).getD default] [] L₃) rev []) main
      ((elim (trList L₁) [(some Γ'.cons).getD default] [] L₃ rev).reverseAux
        (elim (trList L₁) [(some Γ'.cons).getD default] [] L₃ main))

Tactic:
simp
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
a : ℕ
L₂ : List ℕ
⊢ stack ≠ rev

Tactic:
decide
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
a : ℕ
L₂ : List ℕ
⊢ elim (trList L₁) [] [] (trList (a :: L₂) ++ Γ'.consₗ :: L₃) stack =
    trNat a ++ Γ'.cons :: (trList L₂ ++ Γ'.consₗ :: L₃)

Tactic:
simp