awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k : K'
q : Λ'
a : Γ'
s : Option Γ'
S : K' → List Γ'
Sk fst : List Γ'
fst_1 : Option Γ'
snd : List Γ'
e₃ : splitAtPred p Sk = (fst, fst_1, snd)
e₁ : S k = a :: Sk
e₂ : p a = false
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'}
    (e : splitAtPred p (S k) = ((fst, fst_1, snd).1, (fst, fst_1, snd).2.1, (fst, fst_1, snd).2.2)),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) s S)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) (fst, fst_1, snd).2.1
        (update (β := fun (k : K') ↦ List Γ') S k (fst, fst_1, snd).2.2))
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 p k q)) (some a) (update (β := fun (k : K') ↦ List Γ') S k Sk))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) fst_1 (update (β := fun (k : K') ↦ List Γ') S k snd))
⊢ 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)
    (bif
        match (motive := Option Γ' → Bool → (Γ' → Bool) → Bool) (a :: Sk).head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) (a :: Sk).head?
        (update (β := fun (k : K') ↦ List Γ') S k (a :: Sk).tail)
    else
      TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) (a :: Sk).head?
        (update (β := fun (k : K') ↦ List Γ') S k (a :: Sk).tail))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) (fst, fst_1, snd).2.1
      (update (β := fun (k : K') ↦ List Γ') S k (fst, fst_1, snd).2.2))

Tactic:
simp only [List.head?_cons, e₂, List.tail_cons, cond_false]

Premises used: List.tail_cons, List.head?_cons, cond_false
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k : K'
q : Λ'
a : Γ'
s : Option Γ'
S : K' → List Γ'
Sk fst : List Γ'
fst_1 : Option Γ'
snd : List Γ'
e₃ : splitAtPred p Sk = (fst, fst_1, snd)
e₁ : S k = a :: Sk
e₂ : p a = false
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'}
    (e : splitAtPred p (S k) = ((fst, fst_1, snd).1, (fst, fst_1, snd).2.1, (fst, fst_1, snd).2.2)),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) s S)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) (fst, fst_1, snd).2.1
        (update (β := fun (k : K') ↦ List Γ') S k (fst, fst_1, snd).2.2))
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) (some a) (update (β := fun (a : K') ↦ List Γ') S k Sk))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) (fst, fst_1, snd).2.1
      (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k Sk) k (fst, fst_1, snd).2.2))

Tactic:
@IH _ (update S k Sk) _
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k : K'
q : Λ'
a : Γ'
s : Option Γ'
S : K' → List Γ'
Sk fst : List Γ'
fst_1 : Option Γ'
snd : List Γ'
e₃ : splitAtPred p Sk = (fst, fst_1, snd)
e₁ : S k = a :: Sk
e₂ : p a = false
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'}
    (e : splitAtPred p (S k) = ((fst, fst_1, snd).1, (fst, fst_1, snd).2.1, (fst, fst_1, snd).2.2)),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) s S)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) (fst, fst_1, snd).2.1
        (update (β := fun (k : K') ↦ List Γ') S k (fst, fst_1, snd).2.2))
h :
  update (β := fun (k : K') ↦ List Γ') S k snd =
    update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k Sk) k (fst, fst_1, snd).2.2
cons :
  splitAtPred p (update (β := fun (a : K') ↦ List Γ') S k Sk k) =
    ((fst, fst_1, snd).1, (fst, fst_1, snd).2.1, (fst, fst_1, snd).2.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 p k q)) (some a) (update (β := fun (k : K') ↦ List Γ') S k Sk))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) fst_1 (update (β := fun (k : K') ↦ List Γ') S k snd))

Tactic:
convert! @IH _ (update S k Sk) _ using 2
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k : K'
q : Λ'
a : Γ'
s : Option Γ'
S : K' → List Γ'
Sk fst : List Γ'
fst_1 : Option Γ'
snd : List Γ'
e₃ : splitAtPred p Sk = (fst, fst_1, snd)
e₁ : S k = a :: Sk
e₂ : p a = false
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'}
    (e : splitAtPred p (S k) = ((fst, fst_1, snd).1, (fst, fst_1, snd).2.1, (fst, fst_1, snd).2.2)),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) s S)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) (fst, fst_1, snd).2.1
        (update (β := fun (k : K') ↦ List Γ') S k (fst, fst_1, snd).2.2))
⊢ update (β := fun (k : K') ↦ List Γ') S k snd =
    update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k Sk) k (fst, fst_1, snd).2.2

