awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
conv : ((addBottom (Γ := Γ) L).nth n).2 = L.nth n
conv₁ :
  ((addBottom (Γ := Γ) L).nth n).2 =
    PointedMap.f { f := Prod.snd, map_pt' := ⋯ : PointedMap (Bool × ((k : K) → Option (Γ k))) ((k : K) → Option (Γ k)) }
      ((addBottom (Γ := Γ) L).nth n)
⊢ ((addBottom (Γ := Γ) L).nth n).2 = L.nth n

Tactic:
conv => rhs; rw [← addBottom_map L, ListBlank.nth_map]

Premises used: Turing.TM2to1.addBottom_map, Turing.ListBlank.nth_map
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
rw : ((addBottom (Γ := Γ) L).tail.nth n).1 = false
rw₁ :
  (ListBlank.nth
        (ListBlank.tail
          (ListBlank.cons (true, L.head)
            (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ : PointedMap ((k : K) → Option (Γ k)) (Γ' K Γ) } L.tail)))
        n).1 =
    false
rw₂ :
  (ListBlank.nth
        (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ : PointedMap ((k : K) → Option (Γ k)) (Γ' K Γ) } L.tail)
        n).1 =
    false
rw₃ rw₄ :
  (PointedMap.f { f := Prod.mk false, map_pt' := ⋯ : PointedMap ((k : K) → Option (Γ k)) (Γ' K Γ) } (L.tail.nth n)).1 =
    false
⊢ ((addBottom (Γ := Γ) L).nth (n + 1)).1 = false

Tactic:
rw [ListBlank.nth_succ, addBottom, ListBlank.tail_cons, ListBlank.nth_map]

Premises used: Turing.TM2to1.addBottom, Turing.ListBlank.nth_succ, Turing.ListBlank.tail_cons, Turing.ListBlank.nth_map
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
rw :
  (ListBlank.head
        (ListBlank.cons (true, L.head)
          (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ : PointedMap ((k : K) → Option (Γ k)) (Γ' K Γ) }
            L.tail))).1 =
    true
rw₁ rw₂ : (true, L.head).1 = true
⊢ (addBottom (Γ := Γ) L).head.1 = true

Tactic:
rw [addBottom, ListBlank.head_cons]

Premises used: Turing.TM2to1.addBottom, Turing.ListBlank.head_cons
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
push :
  ∀ (a : σ → Γ k),
    TM2.SupportsStmt (Γ := Γ) S (stRun (Γ := Γ) (StAct.push (Γ := Γ) a) q) ↔ TM2.SupportsStmt (Γ := Γ) S q
peek :
  ∀ (a : σ → Option (Γ k) → σ),
    TM2.SupportsStmt (Γ := Γ) S (stRun (Γ := Γ) (StAct.peek (Γ := Γ) a) q) ↔ TM2.SupportsStmt (Γ := Γ) S q
pop :
  ∀ (a : σ → Option (Γ k) → σ),
    TM2.SupportsStmt (Γ := Γ) S (stRun (Γ := Γ) (StAct.pop (Γ := Γ) a) q) ↔ TM2.SupportsStmt (Γ := Γ) S q
⊢ TM2.SupportsStmt (Γ := Γ) S (stRun (Γ := Γ) s q) ↔ TM2.SupportsStmt (Γ := Γ) S q

Tactic:
cases s
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
k : K
q : TM2.Stmt Γ Λ σ
a : σ → Γ k
⊢ TM2.SupportsStmt (Γ := Γ) S (stRun (Γ := Γ) (push (Γ := Γ) a) q) ↔ TM2.SupportsStmt (Γ := Γ) S q

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
k : K
q : TM2.Stmt Γ Λ σ
a : σ → Option (Γ k) → σ
⊢ TM2.SupportsStmt (Γ := Γ) S (stRun (Γ := Γ) (peek (Γ := Γ) a) q) ↔ TM2.SupportsStmt (Γ := Γ) S q

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
k : K
q : TM2.Stmt Γ Λ σ
a : σ → Option (Γ k) → σ
⊢ TM2.SupportsStmt (Γ := Γ) S (stRun (Γ := Γ) (pop (Γ := Γ) a) q) ↔ TM2.SupportsStmt (Γ := Γ) S q

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 : TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
f : σ → Option (Γ k) → σ
unfold :
  TM2.stepAux (Γ := Γ) (stRun (Γ := Γ) (StAct.peek (Γ := Γ) f) q) v S =
    TM2.stepAux (Γ := Γ) q (stVar (Γ := Γ) v (S k) (StAct.peek (Γ := Γ) f))
      (update (β := fun (k : K) ↦ List (Γ k)) S k
        (match (motive := StAct K Γ σ k → List (Γ k)) StAct.peek (Γ := Γ) f with
        | StAct.push f => f v :: S k
        | StAct.peek a => S k
        | StAct.pop a => (S k).tail))
⊢ TM2.stepAux (Γ := Γ) (stRun (Γ := Γ) (StAct.peek (Γ := Γ) f) q) v S =
    TM2.stepAux (Γ := Γ) q (stVar (Γ := Γ) v (S k) (StAct.peek (Γ := Γ) f))
      (update (β := fun (k : K) ↦ List (Γ k)) S k (stWrite (Γ := Γ) v (S k) (StAct.peek (Γ := Γ) f)))

Tactic:
unfold stWrite

Premises used: 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 : TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
f : σ → Option (Γ k) → σ
rw :
  TM2.stepAux (Γ := Γ) (stRun (Γ := Γ) (StAct.peek (Γ := Γ) f) q) v S =
    TM2.stepAux (Γ := Γ) q (stVar (Γ := Γ) v (S k) (StAct.peek (Γ := Γ) f)) S
⊢ TM2.stepAux (Γ := Γ) (stRun (Γ := Γ) (StAct.peek (Γ := Γ) f) q) v S =
    TM2.stepAux (Γ := Γ) q (stVar (Γ := Γ) v (S k) (StAct.peek (Γ := Γ) f))
      (update (β := fun (k : K) ↦ List (Γ k)) S k
        (match (motive := StAct K Γ σ k → List (Γ k)) StAct.peek (Γ := Γ) f with
        | StAct.push f => f v :: S k
        | StAct.peek a => S k
        | StAct.pop a => (S k).tail))

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 : TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
f : σ → Option (Γ k) → σ
⊢ TM2.stepAux (Γ := Γ) (stRun (Γ := Γ) (StAct.peek (Γ := Γ) f) q) v S =
    TM2.stepAux (Γ := Γ) q (stVar (Γ := Γ) v (S k) (StAct.peek (Γ := Γ) f)) S

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
push :
  ∀ (a : σ → Γ k),
    trNormal (Γ := Γ) (stRun (Γ := Γ) (StAct.push (Γ := Γ) a) q) =
      goto fun (x : Γ' K Γ) (x_1 : σ) ↦ go (Γ := Γ) k (StAct.push (Γ := Γ) a) q
peek :
  ∀ (a : σ → Option (Γ k) → σ),
    trNormal (Γ := Γ) (stRun (Γ := Γ) (StAct.peek (Γ := Γ) a) q) =
      goto fun (x : Γ' K Γ) (x_1 : σ) ↦ go (Γ := Γ) k (StAct.peek (Γ := Γ) a) q
pop :
  ∀ (a : σ → Option (Γ k) → σ),
    trNormal (Γ := Γ) (stRun (Γ := Γ) (StAct.pop (Γ := Γ) a) q) =
      goto fun (x : Γ' K Γ) (x_1 : σ) ↦ go (Γ := Γ) k (StAct.pop (Γ := Γ) a) q
⊢ trNormal (Γ := Γ) (stRun (Γ := Γ) s q) = goto fun (x : Γ' K Γ) (x_1 : σ) ↦ go (Γ := Γ) k s q

Tactic:
cases s
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k : K
q : TM2.Stmt Γ Λ σ
a : σ → Γ k
⊢ trNormal (Γ := Γ) (stRun (Γ := Γ) (StAct.push (Γ := Γ) a) q) =
    goto fun (x : Γ' K Γ) (x_1 : σ) ↦ go (Γ := Γ) k (StAct.push (Γ := Γ) a) q

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k : K
q : TM2.Stmt Γ Λ σ
a : σ → Option (Γ k) → σ
⊢ trNormal (Γ := Γ) (stRun (Γ := Γ) (StAct.peek (Γ := Γ) a) q) =
    goto fun (x : Γ' K Γ) (x_1 : σ) ↦ go (Γ := Γ) k (StAct.peek (Γ := Γ) a) q

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k : K
q : TM2.Stmt Γ Λ σ
a : σ → Option (Γ k) → σ
⊢ trNormal (Γ := Γ) (stRun (Γ := Γ) (StAct.pop (Γ := Γ) a) q) =
    goto fun (x : Γ' K Γ) (x_1 : σ) ↦ go (Γ := Γ) k (StAct.pop (Γ := Γ) a) q

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
push :
  ∀ (a : σ → Γ k),
    trStmts₁ (Γ := Γ) (stRun (Γ := Γ) (StAct.push (Γ := Γ) a) q) =
      {go (Γ := Γ) k (StAct.push (Γ := Γ) a) q, ret (Γ := Γ) q} ∪ trStmts₁ (Γ := Γ) q
peek :
  ∀ (a : σ → Option (Γ k) → σ),
    trStmts₁ (Γ := Γ) (stRun (Γ := Γ) (StAct.peek (Γ := Γ) a) q) =
      {go (Γ := Γ) k (StAct.peek (Γ := Γ) a) q, ret (Γ := Γ) q} ∪ trStmts₁ (Γ := Γ) q
pop :
  ∀ (a : σ → Option (Γ k) → σ),
    trStmts₁ (Γ := Γ) (stRun (Γ := Γ) (StAct.pop (Γ := Γ) a) q) =
      {go (Γ := Γ) k (StAct.pop (Γ := Γ) a) q, ret (Γ := Γ) q} ∪ trStmts₁ (Γ := Γ) q
⊢ trStmts₁ (Γ := Γ) (stRun (Γ := Γ) s q) = {go (Γ := Γ) k s q, ret (Γ := Γ) q} ∪ trStmts₁ (Γ := Γ) q

Tactic:
cases s
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k : K
q : TM2.Stmt Γ Λ σ
a : σ → Γ k
⊢ trStmts₁ (Γ := Γ) (stRun (Γ := Γ) (StAct.push (Γ := Γ) a) q) =
    {go (Γ := Γ) k (StAct.push (Γ := Γ) a) q, ret (Γ := Γ) q} ∪ trStmts₁ (Γ := Γ) q

Tactic:
simp only [trStmts₁, stRun]

Premises used: Turing.TM2to1.stRun, Turing.TM2to1.trStmts₁
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k : K
q : TM2.Stmt Γ Λ σ
a : σ → Option (Γ k) → σ
⊢ trStmts₁ (Γ := Γ) (stRun (Γ := Γ) (StAct.peek (Γ := Γ) a) q) =
    {go (Γ := Γ) k (StAct.peek (Γ := Γ) a) q, ret (Γ := Γ) q} ∪ trStmts₁ (Γ := Γ) q

Tactic:
simp only [trStmts₁, stRun]

Premises used: Turing.TM2to1.stRun, Turing.TM2to1.trStmts₁
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k : K
q : TM2.Stmt Γ Λ σ
a : σ → Option (Γ k) → σ
⊢ trStmts₁ (Γ := Γ) (stRun (Γ := Γ) (StAct.pop (Γ := Γ) a) q) =
    {go (Γ := Γ) k (StAct.pop (Γ := Γ) a) q, ret (Γ := Γ) q} ∪ trStmts₁ (Γ := Γ) q

Tactic:
simp only [trStmts₁, stRun]

Premises used: Turing.TM2to1.stRun, Turing.TM2to1.trStmts₁
-- 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
o : StAct K Γ σ k
simp :
  ∃ (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) o) k_1)).reverse) ∧
      TM1.stepAux (trStAct (Γ := Γ) q o) v ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L))) =
        TM1.stepAux q (stVar (Γ := Γ) v (S k) o)
          ((Tape.move Dir.right)^[(stWrite (Γ := Γ) v (S k) o).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L')))
⊢ let v' := stVar (Γ := Γ) v (S k) o;
  let Sk' := stWrite (Γ := Γ) v (S k) o;
  let S' := update (β := fun (a : K) ↦ List (Γ a)) S k Sk';
  ∃ (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 (trStAct (Γ := Γ) q o) v ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L))) =
        TM1.stepAux q v' ((Tape.move Dir.right)^[(S' k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L')))

Tactic:
simp only [Function.update_self]

Premises used: Function.update_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 : σ → Γ k
push :
  ∃ (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 (f v :: S k) k_1)).reverse) ∧
      TM1.stepAux q v
          (Tape.move Dir.right
            (Tape.write
              (((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L))).head.1,
                update (β := fun (k : K) ↦ Option (Γ k))
                  ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L))).head.2 k (some (f v)))
              ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L))))) =
        TM1.stepAux q v ((Tape.move Dir.right)^[(f v :: 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.push (Γ := Γ) f))
                  k_1)).reverse) ∧
      TM1.stepAux (trStAct (Γ := Γ) q (StAct.push (Γ := Γ) f)) v
          ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L))) =
        TM1.stepAux q (stVar (Γ := Γ) v (S k) (StAct.push (Γ := Γ) f))
          ((Tape.move Dir.right)^[(stWrite (Γ := Γ) v (S k) (StAct.push (Γ := Γ) 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 : σ → Γ k
⊢ ∀ (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))

Tactic:
have := Tape.write_move_right_n fun a : Γ' K Γ ↦ (a.1, update a.2 k (some (f v)))
-- 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))
rw :
  TM1.stepAux q v
      (Tape.move Dir.right
        ((Tape.move Dir.right)^[(S k).length]
          (Tape.mk' ∅
            (ListBlank.modifyNth (fun (a : Γ' K Γ) ↦ (a.1, update (β := fun (k : K) ↦ Option (Γ k)) a.2 k (some (f v))))
              (S k).length (addBottom (Γ := Γ) L))))) =
    TM1.stepAux q v
      ((Tape.move Dir.right)^[(S k).length + 1]
        (Tape.mk' ∅
          (addBottom (Γ := Γ)
            (ListBlank.modifyNth
              (fun (a : (k : K) → Option (Γ k)) ↦ update (β := fun (k : K) ↦ Option (Γ k)) a k (some (f v)))
              (S k).length L))))
⊢ TM1.stepAux q v
      (Tape.move Dir.right
        (Tape.write
          (((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L))).head.1,
            update (β := fun (k : K) ↦ Option (Γ k))
              ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L))).head.2 k (some (f v)))
          ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L))))) =
    TM1.stepAux q v
      ((Tape.move Dir.right)^[(f v :: S k).length]
        (Tape.mk' ∅
          (addBottom (Γ := Γ)
            (ListBlank.modifyNth
              (fun (a : (k : K) → Option (Γ k)) ↦ update (β := fun (k : K) ↦ Option (Γ k)) a k (some (f v)))
              (S k).length L))))

