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 : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
k' : K
i : ℕ
h' : ¬k' = k
h : ¬i = tl.length
⊢ L.nth i k' =
    ListBlank.nth (ListBlank.mk (List.map some (update (β := fun (a : K) ↦ List (Γ a)) S k (hd :: tl).tail k')).reverse)
      i
have neg : L.nth i k' = 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 : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
k' : K
i : ℕ
h' : ¬k' = k
h : ¬i = tl.length
neg : L.nth i k' = 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 (hd :: tl).tail k')).reverse)
      i
have neg₁ : (ListBlank.map (proj (Γ := fun (i : K) ↦ Option (Γ i)) k') L).nth 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 : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
k' : K
i : ℕ
h' : ¬k' = k
h : ¬i = tl.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 (hd :: tl).tail 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 : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
k' : K
i : ℕ
h' : ¬k' = k
h : i = tl.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 (hd :: tl).tail 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
M : Λ → TM2.Stmt Γ Λ σ
k : K
o : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
v : σ
S : List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some S).reverse
n : ℕ
IH :
  ∀ (H : n ≤ S.length),
    Reaches₀ (TM1.step (tr (Γ := Γ) M))
      { l := some (go (Γ := Γ) k o q), var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L) :
        TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ }
      { l := some (go (Γ := Γ) k o q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom (Γ := Γ) L)) }
H : n + 1 ≤ S.length
⊢ Reaches₀ (TM1.step (tr (Γ := Γ) M))
    { l := some (go (Γ := Γ) k o q), var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L) :
      TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ }
    { l := some (go (Γ := Γ) k o q), var := v,
      Tape := (Tape.move Dir.right)^[n + 1] (Tape.mk' ∅ (addBottom (Γ := Γ) L)) }
have succ : { l := some (go (Γ := Γ) k o q), var := v, Tape := (Tape.move Dir.right)^[n + 1] (Tape.mk' ∅ (addBottom (Γ := Γ) L)) :
    TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ } ∈
  TM1.step (tr (Γ := Γ) M)
    { l := some (go (Γ := Γ) k o q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom (Γ := Γ) L)) :
      TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ }
Tactic: apply (IH (le_of_lt H)).tail
-- 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
M : Λ → TM2.Stmt Γ Λ σ
k : K
o : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
v : σ
S : List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some S).reverse
n : ℕ
IH :
  ∀ (H : n ≤ S.length),
    Reaches₀ (TM1.step (tr (Γ := Γ) M))
      { l := some (go (Γ := Γ) k o q), var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L) :
        TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ }
      { l := some (go (Γ := Γ) k o q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom (Γ := Γ) L)) }
H : n + 1 ≤ S.length
⊢ { l := some (go (Γ := Γ) k o q), var := v, Tape := (Tape.move Dir.right)^[n + 1] (Tape.mk' ∅ (addBottom (Γ := Γ) L)) :
      TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ } ∈
    TM1.step (tr (Γ := Γ) M)
      { l := some (go (Γ := Γ) k o q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom (Γ := Γ) L)) :
        TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ }
have succ : { l := some (go (Γ := Γ) k o q), var := v,
    Tape := Tape.move Dir.right ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom (Γ := Γ) L))) :
    TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ } ∈
  TM1.step (tr (Γ := Γ) M)
    { l := some (go (Γ := Γ) k o q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom (Γ := Γ) L)) :
      TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ }
Tactic: rw [iterate_succ_apply']
-- 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
M : Λ → TM2.Stmt Γ Λ σ
k : K
o : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
v : σ
S : List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some S).reverse
n : ℕ
IH :
  ∀ (H : n ≤ S.length),
    Reaches₀ (TM1.step (tr (Γ := Γ) M))
      { l := some (go (Γ := Γ) k o q), var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L) :
        TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ }
      { l := some (go (Γ := Γ) k o q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom (Γ := Γ) L)) }