Tactic:
simp [e₃]
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k : K'
q : Λ'
a : Γ'
s : Option Γ'
S : K' → List Γ'
Sk fst : List Γ'
fst_1 : Option Γ'
snd : List Γ'
e₃ : splitAtPred p Sk = (fst, fst_1, snd)
e₁ : S k = a :: Sk
e₂ : p a = false
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'}
    (e : splitAtPred p (S k) = ((fst, fst_1, snd).1, (fst, fst_1, snd).2.1, (fst, fst_1, snd).2.2)),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) s S)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) (fst, fst_1, snd).2.1
        (update (β := fun (k : K') ↦ List Γ') S k (fst, fst_1, snd).2.2))
⊢ splitAtPred p (update (β := fun (a : K') ↦ List Γ') S k Sk k) =
    ((fst, fst_1, snd).1, (fst, fst_1, snd).2.1, (fst, fst_1, snd).2.2)

Tactic:
simp [e₃]
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k : K'
q : Λ'
s : Option Γ'
L₁ : List Γ'
o : Option Γ'
L₂ : List Γ'
S : K' → List Γ'
e : splitAtPred p (S k) = (L₁, o, L₂)
nil :
  ∀ {s : Option Γ'} {S : K' → List Γ'} (e : splitAtPred p (S k) = ([], o, L₂)),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) s S)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
cons :
  ∀ (a : Γ') (L₁ : List Γ')
    (IH :
      ∀ {s : Option Γ'} {S : K' → List Γ'} (e : splitAtPred p (S k) = (L₁, o, L₂)),
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) s S)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂)))
    {s : Option Γ'} {S : K' → List Γ'} (e : splitAtPred p (S k) = (a :: L₁, o, L₂)),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) s S)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) s S)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))

Tactic:
induction L₁ generalizing S s with
  | nil =>
    refine TransGen.head' rfl ?_
    rw [tr]; simp only [pop', TM2.step, Option.mem_def, TM2.stepAux, Option.elim]
    revert e; rcases S k with - | ⟨a, Sk⟩ <;> intro e
    · cases e
      rfl
    simp only [splitAtPred, List.head?, List.tail_cons] at e ⊢
    revert e; cases p a <;> intro e <;>
      simp only [cond_false, cond_true, Prod.mk.injEq, true_and, false_and, reduceCtorEq] at e ⊢
    rcases e with ⟨e₁, e₂⟩
    rw [e₁, e₂]
  | cons a L₁ IH =>
    refine TransGen.head rfl ?_
    rw [tr]; simp only [pop', TM2.step, Option.mem_def, TM2.stepAux, Option.elim]
    rcases e₁ : S k with - | ⟨a', Sk⟩ <;> rw [e₁, splitAtPred] at e
    · cases e
    cases e₂ : p a' <;> simp only [e₂, cond] at e
    swap
    · cases e
    rcases e₃ : splitAtPred p Sk with ⟨_, _, _⟩
    rw [e₃] at e
    cases e
    simp only [List.head?_cons, e₂, List.tail_cons, cond_false]
    convert! @IH _ (update S k Sk) _ using 2 <;> simp [e₃]

Premises used: List.head?, cond, reduceCtorEq, Turing.PartrecToTM2.tr, Turing.TM2.stepAux, Relation.TransGen.head, false_and, cond_true, List.tail_cons, Turing.TM2.step, Relation.TransGen.head', Turing.PartrecToTM2.pop', Turing.PartrecToTM2.splitAtPred, List.head?_cons, Prod.mk.injEq, Option.elim, cond_false, rfl, true_and, Option.mem_def
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
c : List Γ'
s : Option Γ'
a d : List Γ'
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.copy) s (elim a [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (List.reverseAux [] a) [] c (List.reverseAux [] d)))

Tactic:
TransGen.single ?_

Premises used: Relation.TransGen.single, StateTransition.Reaches₁
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
c : List Γ'
s : Option Γ'
a d : List Γ'
nil :
  TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (List.reverseAux [] a) [] c (List.reverseAux [] d)) ∈
    TM2.step (Γ := fun (x : K') ↦ Γ') tr (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.copy) s (elim a [] c d))
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.copy) s (elim a [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (List.reverseAux [] a) [] c (List.reverseAux [] d)))

Tactic:
refine TransGen.single ?_

Premises used: Relation.TransGen.single
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
c : List Γ'
s : Option Γ'
a d : List Γ'
⊢ TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (List.reverseAux [] a) [] c (List.reverseAux [] d)) ∈
    TM2.step (Γ := fun (x : K') ↦ Γ') tr (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.copy) s (elim a [] c d))

