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 : σ → Option (Γ k) → σ
e : S k = []
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'))
⊢ ∃ (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:
rw [← e, Function.update_eq_self]

Premises used: Function.update_eq_self
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
k : K
q : 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))
rw₁ rw₂ :
  TM1.stepAux q (f v none) (Tape.mk' ∅ (addBottom (Γ := Γ) L)) =
    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))

Tactic:
rw [addBottom_head_fst, cond]

Premises used: cond, Turing.TM2to1.addBottom_head_fst
-- 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 : σ → Option (Γ k) → σ
e : S 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) ∧
      (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:
exact ⟨L, hL, by rw [addBottom_head_fst, cond]⟩
-- 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 : σ → 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
rw₁ : getElem? (valid := fun (as : List (Γ k)) (i : ℕ) ↦ i < as.length) (tl.reverse ++ [hd]) tl.reverse.length = some hd
rw₂ rw₃ : some hd = some hd
⊢ getElem? (valid := fun (as : List (Γ k)) (i : ℕ) ↦ i < as.length) (hd :: tl).reverse tl.length = some hd

Tactic:
rw [List.reverse_cons, ← List.length_reverse, List.getElem?_concat_length]

Premises used: List.length_reverse, List.getElem?_concat_length, List.reverse_cons
-- 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 : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
pop :
  ∀ (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 none)
          tl.length L) =
      ListBlank.mk (List.map some (update (β := fun (a : K) ↦ List (Γ a)) S k (hd :: tl).tail 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 (hd :: tl).tail k_1)).reverse) ∧
      (bif ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L))).head.1 then
          TM1.stepAux q (f v none) ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))
        else
          TM1.stepAux q
            (f v
              ((Tape.move Dir.left
                      ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))).head.2
                k))
            (Tape.write
              ((Tape.move Dir.left
                      ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))).head.1,
                update (β := fun (k : K) ↦ Option (Γ k))
                  (Tape.move Dir.left
                        ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))).head.2
                  k none)
              (Tape.move Dir.left ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))))) =
        TM1.stepAux q (f v (hd :: tl).head?)
          ((Tape.move Dir.right)^[(hd :: tl).tail.length] (Tape.mk' ∅ (addBottom (Γ := Γ) L')))

Tactic:
refine
        ⟨_, fun k' ↦ ?_, by
          erw [List.length_cons, Tape.move_right_n_head, Tape.mk'_nth_nat, addBottom_nth_succ_fst,
            cond_false, iterate_succ', Function.comp, Tape.move_right_left, Tape.move_right_n_head,
            Tape.mk'_nth_nat, Tape.write_move_right_n fun a : Γ' K Γ ↦ (a.1, update a.2 k none),
            addBottom_modifyNth fun a ↦ update a k none, addBottom_nth_snd,
            stk_nth_val _ (hL k), e,
            show (List.cons hd tl).reverse[tl.length]? = some hd by
              rw [List.reverse_cons, ← List.length_reverse, List.getElem?_concat_length],
            List.head?, List.tail]⟩
