awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (β := fun (k : K) ↦ Option (Γ k)) (R.nth n).2 k (some (f v)))
        ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n]
        (Tape.mk' L
          (ListBlank.modifyNth (fun (a : Γ' K Γ) ↦ (a.1, update (β := fun (k : K) ↦ Option (Γ k)) a.2 k (some (f v)))) n
            R))
i : ℕ
h_1 : ¬i = (S k).length
h : (S k).length < i
⊢ ((List.map some (S k)).reverse ++ [some (f v)]).length ≤ i

Tactic:
simp only [Nat.add_one_le_iff, h, List.length, le_of_lt, List.length_reverse,
            List.length_append, List.length_map]

Premises used: List.length_reverse, le_of_lt, List.length_append, Nat.add_one_le_iff, List.length_map, List.length
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (β := fun (k : K) ↦ Option (Γ k)) (R.nth n).2 k (some (f v)))
        ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n]
        (Tape.mk' L
          (ListBlank.modifyNth (fun (a : Γ' K Γ) ↦ (a.1, update (β := fun (k : K) ↦ Option (Γ k)) a.2 k (some (f v)))) n
            R))
i : ℕ
h_1 : ¬i = (S k).length
h : (S k).length < i
⊢ (List.map some (S k)).reverse.length ≤ i

Tactic:
simp only [Nat.add_one_le_iff, h, List.length, le_of_lt, List.length_reverse,
            List.length_append, List.length_map]

Premises used: List.length_reverse, le_of_lt, List.length_append, Nat.add_one_le_iff, List.length_map, List.length
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (β := fun (k : K) ↦ Option (Γ k)) (R.nth n).2 k (some (f v)))
        ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n]
        (Tape.mk' L
          (ListBlank.modifyNth (fun (a : Γ' K Γ) ↦ (a.1, update (β := fun (k : K) ↦ Option (Γ k)) a.2 k (some (f v)))) n
            R))
k' : K
i : ℕ
h' : ¬k' = k
pos :
  i = (S k).length →
    update (β := fun (k : K) ↦ Option (Γ k)) (L.nth i) k (some (f v)) k' =
      ListBlank.nth (ListBlank.mk (List.map some (update (β := fun (a : K) ↦ List (Γ a)) S k (f v :: S k) k')).reverse)
        i
neg :
  ¬i = (S k).length →
    L.nth i k' =
      ListBlank.nth (ListBlank.mk (List.map some (update (β := fun (a : K) ↦ List (Γ a)) S k (f v :: S k) k')).reverse)
        i
⊢ (if i = (S k).length then update (β := fun (k : K) ↦ Option (Γ k)) (L.nth i) k (some (f v)) else L.nth i) k' =
    ListBlank.nth (ListBlank.mk (List.map some (update (β := fun (a : K) ↦ List (Γ a)) S k (f v :: S k) k')).reverse) i

Tactic:
split_ifs
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (β := fun (k : K) ↦ Option (Γ k)) (R.nth n).2 k (some (f v)))
        ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n]
        (Tape.mk' L
          (ListBlank.modifyNth (fun (a : Γ' K Γ) ↦ (a.1, update (β := fun (k : K) ↦ Option (Γ k)) a.2 k (some (f v)))) n
            R))
k' : K
i : ℕ
h' : ¬k' = k
h : i = (S k).length
pos :
  ListBlank.nth (ListBlank.mk (List.map some (S k')).reverse) i =
    ListBlank.nth (ListBlank.mk (List.map some (update (β := fun (a : K) ↦ List (Γ a)) S k (f v :: S k) k')).reverse) i
⊢ update (β := fun (k : K) ↦ Option (Γ k)) (L.nth i) k (some (f v)) k' =
    ListBlank.nth (ListBlank.mk (List.map some (update (β := fun (a : K) ↦ List (Γ a)) S k (f v :: S k) k')).reverse) i

Tactic:
rw [Function.update_of_ne h', ← proj_map_nth, hL]

Premises used: Turing.proj_map_nth, Function.update_of_ne
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (β := fun (k : K) ↦ Option (Γ k)) (R.nth n).2 k (some (f v)))
        ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n]
        (Tape.mk' L
          (ListBlank.modifyNth (fun (a : Γ' K Γ) ↦ (a.1, update (β := fun (k : K) ↦ Option (Γ k)) a.2 k (some (f v)))) n
            R))
k' : K
i : ℕ
h' : ¬k' = k
h : ¬i = (S k).length
neg : L.nth i k' = ListBlank.nth (ListBlank.mk (List.map some (S k')).reverse) i
neg₁ :
  (ListBlank.map (proj (Γ := fun (i : K) ↦ Option (Γ i)) k') L).nth i =
    ListBlank.nth (ListBlank.mk (List.map some (S k')).reverse) i
neg₂ neg₃ :
  ListBlank.nth (ListBlank.mk (List.map some (S k')).reverse) i =
    ListBlank.nth (ListBlank.mk (List.map some (S k')).reverse) i
⊢ L.nth i k' =
    ListBlank.nth (ListBlank.mk (List.map some (update (β := fun (a : K) ↦ List (Γ a)) S k (f v :: S k) k')).reverse) i

Tactic:
rw [Function.update_of_ne h', ← proj_map_nth, hL]

Premises used: Turing.proj_map_nth, Function.update_of_ne
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (β := fun (k : K) ↦ Option (Γ k)) (R.nth n).2 k (some (f v)))
        ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n]
        (Tape.mk' L
          (ListBlank.modifyNth (fun (a : Γ' K Γ) ↦ (a.1, update (β := fun (k : K) ↦ Option (Γ k)) a.2 k (some (f v)))) n
            R))
k' : K
i : ℕ
h' : ¬k' = k
h : i = (S k).length
pos pos₁ :
  ListBlank.nth (ListBlank.mk (List.map some (S k')).reverse) i =
    ListBlank.nth (ListBlank.mk (List.map some (S k')).reverse) i
⊢ ListBlank.nth (ListBlank.mk (List.map some (S k')).reverse) i =
    ListBlank.nth (ListBlank.mk (List.map some (update (β := fun (a : K) ↦ List (Γ a)) S k (f v :: S k) k')).reverse) i

Tactic:
rw [Function.update_of_ne h']

Premises used: Function.update_of_ne
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
peek :
  ∃ (L' : ListBlank ((k : K) → Option (Γ k))),
    (∀ (k_1 : K),
        ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k_1) L' =
          ListBlank.mk (List.map some (update (β := fun (a : K) ↦ List (Γ a)) S k (S k) k_1)).reverse) ∧
      TM1.stepAux q
          (f v
            ((Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))).head.2 k))
          (Tape.move Dir.right
            (Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L))))) =
        TM1.stepAux q (f v (S k).head?) ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L')))
⊢ ∃ (L' : ListBlank ((k : K) → Option (Γ k))),
    (∀ (k_1 : K),
        ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k_1) L' =
          ListBlank.mk
            (List.map some
                (update (β := fun (a : K) ↦ List (Γ a)) S k (stWrite (Γ := Γ) v (S k) (StAct.peek (Γ := Γ) f))
                  k_1)).reverse) ∧
      TM1.stepAux (trStAct (Γ := Γ) q (StAct.peek (Γ := Γ) f)) v
          ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L))) =
        TM1.stepAux q (stVar (Γ := Γ) v (S k) (StAct.peek (Γ := Γ) f))
          ((Tape.move Dir.right)^[(stWrite (Γ := Γ) v (S k) (StAct.peek (Γ := Γ) f)).length]
            (Tape.mk' ∅ (addBottom (Γ := Γ) L')))

Tactic:
simp only [stWrite, stVar, trStAct, TM1.stepAux]

Premises used: Turing.TM1.stepAux, Turing.TM2to1.trStAct, Turing.TM2to1.stVar, Turing.TM2to1.stWrite
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
peek :
  ∃ (L' : ListBlank ((k : K) → Option (Γ k))),
    (∀ (k : K),
        ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L' = ListBlank.mk (List.map some (S k)).reverse) ∧
      TM1.stepAux q
          (f v
            ((Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))).head.2 k))
          (Tape.move Dir.right
            (Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L))))) =
        TM1.stepAux q (f v (S k).head?) ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L')))
⊢ ∃ (L' : ListBlank ((k : K) → Option (Γ k))),
    (∀ (k_1 : K),
        ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k_1) L' =
          ListBlank.mk (List.map some (update (β := fun (a : K) ↦ List (Γ a)) S k (S k) k_1)).reverse) ∧
      TM1.stepAux q
          (f v
            ((Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))).head.2 k))
          (Tape.move Dir.right
            (Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L))))) =
        TM1.stepAux q (f v (S k).head?) ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L')))

Tactic:
rw [Function.update_eq_self]

Premises used: Function.update_eq_self
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
right :
  TM1.stepAux q
      (f v ((Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))).head.2 k))
      (Tape.move Dir.right
        (Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L))))) =
    TM1.stepAux q (f v (S k).head?) ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))
⊢ ∃ (L' : ListBlank ((k : K) → Option (Γ k))),
    (∀ (k : K),
        ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L' = ListBlank.mk (List.map some (S k)).reverse) ∧
      TM1.stepAux q
          (f v
            ((Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))).head.2 k))
          (Tape.move Dir.right
            (Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L))))) =
        TM1.stepAux q (f v (S k).head?) ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L')))

Tactic:
use L, hL
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
right :
  TM1.stepAux q
      (f v ((Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))).head.2 k))
      ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L))) =
    TM1.stepAux q (f v (S k).head?) ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))
⊢ TM1.stepAux q
      (f v ((Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))).head.2 k))
      (Tape.move Dir.right
        (Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L))))) =
    TM1.stepAux q (f v (S k).head?) ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))

Tactic:
rw [Tape.move_left_right]

Premises used: Turing.Tape.move_left_right
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
right :
  (Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))).head.2 k = (S k).head?
⊢ TM1.stepAux q
      (f v ((Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))).head.2 k))
      ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L))) =
    TM1.stepAux q (f v (S k).head?) ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))