Tactic:
simp
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
c : List Γ'
x : Γ'
b : List Γ'
IH :
  ∀ (s : Option Γ') (a d : List Γ'),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.copy) s (elim a b c d))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (b.reverseAux a) [] c (b.reverseAux d)))
s : Option Γ'
a d : List Γ'
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.copy) s (elim a (x :: b) c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim ((x :: b).reverseAux a) [] c ((x :: b).reverseAux d)))

Tactic:
TransGen.head rfl ?_

Premises used: Relation.TransGen.head, StateTransition.Reaches₁, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
c : List Γ'
x : Γ'
b : List Γ'
IH :
  ∀ (s : Option Γ') (a d : List Γ'),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.copy) s (elim a b c d))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (b.reverseAux a) [] c (b.reverseAux d)))
s : Option Γ'
a d : List Γ'
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.copy) s (elim a (x :: b) c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim ((x :: b).reverseAux a) [] c ((x :: b).reverseAux d)))
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.copy) s (elim a (x :: b) c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim ((x :: b).reverseAux a) [] c ((x :: b).reverseAux d)))

Tactic:
refine TransGen.head rfl ?_

Premises used: Relation.TransGen.head, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
c : List Γ'
x : Γ'
b : List Γ'
IH :
  ∀ (s : Option Γ') (a d : List Γ'),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.copy) s (elim a b c d))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (b.reverseAux a) [] c (b.reverseAux d)))
s : Option Γ'
a d : List Γ'
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 q.copy) (some x)
      (elim ((some x).getD default :: a) b c ((some x).getD default :: d)))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (b.reverseAux (x :: a)) [] c (b.reverseAux (x :: d))))
⊢ TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
    (TM2.stepAux (Γ := fun (x : K') ↦ Γ')
      (pop' rev
        (branch (Γ := fun (x : K') ↦ Γ') Option.isSome
          (push' main (push' stack (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ q.copy)))
          (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ q)))
      s (elim a (x :: b) c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim ((x :: b).reverseAux a) [] c ((x :: b).reverseAux d)))

Tactic:
simp only [TM2.step, Option.mem_def, TM2.stepAux, elim_rev, List.head?_cons, Option.isSome_some,
      List.tail_cons, elim_update_rev, elim_main, elim_update_main,
      elim_stack, elim_update_stack, cond_true, List.reverseAux_cons, pop', push']

Premises used: Turing.TM2.stepAux, Turing.PartrecToTM2.push', Turing.PartrecToTM2.K'.elim_update_main, Turing.PartrecToTM2.K'.elim_rev, Turing.PartrecToTM2.K'.elim_main, cond_true, List.tail_cons, Turing.TM2.step, Turing.PartrecToTM2.pop', Turing.PartrecToTM2.K'.elim_update_stack, List.reverseAux_cons, Option.isSome_some, List.head?_cons, Turing.PartrecToTM2.K'.elim_stack, Turing.PartrecToTM2.K'.elim_update_rev, Option.mem_def
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
c : List Γ'
x : Γ'
b : List Γ'
IH :
  ∀ (s : Option Γ') (a d : List Γ'),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.copy) s (elim a b c d))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (b.reverseAux a) [] c (b.reverseAux d)))
s : Option Γ'
a d : List Γ'
⊢ 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 q.copy) (some x)
      (elim ((some x).getD default :: a) b c ((some x).getD default :: d)))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (b.reverseAux (x :: a)) [] c (b.reverseAux (x :: d))))

Tactic:
IH _ _ _

Premises used: Option.getD, Turing.TM2.step, StateTransition.Reaches₁
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
c : List Γ'
x : Γ'
b : List Γ'
IH :
  ∀ (s : Option Γ') (a d : List Γ'),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.copy) s (elim a b c d))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (b.reverseAux a) [] c (b.reverseAux d)))
s : Option Γ'
a d : List Γ'
⊢ 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 q.copy) (some x)
      (elim ((some x).getD default :: a) b c ((some x).getD default :: d)))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (b.reverseAux (x :: a)) [] c (b.reverseAux (x :: d))))

Tactic:
exact IH _ _ _
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
a b c d : List Γ'
nil :
  ∀ (s : Option Γ') (a d : List Γ'),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.copy) s (elim a [] c d))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (List.reverseAux [] a) [] c (List.reverseAux [] d)))
cons :
  ∀ (x : Γ') (b : List Γ')
    (IH :
      ∀ (s : Option Γ') (a d : List Γ'),
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.copy) s (elim a b c d))
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (b.reverseAux a) [] c (b.reverseAux d))))
    (s : Option Γ') (a d : List Γ'),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.copy) s (elim a (x :: b) c d))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim ((x :: b).reverseAux a) [] c ((x :: b).reverseAux d)))
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.copy) s (elim a b c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (b.reverseAux a) [] c (b.reverseAux d)))