H : n + 1 ≤ S.length
⊢ { l := some (go (Γ := Γ) k o q), var := v,
      Tape := Tape.move Dir.right ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom (Γ := Γ) L))) :
      TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ } ∈
    TM1.step (tr (Γ := Γ) M)
      { l := some (go (Γ := Γ) k o q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom (Γ := Γ) L)) :
        TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ }
have succ : some
    (bif (L.nth n k).isNone then
      TM1.stepAux (trStAct (Γ := Γ) (goto fun (x : Γ' K Γ) (x_1 : σ) ↦ ret (Γ := Γ) q) o) v
        ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))
    else
      { l := some (go (Γ := Γ) k o q), var := v,
        Tape := Tape.move Dir.right ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom (Γ := Γ) L))) :
        TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ }) =
  some
    { l := some (go (Γ := Γ) k o q), var := v,
      Tape := Tape.move Dir.right ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom (Γ := Γ) L))) }
Tactic: simp only [TM1.step, TM1.stepAux, tr, Tape.mk'_nth_nat, Tape.move_right_n_head,
      addBottom_nth_snd, Option.mem_def]
-- 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
M : Λ → TM2.Stmt Γ Λ σ
k : K
o : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
v : σ
S : List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some S).reverse
n : ℕ
IH :
  ∀ (H : n ≤ S.length),
    Reaches₀ (TM1.step (tr (Γ := Γ) M))
      { l := some (go (Γ := Γ) k o q), var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L) :
        TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ }
      { l := some (go (Γ := Γ) k o q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom (Γ := Γ) L)) }
H : n + 1 ≤ S.length
⊢ some
      (bif (L.nth n k).isNone then
        TM1.stepAux (trStAct (Γ := Γ) (goto fun (x : Γ' K Γ) (x_1 : σ) ↦ ret (Γ := Γ) q) o) v
          ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))
      else
        { l := some (go (Γ := Γ) k o q), var := v,
          Tape := Tape.move Dir.right ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom (Γ := Γ) L))) :
          TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ }) =
    some
      { l := some (go (Γ := Γ) k o q), var := v,
        Tape := Tape.move Dir.right ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom (Γ := Γ) L))) }
have succ : some
    (bif (some (getElem (valid := fun (as : List (Γ k)) (i : ℕ) ↦ i < as.length) S.reverse n sorry)).isNone then
      TM1.stepAux (trStAct (Γ := Γ) (goto fun (x : Γ' K Γ) (x_1 : σ) ↦ ret (Γ := Γ) q) o) v
        ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))
    else
      { l := some (go (Γ := Γ) k o q), var := v,
        Tape := Tape.move Dir.right ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom (Γ := Γ) L))) :
        TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ }) =
  some
    { l := some (go (Γ := Γ) k o q), var := v,
      Tape := Tape.move Dir.right ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom (Γ := Γ) L))) }
Tactic: rw [stk_nth_val _ hL, List.getElem?_eq_getElem]
-- 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
M : Λ → TM2.Stmt Γ Λ σ
k : K
o : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
v : σ
S : List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some S).reverse
n : ℕ
IH :
  ∀ (H : n ≤ S.length),
    Reaches₀ (TM1.step (tr (Γ := Γ) M))
      { l := some (go (Γ := Γ) k o q), var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L) :
        TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ }
      { l := some (go (Γ := Γ) k o q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom (Γ := Γ) L)) }
H : n + 1 ≤ S.length
succ :
  some
      (bif (some (getElem (valid := fun (as : List (Γ k)) (i : ℕ) ↦ i < as.length) S.reverse n ⋯)).isNone then
        TM1.stepAux (trStAct (Γ := Γ) (goto fun (x : Γ' K Γ) (x_1 : σ) ↦ ret (Γ := Γ) q) o) v
          ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))
      else
        { l := some (go (Γ := Γ) k o q), var := v,
          Tape := Tape.move Dir.right ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom (Γ := Γ) L))) :
          TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ }) =
    some
      { l := some (go (Γ := Γ) k o q), var := v,
        Tape := Tape.move Dir.right ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom (Γ := Γ) L))) }