Tactic:
congr
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
right :
  ∀ (e : S k = []),
    (Tape.move Dir.left
              ((Tape.move Dir.right)^[List.length.{u_2} (α := Γ k) []] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))).head.2
        k =
      List.head? []
right₁ :
  ∀ (head : Γ k) (tail : List (Γ k)) (e : S k = head :: tail),
    (Tape.move Dir.left ((Tape.move Dir.right)^[(head :: tail).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))).head.2 k =
      (head :: tail).head?
⊢ (Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))).head.2 k = (S k).head?

Tactic:
cases e : S k
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
e : S k = []
⊢ (Tape.move Dir.left
            ((Tape.move Dir.right)^[List.length.{u_2} (α := Γ k) []] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))).head.2
      k =
    List.head? []

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
head : Γ k
tail : List (Γ k)
e : S k = head :: tail
right : some head = (head :: tail).head?
⊢ (Tape.move Dir.left ((Tape.move Dir.right)^[(head :: tail).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))).head.2 k =
    (head :: tail).head?

Tactic:
rw [List.length_cons, iterate_succ', Function.comp, Tape.move_right_left,
      Tape.move_right_n_head, Tape.mk'_nth_nat, addBottom_nth_snd, stk_nth_val _ (hL k), e,
      List.reverse_cons, ← List.length_reverse, List.getElem?_concat_length]