-- 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 : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
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 none)
        tl.length L) =
    ListBlank.mk (List.map some (update (β := fun (a : K) ↦ List (Γ a)) S k (hd :: tl).tail 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 : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
k' : K
pop :
  ∀ (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 none)
              tl.length L)).nth
        i =
      ListBlank.nth
        (ListBlank.mk (List.map some (update (β := fun (a : K) ↦ List (Γ a)) S k (hd :: tl).tail 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 none)
        tl.length L) =
    ListBlank.mk (List.map some (update (β := fun (a : K) ↦ List (Γ a)) S k (hd :: tl).tail 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 : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
k' : K
i : ℕ
pop :
  (if i = tl.length then update (β := fun (k : K) ↦ Option (Γ k)) (L.nth i) k none else 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
⊢ (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 none)
            tl.length L)).nth
      i =
    ListBlank.nth (ListBlank.mk (List.map some (update (β := fun (a : K) ↦ List (Γ a)) S k (hd :: tl).tail 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 : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
k' : K
i : ℕ
pos :
  ∀ (h' : k' = k),
    (if i = tl.length then update (β := fun (k : K) ↦ Option (Γ k)) (L.nth i) k none else 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
neg :
  ∀ (h' : ¬k' = k),
    (if i = tl.length then update (β := fun (k : K) ↦ Option (Γ k)) (L.nth i) k none else 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
⊢ (if i = tl.length then update (β := fun (k : K) ↦ Option (Γ k)) (L.nth i) k none else 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

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 : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
k' : K
i : ℕ
h' : k' = k
pos :
  (if i = tl.length then update (β := fun (k : K) ↦ Option (Γ k)) (L.nth i) k none else 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
⊢ (if i = tl.length then update (β := fun (k : K) ↦ Option (Γ k)) (L.nth i) k none else 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

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 : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
pos :
  ∀ (h : i = tl.length),
    update (β := fun (k : K) ↦ Option (Γ k)) (L.nth i) k (none : Option (Γ k)) k =
      ListBlank.nth
        (ListBlank.mk (List.map some (update (β := fun (a : K) ↦ List (Γ a)) S k (hd :: tl).tail k)).reverse) i
neg :
  ∀ (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
⊢ (if i = tl.length then update (β := fun (k : K) ↦ Option (Γ k)) (L.nth i) k none else 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

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 : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h : i = tl.length
pos : none = (List.map some tl).reverse.getI i
⊢ update (β := fun (k : K) ↦ Option (Γ k)) (L.nth i) k (none : Option (Γ k)) k =
    ListBlank.nth (ListBlank.mk (List.map some (update (β := fun (a : K) ↦ List (Γ a)) S k (hd :: tl).tail k)).reverse)
      i

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

Premises used: List.tail, 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 : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h : ¬i = tl.length
neg : L.nth i k = (List.map some tl).reverse.getI 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

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

Premises used: List.tail, 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 : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h : i = tl.length
pos : Eq.{u_2 + 1} (α := Option (Γ k)) none default
pos₁ : (List.map some tl).reverse.length ≤ i
⊢ none = (List.map some tl).reverse.getI i

Tactic:
rw [List.getI_eq_default]

Premises used: List.getI_eq_default
-- 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 : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h : i = tl.length
⊢ Eq.{u_2 + 1} (α := Option (Γ k)) none default

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
k : K
q : 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
i : ℕ
h : i = tl.length
pos : (List.map some tl).reverse.length ≤ tl.length
pos₁ : (List.map some tl).length ≤ tl.length
pos₂ pos₃ : tl.length ≤ tl.length
⊢ (List.map some tl).reverse.length ≤ i

Tactic:
rw [h, List.length_reverse, List.length_map]

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 : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h : ¬i = tl.length
neg : ((List.map some tl).reverse ++ [some hd]).getI i = (List.map some tl).reverse.getI i
⊢ L.nth i k = (List.map some tl).reverse.getI i

Tactic:
rw [← proj_map_nth, hL, ListBlank.nth_mk, e, List.map, List.reverse_cons]

Premises used: List.map, List.reverse_cons, 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 : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h : ¬i = tl.length
neg : ∀ (h : i < tl.length), ((List.map some tl).reverse ++ [some hd]).getI i = (List.map some tl).reverse.getI i
neg₁ : ∀ (h : tl.length < i), ((List.map some tl).reverse ++ [some hd]).getI i = (List.map some tl).reverse.getI i
⊢ ((List.map some tl).reverse ++ [some hd]).getI i = (List.map some tl).reverse.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 : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h_1 : ¬i = tl.length
h : i < tl.length
neg : i < (List.map some tl).reverse.length
⊢ ((List.map some tl).reverse ++ [some hd]).getI i = (List.map some tl).reverse.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 : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h_1 : ¬i = tl.length
h : i < tl.length
⊢ i < (List.map some tl).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 : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h_1 : ¬i = tl.length
h : tl.length < i
neg : (List.map some tl).reverse.length ≤ i
neg₁ : ((List.map some tl).reverse ++ [some hd]).length ≤ i
⊢ ((List.map some tl).reverse ++ [some hd]).getI i = (List.map some tl).reverse.getI i

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

Premises used: List.getI_eq_default
-- 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 : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h_1 : ¬i = tl.length
h : tl.length < i
⊢ (List.map some tl).reverse.length ≤ i

Tactic:
simp only [Nat.add_one_le_iff, h, List.length, le_of_lt, List.length_reverse,
              List.length_append, List.length_map]

Premises used: List.length_reverse, le_of_lt, List.length_append, Nat.add_one_le_iff, List.length_map, List.length
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h_1 : ¬i = tl.length
h : tl.length < i
⊢ ((List.map some tl).reverse ++ [some hd]).length ≤ i

Tactic:
simp only [Nat.add_one_le_iff, h, List.length, le_of_lt, List.length_reverse,
              List.length_append, List.length_map]

Premises used: List.length_reverse, le_of_lt, List.length_append, Nat.add_one_le_iff, List.length_map, List.length