⊢ some
      (bif (L.nth n k).isNone then
        TM1.stepAux (trStAct (Γ := Γ) (goto fun (x : Γ' K Γ) (x_1 : σ) ↦ ret (Γ := Γ) q) o) v
          ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))
      else
        { l := some (go (Γ := Γ) k o q), var := v,
          Tape := Tape.move Dir.right ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom (Γ := Γ) L))) :
          TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ }) =
    some
      { l := some (go (Γ := Γ) k o q), var := v,
        Tape := Tape.move Dir.right ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom (Γ := Γ) L))) }
have succ₁ : n < S.reverse.length
Tactic: rw [stk_nth_val _ hL, List.getElem?_eq_getElem]
-- 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
M : Λ → TM2.Stmt Γ Λ σ
k : K
o : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
v : σ
S : List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some S).reverse
n : ℕ
IH :
  ∀ (H : n ≤ S.length),
    Reaches₀ (TM1.step (tr (Γ := Γ) M))
      { l := some (go (Γ := Γ) k o q), var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L) :
        TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ }
      { l := some (go (Γ := Γ) k o q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom (Γ := Γ) L)) }
H : n + 1 ≤ S.length
⊢ n < S.reverse.length
have succ : n < S.length
Tactic: rwa [List.length_reverse]
-- 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
M : Λ → TM2.Stmt Γ Λ σ
k : K
o : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
v : σ
S : List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some S).reverse
n : ℕ
H : n ≤ S.length
⊢ Reaches₀ (TM1.step (tr (Γ := Γ) M))
    { l := some (go (Γ := Γ) k o q), var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L) :
      TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ }
    { l := some (go (Γ := Γ) k o q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom (Γ := Γ) L)) }
have zero : ∀ (H : 0 ≤ S.length),
  Reaches₀ (TM1.step (tr (Γ := Γ) M))
    { l := some (go (Γ := Γ) k o q), var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L) :
      TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ }
    { l := some (go (Γ := Γ) k o q), var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L) }
Tactic: induction n with
  | zero => rfl
  | succ n IH =>
    apply (IH (le_of_lt H)).tail
    rw [iterate_succ_apply']
    simp only [TM1.step, TM1.stepAux, tr, Tape.mk'_nth_nat, Tape.move_right_n_head,
      addBottom_nth_snd, Option.mem_def]
    rw [stk_nth_val _ hL, List.getElem?_eq_getElem]
    · rfl
    · rwa [List.length_reverse]
Cleared hypotheses: n, 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
M : Λ → TM2.Stmt Γ Λ σ
k : K
o : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
v : σ
S : List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some S).reverse
n : ℕ
H : n ≤ S.length
zero :
  ∀ (H : 0 ≤ S.length),
    Reaches₀ (TM1.step (tr (Γ := Γ) M))
      { l := some (go (Γ := Γ) k o q), var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L) :
        TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ }
      { l := some (go (Γ := Γ) k o q), var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L) }
⊢ Reaches₀ (TM1.step (tr (Γ := Γ) M))
    { l := some (go (Γ := Γ) k o q), var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L) :
      TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ }
    { l := some (go (Γ := Γ) k o q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom (Γ := Γ) L)) }
