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
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
⊢ trNormal (Γ := Γ) (stRun (Γ := Γ) s q) = goto fun (x : Γ' K Γ) (x_1 : σ) ↦ go (Γ := Γ) k s q
have peek : ∀ (a : σ → Option (Γ k) → σ),
  trNormal (Γ := Γ) (stRun (Γ := Γ) (StAct.peek (Γ := Γ) a) q) =
    goto fun (x : Γ' K Γ) (x_1 : σ) ↦ go (Γ := Γ) k (StAct.peek (Γ := Γ) a) q
Tactic: cases s
Cleared hypotheses: s
-- 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
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
⊢ trNormal (Γ := Γ) (stRun (Γ := Γ) s q) = goto fun (x : Γ' K Γ) (x_1 : σ) ↦ go (Γ := Γ) k s q
have pop : ∀ (a : σ → Option (Γ k) → σ),
  trNormal (Γ := Γ) (stRun (Γ := Γ) (StAct.pop (Γ := Γ) a) q) =
    goto fun (x : Γ' K Γ) (x_1 : σ) ↦ go (Γ := Γ) k (StAct.pop (Γ := Γ) a) q
Tactic: cases s
Cleared hypotheses: s
-- 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
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
⊢ trStmts₁ (Γ := Γ) (stRun (Γ := Γ) s q) = {go (Γ := Γ) k s q, ret (Γ := Γ) q} ∪ trStmts₁ (Γ := Γ) q
have push : ∀ (a : σ → Γ k),
  trStmts₁ (Γ := Γ) (stRun (Γ := Γ) (StAct.push (Γ := Γ) a) q) =
    {go (Γ := Γ) k (StAct.push (Γ := Γ) a) q, ret (Γ := Γ) q} ∪ trStmts₁ (Γ := Γ) q
Tactic: cases s
Cleared hypotheses: s
-- 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
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
⊢ trStmts₁ (Γ := Γ) (stRun (Γ := Γ) s q) = {go (Γ := Γ) k s q, ret (Γ := Γ) q} ∪ trStmts₁ (Γ := Γ) q
have peek : ∀ (a : σ → Option (Γ k) → σ),
  trStmts₁ (Γ := Γ) (stRun (Γ := Γ) (StAct.peek (Γ := Γ) a) q) =
    {go (Γ := Γ) k (StAct.peek (Γ := Γ) a) q, ret (Γ := Γ) q} ∪ trStmts₁ (Γ := Γ) q
Tactic: cases s
Cleared hypotheses: s
-- 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
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
⊢ trStmts₁ (Γ := Γ) (stRun (Γ := Γ) s q) = {go (Γ := Γ) k s q, ret (Γ := Γ) q} ∪ trStmts₁ (Γ := Γ) q
have pop : ∀ (a : σ → Option (Γ k) → σ),
  trStmts₁ (Γ := Γ) (stRun (Γ := Γ) (StAct.pop (Γ := Γ) a) q) =
    {go (Γ := Γ) k (StAct.pop (Γ := Γ) a) q, ret (Γ := Γ) q} ∪ trStmts₁ (Γ := Γ) q
Tactic: cases s
Cleared hypotheses: s
-- 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
o : StAct K Γ σ k
⊢ 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')))
have 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')))
Tactic: simp only [Function.update_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 : σ → Γ 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.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')))
have 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')))
Tactic: simp only [stWrite, stVar, trStAct, TM1.stepAux]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (hypothesis)
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' : 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')))
have 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))
Tactic: have := Tape.write_move_right_n fun a : Γ' K Γ ↦ (a.1, update a.2 k (some (f v)))
-- 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))
⊢ 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))))
have 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))))
Tactic: rw [Tape.move_right_n_head, List.length, Tape.mk'_nth_nat, this]
-- 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))
⊢ 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))))
have 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))))
Tactic: erw [addBottom_modifyNth fun a ↦ update a k (some (f v))]
-- 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))
⊢ 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))))
have 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))))
Tactic: rw [Nat.add_one, iterate_succ']
-- 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))
⊢ ∃ (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')))
have push : ∀ (k' : K),
  ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k')
      (ListBlank.modifyNth
        (fun (a : (k : K) → Option (Γ k)) ↦ update (β := fun (k : K) ↦ Option (Γ k)) a k (some (f v))) (S k).length L) =
    ListBlank.mk (List.map some (update (β := fun (a : K) ↦ List (Γ a)) S k (f v :: S k) k')).reverse
Tactic: refine
      ⟨_, fun k' ↦ ?_, by
        -- Porting note: `rw [...]` to `erw [...]; rfl`.
        -- https://github.com/leanprover-community/mathlib4/issues/5164
        rw [Tape.move_right_n_head, List.length, Tape.mk'_nth_nat, this]
        erw [addBottom_modifyNth fun a ↦ update a k (some (f v))]
        rw [Nat.add_one, iterate_succ']
        rfl⟩
-- 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
⊢ ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k')
      (ListBlank.modifyNth
        (fun (a : (k : K) → Option (Γ k)) ↦ update (β := fun (k : K) ↦ Option (Γ k)) a k (some (f v))) (S k).length L) =
    ListBlank.mk (List.map some (update (β := fun (a : K) ↦ List (Γ a)) S k (f v :: S k) k')).reverse
have push : ∀ (i : ℕ),
  (ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k')
          (ListBlank.modifyNth
            (fun (a : (k : K) → Option (Γ k)) ↦ update (β := fun (k : K) ↦ Option (Γ k)) a k (some (f v))) (S k).length
            L)).nth
      i =
    ListBlank.nth (ListBlank.mk (List.map some (update (β := fun (a : K) ↦ List (Γ a)) S k (f v :: S k) k')).reverse) i
Tactic: refine ListBlank.ext fun i ↦ ?_
-- 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 : ℕ
⊢ (ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k')
          (ListBlank.modifyNth
            (fun (a : (k : K) → Option (Γ k)) ↦ update (β := fun (k : K) ↦ Option (Γ k)) a k (some (f v))) (S k).length
            L)).nth
      i =
    ListBlank.nth (ListBlank.mk (List.map some (update (β := fun (a : K) ↦ List (Γ a)) S k (f v :: S k) k')).reverse) i
have push : (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: rw [ListBlank.nth_map, ListBlank.nth_modifyNth, proj, PointedMap.mk_val]
-- 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 : ℕ
⊢ (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
have pos : ∀ (h' : k' = k),
  (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: by_cases h' : k' = 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 : σ → Γ 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 : ℕ
pos :
  ∀ (h' : k' = k),
    (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
⊢ (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
have neg : ∀ (h' : ¬k' = k),
  (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: by_cases h' : k' = k