awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
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
⊢ 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
have neg₂ : ListBlank.nth (ListBlank.mk (List.map some (S k')).reverse) i =
  ListBlank.nth (ListBlank.mk (List.map some (S k')).reverse) i
Tactic: rw [Function.update_of_ne h', ← proj_map_nth, hL]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
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
⊢ 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
have pos : ListBlank.nth (ListBlank.mk (List.map some (S k')).reverse) i =
  ListBlank.nth (ListBlank.mk (List.map some (S k')).reverse) i
Tactic: rw [Function.update_of_ne h']
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
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) → σ
⊢ ∃ (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')))
have 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')))
Tactic: simp only [stWrite, stVar, trStAct, TM1.stepAux]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
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) → σ
⊢ ∃ (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')))
have 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')))
Tactic: rw [Function.update_eq_self]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
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) → σ
⊢ ∃ (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')))
have 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)))
Tactic: use L, hL
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
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) → σ
⊢ 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)))
have 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)))
Tactic: rw [Tape.move_left_right]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
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) → σ
⊢ 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)))
have right : (Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))).head.2 k = (S k).head?
Tactic: congr
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
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) → σ
⊢ (Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))).head.2 k = (S k).head?
have 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? []
Tactic: cases e : S k
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
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? []
⊢ (Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))).head.2 k = (S k).head?
have 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?
Tactic: cases e : S k
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
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
⊢ (Tape.move Dir.left ((Tape.move Dir.right)^[(head :: tail).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))).head.2 k =
    (head :: tail).head?
have right : some head = (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]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
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) → σ
⊢ ∃ (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')))
have 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')))
Tactic: simp only [stWrite, stVar, trStAct, TM1.stepAux]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
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 = []
⊢ ∃ (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')))
have 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'))
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]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
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 = []
⊢ ∃ (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'))
have pop : ∃ (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) ∧
    (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'))
Tactic: rw [← e, Function.update_eq_self]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
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 = []
⊢ (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))
have rw : (bif true 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))
Tactic: rw [addBottom_head_fst, cond]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
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 = []
rw :
  (bif true 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))
⊢ (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))
have rw₁ : TM1.stepAux q (f v none) (Tape.mk' ∅ (addBottom (Γ := Γ) L)) =
  TM1.stepAux q (f v none) (Tape.mk' ∅ (addBottom (Γ := Γ) L))
Tactic: rw [addBottom_head_fst, cond]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
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) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
⊢ getElem? (valid := fun (as : List (Γ k)) (i : ℕ) ↦ i < as.length) (hd :: tl).reverse tl.length = some hd
have rw : getElem? (valid := fun (as : List (Γ k)) (i : ℕ) ↦ i < as.length) (tl.reverse ++ [hd]) tl.length = some hd
Tactic: rw [List.reverse_cons, ← List.length_reverse, List.getElem?_concat_length]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
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) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
rw : getElem? (valid := fun (as : List (Γ k)) (i : ℕ) ↦ i < as.length) (tl.reverse ++ [hd]) tl.length = some hd
⊢ getElem? (valid := fun (as : List (Γ k)) (i : ℕ) ↦ i < as.length) (hd :: tl).reverse tl.length = some hd
have rw₁ : getElem? (valid := fun (as : List (Γ k)) (i : ℕ) ↦ i < as.length) (tl.reverse ++ [hd]) tl.reverse.length = some hd
Tactic: rw [List.reverse_cons, ← List.length_reverse, List.getElem?_concat_length]