have succ : ∀ (n : ℕ)
  (IH :
    ∀ (H : n ≤ S.length),
      Reaches₀ (TM1.step (tr (Γ := Γ) M))
        { l := some (go (Γ := Γ) k o q), var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L) :
          TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ }
        { l := some (go (Γ := Γ) k o q), var := v,
          Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom (Γ := Γ) L)) })
  (H : n + 1 ≤ S.length),
  Reaches₀ (TM1.step (tr (Γ := Γ) M))
    { l := some (go (Γ := Γ) k o q), var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L) :
      TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ }
    { l := some (go (Γ := Γ) k o q), var := v,
      Tape := (Tape.move Dir.right)^[n + 1] (Tape.mk' ∅ (addBottom (Γ := Γ) L)) }
Tactic: induction n with
  | zero => rfl
  | succ n IH =>
    apply (IH (le_of_lt H)).tail
    rw [iterate_succ_apply']
    simp only [TM1.step, TM1.stepAux, tr, Tape.mk'_nth_nat, Tape.move_right_n_head,
      addBottom_nth_snd, Option.mem_def]
    rw [stk_nth_val _ hL, List.getElem?_eq_getElem]
    · rfl
    · rwa [List.length_reverse]
Cleared hypotheses: n, 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
M : Λ → TM2.Stmt Γ Λ σ
q : TM2.Stmt Γ Λ σ
v : σ
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
IH :
  Reaches₀ (TM1.step (tr (Γ := Γ) M))
    { l := some (ret (Γ := Γ) q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom (Γ := Γ) L)) :
      TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ }
    { l := some (ret (Γ := Γ) q), var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L) }
⊢ Reaches₀ (TM1.step (tr (Γ := Γ) M))
    { l := some (ret (Γ := Γ) q), var := v, Tape := (Tape.move Dir.right)^[n + 1] (Tape.mk' ∅ (addBottom (Γ := Γ) L)) :
      TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ }
    { l := some (ret (Γ := Γ) q), var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L) }
have succ : { l := some (ret (Γ := Γ) q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom (Γ := Γ) L)) :
    TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ } ∈
  TM1.step (tr (Γ := Γ) M)
    { l := some (ret (Γ := Γ) q), var := v, Tape := (Tape.move Dir.right)^[n + 1] (Tape.mk' ∅ (addBottom (Γ := Γ) L)) :
      TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ }
Tactic: refine Reaches₀.head ?_ IH
-- 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
M : Λ → TM2.Stmt Γ Λ σ
q : TM2.Stmt Γ Λ σ
v : σ
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
IH :
  Reaches₀ (TM1.step (tr (Γ := Γ) M))
    { l := some (ret (Γ := Γ) q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom (Γ := Γ) L)) :
      TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ }
    { l := some (ret (Γ := Γ) q), var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L) }
⊢ some
      (TM1.stepAux (tr (Γ := Γ) M (ret (Γ := Γ) q)) v
        ((Tape.move Dir.right)^[n + 1] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))) =
    some { l := some (ret (Γ := Γ) q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom (Γ := Γ) L)) }
have succ : (bif false then
    TM1.stepAux (trNormal (Γ := Γ) q) v
      (Tape.move Dir.right ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom (Γ := Γ) L))))
  else
    TM1.stepAux (goto fun (x : Γ' K Γ) (x_1 : σ) ↦ ret (Γ := Γ) q) v
      ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))) =
  { l := some (ret (Γ := Γ) q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom (Γ := Γ) L)) }
Tactic: rw [Option.some_inj, tr, TM1.stepAux, Tape.move_right_n_head, Tape.mk'_nth_nat,
      addBottom_nth_succ_fst, TM1.stepAux, iterate_succ', Function.comp_apply, Tape.move_right_left]
-- 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
M : Λ → TM2.Stmt Γ Λ σ
q : TM2.Stmt Γ Λ σ
v : σ
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
⊢ Reaches₀ (TM1.step (tr (Γ := Γ) M))
    { l := some (ret (Γ := Γ) q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom (Γ := Γ) L)) :
      TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ }
    { l := some (ret (Γ := Γ) q), var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L) }