Tactic:
rw [Tape.move_right_n_head, List.length, Tape.mk'_nth_nat, this]

Premises used: Turing.Tape.move_right_n_head, Turing.Tape.mk'_nth_nat, 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))
erw :
  TM1.stepAux q v
      (Tape.move Dir.right
        ((Tape.move Dir.right)^[(S k).length]
          (Tape.mk' ∅
            (addBottom (Γ := Γ)
              (ListBlank.modifyNth
                (fun (a : (k : K) → Option (Γ k)) ↦ update (β := fun (k : K) ↦ Option (Γ k)) a k (some (f v)))
                (S k).length L))))) =
    TM1.stepAux q v
      ((Tape.move Dir.right)^[(S k).length + 1]
        (Tape.mk' ∅
          (addBottom (Γ := Γ)
            (ListBlank.modifyNth
              (fun (a : (k : K) → Option (Γ k)) ↦ update (β := fun (k : K) ↦ Option (Γ k)) a k (some (f v)))
              (S k).length L))))
⊢ TM1.stepAux q v
      (Tape.move Dir.right
        ((Tape.move Dir.right)^[(S k).length]
          (Tape.mk' ∅
            (ListBlank.modifyNth (fun (a : Γ' K Γ) ↦ (a.1, update (β := fun (k : K) ↦ Option (Γ k)) a.2 k (some (f v))))
              (S k).length (addBottom (Γ := Γ) L))))) =
    TM1.stepAux q v
      ((Tape.move Dir.right)^[(S k).length + 1]
        (Tape.mk' ∅
          (addBottom (Γ := Γ)
            (ListBlank.modifyNth
              (fun (a : (k : K) → Option (Γ k)) ↦ update (β := fun (k : K) ↦ Option (Γ k)) a k (some (f v)))
              (S k).length L))))

Tactic:
erw [addBottom_modifyNth fun a ↦ update a k (some (f v))]

Premises used: Function.update, Turing.TM2to1.addBottom_modifyNth, Option.some
-- 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))
rw :
  TM1.stepAux q v
      (Tape.move Dir.right
        ((Tape.move Dir.right)^[(S k).length]
          (Tape.mk' ∅
            (addBottom (Γ := Γ)
              (ListBlank.modifyNth
                (fun (a : (k : K) → Option (Γ k)) ↦ update (β := fun (k : K) ↦ Option (Γ k)) a k (some (f v)))
                (S k).length L))))) =
    TM1.stepAux q v
      ((Tape.move Dir.right ∘ (Tape.move Dir.right)^[(S k).length])
        (Tape.mk' ∅
          (addBottom (Γ := Γ)
            (ListBlank.modifyNth
              (fun (a : (k : K) → Option (Γ k)) ↦ update (β := fun (k : K) ↦ Option (Γ k)) a k (some (f v)))
              (S k).length L))))
⊢ TM1.stepAux q v
      (Tape.move Dir.right
        ((Tape.move Dir.right)^[(S k).length]
          (Tape.mk' ∅
            (addBottom (Γ := Γ)
              (ListBlank.modifyNth
                (fun (a : (k : K) → Option (Γ k)) ↦ update (β := fun (k : K) ↦ Option (Γ k)) a k (some (f v)))
                (S k).length L))))) =
    TM1.stepAux q v
      ((Tape.move Dir.right)^[(S k).length + 1]
        (Tape.mk' ∅
          (addBottom (Γ := Γ)
            (ListBlank.modifyNth
              (fun (a : (k : K) → Option (Γ k)) ↦ update (β := fun (k : K) ↦ Option (Γ k)) a k (some (f v)))
              (S k).length L))))

Tactic:
rw [Nat.add_one, iterate_succ']

Premises used: Function.iterate_succ', Nat.add_one
-- 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))
⊢ TM1.stepAux q v
      (Tape.move Dir.right
        ((Tape.move Dir.right)^[(S k).length]
          (Tape.mk' ∅
            (addBottom (Γ := Γ)
              (ListBlank.modifyNth
                (fun (a : (k : K) → Option (Γ k)) ↦ update (β := fun (k : K) ↦ Option (Γ k)) a k (some (f v)))
                (S k).length L))))) =
    TM1.stepAux q v
      ((Tape.move Dir.right ∘ (Tape.move Dir.right)^[(S k).length])
        (Tape.mk' ∅
          (addBottom (Γ := Γ)
            (ListBlank.modifyNth
              (fun (a : (k : K) → Option (Γ k)) ↦ update (β := fun (k : K) ↦ Option (Γ k)) a k (some (f v)))
              (S k).length L))))

Tactic:
rfl