Tactic:
induction b generalizing a d s with
  | nil =>
    refine TransGen.single ?_
    simp
  | cons x b IH =>
    refine TransGen.head rfl ?_
    rw [tr]
    simp only [TM2.step, Option.mem_def, TM2.stepAux, elim_rev, List.head?_cons, Option.isSome_some,
      List.tail_cons, elim_update_rev, elim_main, elim_update_main,
      elim_stack, elim_update_stack, cond_true, List.reverseAux_cons, pop', push']
    exact IH _ _ _

Premises used: Turing.PartrecToTM2.tr, Turing.TM2.stepAux, Relation.TransGen.head, Turing.PartrecToTM2.push', Turing.PartrecToTM2.K'.elim_update_main, Turing.PartrecToTM2.K'.elim_rev, Turing.PartrecToTM2.K'.elim_main, cond_true, List.tail_cons, Turing.TM2.step, Turing.PartrecToTM2.pop', Turing.PartrecToTM2.K'.elim_update_stack, List.reverseAux_cons, Option.isSome_some, Relation.TransGen.single, List.head?_cons, Turing.PartrecToTM2.K'.elim_stack, rfl, Turing.PartrecToTM2.K'.elim_update_rev, Option.mem_def
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
n : ℕ
⊢ ∀ x ∈ trNat n, natEnd x = false

Tactic:
trNum_natEnd _

Premises used: Turing.PartrecToTM2.trNum_natEnd, Turing.PartrecToTM2.trNat
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
a : ℕ
l : List ℕ
x : Γ'
h : x ∈ trList (a :: l)
⊢ x ∈ trNat a ∨ x = Γ'.cons ∨ x ∈ trList l

Tactic:
simp only [trList, List.mem_append, List.mem_cons] at h

Premises used: Turing.PartrecToTM2.trList, List.mem_append, List.mem_cons
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
a : ℕ
l : List ℕ
x : Γ'
h : x ∈ trNat a ∨ x = Γ'.cons ∨ x ∈ trList l
inl : ∀ (h : x ∈ trNat a), x ≠ Γ'.consₗ
inr : Γ'.cons ≠ Γ'.consₗ
inr₁ : ∀ (h : x ∈ trList l), x ≠ Γ'.consₗ
⊢ x ≠ Γ'.consₗ

Tactic:
obtain h | rfl | h := h

Premises used: rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
a : ℕ
l : List ℕ
h : Γ'.consₗ ∈ trNat a
⊢ False

Tactic:
cases trNat_natEnd _ _ h

Premises used: Turing.PartrecToTM2.trNat_natEnd
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
a : ℕ
l : List ℕ
x : Γ'
h : x ∈ trList l
⊢ x ≠ Γ'.consₗ

Tactic:
trList_ne_consₗ l _ h
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
a : ℕ
l : List ℕ
x : Γ'
h : x ∈ trList l
⊢ x ≠ Γ'.consₗ

Tactic:
exact trList_ne_consₗ l _ h
-- 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
⊢ main ≠ rev

Tactic:
decide
-- 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_1 :
  Option.elim' (elim (trList L) [] c d main = trNat L.headI ∧ trList L.tail = [])
    (fun (a : Γ') ↦ natEnd a = true ∧ elim (trList L) [] c d main = trNat L.headI ++ a :: trList L.tail) o
refine_2 :
  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ₗ)) main) (unrev q))
          o))
      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))
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (head main q)) s (elim (trList L) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trList [L.headI]) [] c d))

Tactic:
refine
    (move_ok (by decide)
          (splitAtPred_eq _ _ (trNat L.headI) o (trList L.tail) (trNat_natEnd _) ?_)).trans
      (TransGen.head rfl (TransGen.head rfl ?_))

Premises used: Relation.TransGen.head, Turing.PartrecToTM2.trList, Turing.PartrecToTM2.move_ok, List.tail, Turing.PartrecToTM2.splitAtPred_eq, Relation.TransGen.trans, List.headI, Turing.PartrecToTM2.trNat, rfl, Turing.PartrecToTM2.trNat_natEnd
-- 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_1 :
  let 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
refine_1₁ :
  ∀ (head : ℕ) (tail : List ℕ),
    let 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
⊢ Option.elim' (elim (trList L) [] c d main = trNat L.headI ∧ trList L.tail = [])
    (fun (a : Γ') ↦ natEnd a = true ∧ elim (trList L) [] c d main = trNat L.headI ++ a :: trList L.tail) o

Tactic:
cases L