Premises used: Turing.Tape.move_right_n_head, Turing.TM2to1.stk_nth_val, List.length_cons, List.length_reverse, Function.iterate_succ', Function.comp, List.getElem?_concat_length, List.reverse_cons, Turing.Tape.move_right_left, Turing.Tape.mk'_nth_nat, Turing.TM2to1.addBottom_nth_snd
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
head : Γ k
tail : List (Γ k)
e : S k = head :: tail
⊢ some head = (head :: tail).head?

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
pop :
  ∃ (L' : ListBlank ((k : K) → Option (Γ k))),
    (∀ (k_1 : K),
        ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k_1) L' =
          ListBlank.mk (List.map some (update (β := fun (a : K) ↦ List (Γ a)) S k (S k).tail k_1)).reverse) ∧
      (bif ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L))).head.1 then
          TM1.stepAux q (f v none) ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))
        else
          TM1.stepAux q
            (f v
              ((Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))).head.2
                k))
            (Tape.write
              ((Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))).head.1,
                update (β := fun (k : K) ↦ Option (Γ k))
                  (Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))).head.2
                  k none)
              (Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))))) =
        TM1.stepAux q (f v (S k).head?) ((Tape.move Dir.right)^[(S k).tail.length] (Tape.mk' ∅ (addBottom (Γ := Γ) L')))