have zero : Reaches₀ (TM1.step (tr (Γ := Γ) M))
  { l := some (ret (Γ := Γ) q), var := v, Tape := (Tape.move Dir.right)^[0] (Tape.mk' ∅ (addBottom (Γ := Γ) L)) :
    TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ }
  { l := some (ret (Γ := Γ) q), var := v, Tape := (Tape.move Dir.right)^[0] (Tape.mk' ∅ (addBottom (Γ := Γ) L)) }
Tactic: induction n with
  | zero => rfl
  | succ n IH =>
    refine Reaches₀.head ?_ IH
    simp only [Option.mem_def, TM1.step]
    rw [Option.some_inj, tr, TM1.stepAux, Tape.move_right_n_head, Tape.mk'_nth_nat,
      addBottom_nth_succ_fst, TM1.stepAux, iterate_succ', Function.comp_apply, Tape.move_right_left]
    rfl
Cleared hypotheses: n
-- 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
M : Λ → TM2.Stmt Γ Λ σ
q : TM2.Stmt Γ Λ σ
v : σ
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
zero :
  Reaches₀ (TM1.step (tr (Γ := Γ) M))
    { l := some (ret (Γ := Γ) q), var := v, Tape := (Tape.move Dir.right)^[0] (Tape.mk' ∅ (addBottom (Γ := Γ) L)) :
      TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ }
    { l := some (ret (Γ := Γ) q), var := v, Tape := (Tape.move Dir.right)^[0] (Tape.mk' ∅ (addBottom (Γ := Γ) L)) }
⊢ Reaches₀ (TM1.step (tr (Γ := Γ) M))
    { l := some (ret (Γ := Γ) q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom (Γ := Γ) L)) :
      TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ }
    { l := some (ret (Γ := Γ) q), var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L) }
have succ : ∀ (n : ℕ)
  (IH :
    Reaches₀ (TM1.step (tr (Γ := Γ) M))
      { l := some (ret (Γ := Γ) q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom (Γ := Γ) L)) :
        TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ }
      { l := some (ret (Γ := Γ) q), var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L) }),
  Reaches₀ (TM1.step (tr (Γ := Γ) M))
    { l := some (ret (Γ := Γ) q), var := v, Tape := (Tape.move Dir.right)^[n + 1] (Tape.mk' ∅ (addBottom (Γ := Γ) L)) :
      TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ }
    { l := some (ret (Γ := Γ) q), var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L) }
Tactic: induction n with
  | zero => rfl
  | succ n IH =>
    refine Reaches₀.head ?_ IH
    simp only [Option.mem_def, TM1.step]
    rw [Option.some_inj, tr, TM1.stepAux, Tape.move_right_n_head, Tape.mk'_nth_nat,
      addBottom_nth_succ_fst, TM1.stepAux, iterate_succ', Function.comp_apply, Tape.move_right_left]
    rfl
Cleared hypotheses: n
-- 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
M : Λ → TM2.Stmt Γ Λ σ
q : TM2.Stmt Γ Λ σ
v : σ
T : ListBlank ((i : K) → Option (Γ i))
k : K
S : (k : K) → List (Γ k)
hT : ∀ (k : K), ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) T = ListBlank.mk (List.map some (S k)).reverse
o : StAct K Γ σ k
IH :
  ∀ {v : σ} {S : (k : K) → List (Γ k)} {T : ListBlank ((k : K) → Option (Γ k))},
    (∀ (k : K),
        ListBlank.map (proj (Γ := fun (i : K) ↦ Option (Γ i)) k) T = ListBlank.mk (List.map some (S k)).reverse) →
      ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
        TrCfg (Γ := Γ) (TM2.stepAux (Γ := Γ) q v S) b ∧
          Reaches (TM1.step (tr (Γ := Γ) M)) (TM1.stepAux (trNormal (Γ := Γ) q) v (Tape.mk' ∅ (addBottom (Γ := Γ) T))) b
⊢ ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
    TrCfg (Γ := Γ) (TM2.stepAux (Γ := Γ) (stRun (Γ := Γ) o q) v S) b ∧
      Reaches (TM1.step (tr (Γ := Γ) M))
        (TM1.stepAux (trNormal (Γ := Γ) (stRun (Γ := Γ) o q)) v (Tape.mk' ∅ (addBottom (Γ := Γ) T))) b
have simp : ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
  TrCfg (Γ := Γ)
      (TM2.stepAux (Γ := Γ) q (stVar (Γ := Γ) v (S k) o)
        (update (β := fun (k : K) ↦ List (Γ k)) S k (stWrite (Γ := Γ) v (S k) o)))
      b ∧
    Reaches (TM1.step (tr (Γ := Γ) M))
      (TM1.stepAux (goto fun (x : Γ' K Γ) (x_1 : σ) ↦ go (Γ := Γ) k o q) v (Tape.mk' ∅ (addBottom (Γ := Γ) T))) b
Tactic: simp only [trNormal_run, step_run]