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

Premises used: Turing.ListBlank.ext
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (β := fun (k : K) ↦ Option (Γ k)) (R.nth n).2 k (some (f v)))
        ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n]
        (Tape.mk' L
          (ListBlank.modifyNth (fun (a : Γ' K Γ) ↦ (a.1, update (β := fun (k : K) ↦ Option (Γ k)) a.2 k (some (f v)))) n
            R))
k' : K
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
⊢ 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 ListBlank.ext fun i ↦ ?_

Premises used: Turing.ListBlank.ext
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (β := fun (k : K) ↦ Option (Γ k)) (R.nth n).2 k (some (f v)))
        ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n]
        (Tape.mk' L
          (ListBlank.modifyNth (fun (a : Γ' K Γ) ↦ (a.1, update (β := fun (k : K) ↦ Option (Γ k)) a.2 k (some (f v)))) n
            R))
k' : K
i : ℕ
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
⊢ (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:
rw [ListBlank.nth_map, ListBlank.nth_modifyNth, proj, PointedMap.mk_val]

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

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

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

Tactic:
simp only [List.reverse_cons, Function.update_self, ListBlank.nth_mk, List.map]

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

Tactic:
simp only [List.reverse_cons, Function.update_self, ListBlank.nth_mk, List.map]

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

Tactic:
rw [List.getI_eq_getElem _, List.getElem_append_right]

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

Tactic:
simp only [List.length_append, List.length_reverse, List.length_map, ← h,
          Nat.sub_self, List.length_singleton, List.getElem_singleton,
          le_refl, Nat.lt_succ_self]

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

Tactic:
simp only [List.length_append, List.length_reverse, List.length_map, ← h,
          Nat.sub_self, List.length_singleton, List.getElem_singleton,
          le_refl, Nat.lt_succ_self]

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

Tactic:
simp only [List.length_append, List.length_reverse, List.length_map, ← h,
          Nat.sub_self, List.length_singleton, List.getElem_singleton,
          le_refl, Nat.lt_succ_self]

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

Tactic:
rw [← proj_map_nth, hL, ListBlank.nth_mk]

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

Tactic:
rcases lt_or_gt_of_ne h with h | h

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

Tactic:
rw [List.getI_append]

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

Tactic:
simpa only [List.length_map, List.length_reverse] using h

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

Tactic:
rw [List.getI_eq_default, List.getI_eq_default]

Premises used: List.getI_eq_default