⊢ ∃ (L' : ListBlank ((k : K) → Option (Γ k))),
    (∀ (k_1 : K),
        ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k_1) L' =
          ListBlank.mk
            (List.map some
                (update (β := fun (a : K) ↦ List (Γ a)) S k (stWrite (Γ := Γ) v (S k) (StAct.pop (Γ := Γ) f))
                  k_1)).reverse) ∧
      TM1.stepAux (trStAct (Γ := Γ) q (StAct.pop (Γ := Γ) f)) v
          ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L))) =
        TM1.stepAux q (stVar (Γ := Γ) v (S k) (StAct.pop (Γ := Γ) f))
          ((Tape.move Dir.right)^[(stWrite (Γ := Γ) v (S k) (StAct.pop (Γ := Γ) f)).length]
            (Tape.mk' ∅ (addBottom (Γ := Γ) L')))

Tactic:
simp only [stWrite, stVar, trStAct, TM1.stepAux]

Premises used: Turing.TM1.stepAux, Turing.TM2to1.trStAct, Turing.TM2to1.stVar, Turing.TM2to1.stWrite
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
e : S k = []
pop :
  ∃ (L' : ListBlank ((k : K) → Option (Γ k))),
    (∀ (k_1 : K),
        ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k_1) L' =
          ListBlank.mk (List.map some (update (β := fun (a : K) ↦ List (Γ a)) S k ([] : List (Γ k)) k_1)).reverse) ∧
      (bif (addBottom (Γ := Γ) L).head.1 then TM1.stepAux q (f v none) (Tape.mk' ∅ (addBottom (Γ := Γ) L))
        else
          TM1.stepAux q (f v ((ListBlank.head ∅).2 k))
            (Tape.mk' (ListBlank.tail ∅)
              (ListBlank.cons
                ((ListBlank.head ∅).1, update (β := fun (k : K) ↦ Option (Γ k)) (ListBlank.head ∅).2 k none)
                (ListBlank.cons (ListBlank.head ∅) (addBottom (Γ := Γ) L)).tail))) =
        TM1.stepAux q (f v none) (Tape.mk' ∅ (addBottom (Γ := Γ) L'))
⊢ ∃ (L' : ListBlank ((k : K) → Option (Γ k))),
    (∀ (k_1 : K),
        ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k_1) L' =
          ListBlank.mk
            (List.map some (update (β := fun (a : K) ↦ List (Γ a)) S k (List.tail [] : List (Γ k)) k_1)).reverse) ∧
      (bif ((Tape.move Dir.right)^[List.length.{u_2} (α := Γ k) []] (Tape.mk' ∅ (addBottom (Γ := Γ) L))).head.1 then
          TM1.stepAux q (f v none)
            ((Tape.move Dir.right)^[List.length.{u_2} (α := Γ k) []] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))
        else
          TM1.stepAux q
            (f v
              ((Tape.move Dir.left
                      ((Tape.move Dir.right)^[List.length.{u_2} (α := Γ k) []]
                        (Tape.mk' ∅ (addBottom (Γ := Γ) L)))).head.2
                k))
            (Tape.write
              ((Tape.move Dir.left
                      ((Tape.move Dir.right)^[List.length.{u_2} (α := Γ k) []]
                        (Tape.mk' ∅ (addBottom (Γ := Γ) L)))).head.1,
                update (β := fun (k : K) ↦ Option (Γ k))
                  (Tape.move Dir.left
                        ((Tape.move Dir.right)^[List.length.{u_2} (α := Γ k) []]
                          (Tape.mk' ∅ (addBottom (Γ := Γ) L)))).head.2
                  k none)
              (Tape.move Dir.left
                ((Tape.move Dir.right)^[List.length.{u_2} (α := Γ k) []] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))))) =
        TM1.stepAux q (f v (List.head? []))
          ((Tape.move Dir.right)^[List.length.{u_2} (α := Γ k) (List.tail [])] (Tape.mk' ∅ (addBottom (Γ := Γ) L')))

Tactic:
simp only [Tape.mk'_head, ListBlank.head_cons, Tape.move_left_mk', List.length,
        Tape.write_mk', List.head?, iterate_zero_apply, List.tail_nil]

Premises used: List.head?, Turing.Tape.move_left_mk', Turing.ListBlank.head_cons, Turing.Tape.write_mk', Turing.Tape.mk'_head, List.tail_nil, Function.iterate_zero_apply, List.length