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 : Inhabited Λ
inst_1 : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports (Γ := Γ) M S
l₁ : Λ
a : σ → Λ
v : σ
T : (k : K) → List (Γ k)
hs : SupportsStmt (Γ := Γ) S (goto (Γ := Γ) a)
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
    ((stepAux (Γ := Γ) (goto (Γ := Γ) a) v T).l (Γ := Γ))

Tactic:
Finset.some_mem_insertNone.2 (hs _)

Premises used: Iff.mpr, Set.Mem, setOf, Finset.some_mem_insertNone
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : Inhabited Λ
inst_1 : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports (Γ := Γ) M S
l₁ : Λ
a : σ → Λ
v : σ
T : (k : K) → List (Γ k)
hs : SupportsStmt (Γ := Γ) S (goto (Γ := Γ) a)
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
    ((stepAux (Γ := Γ) (goto (Γ := Γ) a) v T).l (Γ := Γ))

Tactic:
exact Finset.some_mem_insertNone.2 (hs _)

Premises used: Iff.mpr, Finset.some_mem_insertNone
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : Inhabited Λ
inst_1 : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports (Γ := Γ) M S
l₁ : Λ
v : σ
T : (k : K) → List (Γ k)
hs : SupportsStmt.{u_1, u_2, u_3, u_4} (Γ := Γ) (σ := σ) S (halt (Γ := Γ))
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
    (Cfg.l (Γ := Γ) (stepAux (Γ := Γ) (halt (Γ := Γ)) v T))

Tactic:
apply Multiset.mem_cons_self

Premises used: Multiset.mem_cons_self
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : Inhabited Λ
inst_1 : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports (Γ := Γ) M S
l₁ : Λ
a : σ → σ
a_1 : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (T : (k : K) → List (Γ k)) (h₂ : SupportsStmt (Γ := Γ) S a_1),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
      ((stepAux (Γ := Γ) a_1 v T).l (Γ := Γ))
v : σ
T : (k : K) → List (Γ k)
hs : SupportsStmt (Γ := Γ) S (load (Γ := Γ) a a_1)
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
    ((stepAux (Γ := Γ) (load (Γ := Γ) a a_1) v T).l (Γ := Γ))

Tactic:
IH _ _ hs

Premises used: Set.Mem, setOf
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : Inhabited Λ
inst_1 : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports (Γ := Γ) M S
l₁ : Λ
a : σ → σ
a_1 : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (T : (k : K) → List (Γ k)) (h₂ : SupportsStmt (Γ := Γ) S a_1),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
      ((stepAux (Γ := Γ) a_1 v T).l (Γ := Γ))
v : σ
T : (k : K) → List (Γ k)
hs : SupportsStmt (Γ := Γ) S (load (Γ := Γ) a a_1)
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
    ((stepAux (Γ := Γ) (load (Γ := Γ) a a_1) v T).l (Γ := Γ))

Tactic:
exact IH _ _ hs
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : Inhabited Λ
inst_1 : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports (Γ := Γ) M S
l₁ : Λ
k : K
a : σ → Γ k
a_1 : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (T : (k : K) → List (Γ k)) (h₂ : SupportsStmt (Γ := Γ) S a_1),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
      ((stepAux (Γ := Γ) a_1 v T).l (Γ := Γ))
v : σ
T : (k : K) → List (Γ k)
hs : SupportsStmt (Γ := Γ) S (push (Γ := Γ) k a a_1)
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
    ((stepAux (Γ := Γ) (push (Γ := Γ) k a a_1) v T).l (Γ := Γ))

Tactic:
IH _ _ hs

Premises used: Set.Mem, setOf
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : Inhabited Λ
inst_1 : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports (Γ := Γ) M S
l₁ : Λ
k : K
a : σ → Γ k
a_1 : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (T : (k : K) → List (Γ k)) (h₂ : SupportsStmt (Γ := Γ) S a_1),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
      ((stepAux (Γ := Γ) a_1 v T).l (Γ := Γ))
v : σ
T : (k : K) → List (Γ k)
hs : SupportsStmt (Γ := Γ) S (push (Γ := Γ) k a a_1)
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
    ((stepAux (Γ := Γ) (push (Γ := Γ) k a a_1) v T).l (Γ := Γ))

Tactic:
exact IH _ _ hs
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : Inhabited Λ
inst_1 : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports (Γ := Γ) M S
l₁ : Λ
k : K
a : σ → Option (Γ k) → σ
a_1 : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (T : (k : K) → List (Γ k)) (h₂ : SupportsStmt (Γ := Γ) S a_1),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
      ((stepAux (Γ := Γ) a_1 v T).l (Γ := Γ))
v : σ
T : (k : K) → List (Γ k)
hs : SupportsStmt (Γ := Γ) S (peek (Γ := Γ) k a a_1)
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
    ((stepAux (Γ := Γ) (peek (Γ := Γ) k a a_1) v T).l (Γ := Γ))

Tactic:
IH _ _ hs

Premises used: Set.Mem, setOf
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : Inhabited Λ
inst_1 : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports (Γ := Γ) M S
l₁ : Λ
k : K
a : σ → Option (Γ k) → σ
a_1 : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (T : (k : K) → List (Γ k)) (h₂ : SupportsStmt (Γ := Γ) S a_1),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
      ((stepAux (Γ := Γ) a_1 v T).l (Γ := Γ))
v : σ
T : (k : K) → List (Γ k)
hs : SupportsStmt (Γ := Γ) S (peek (Γ := Γ) k a a_1)
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
    ((stepAux (Γ := Γ) (peek (Γ := Γ) k a a_1) v T).l (Γ := Γ))

Tactic:
exact IH _ _ hs
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : Inhabited Λ
inst_1 : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports (Γ := Γ) M S
l₁ : Λ
k : K
a : σ → Option (Γ k) → σ
a_1 : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (T : (k : K) → List (Γ k)) (h₂ : SupportsStmt (Γ := Γ) S a_1),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
      ((stepAux (Γ := Γ) a_1 v T).l (Γ := Γ))
v : σ
T : (k : K) → List (Γ k)
hs : SupportsStmt (Γ := Γ) S (pop (Γ := Γ) k a a_1)
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
    ((stepAux (Γ := Γ) (pop (Γ := Γ) k a a_1) v T).l (Γ := Γ))

Tactic:
IH _ _ hs

Premises used: Set.Mem, setOf
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : Inhabited Λ
inst_1 : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports (Γ := Γ) M S
l₁ : Λ
k : K
a : σ → Option (Γ k) → σ
a_1 : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (T : (k : K) → List (Γ k)) (h₂ : SupportsStmt (Γ := Γ) S a_1),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
      ((stepAux (Γ := Γ) a_1 v T).l (Γ := Γ))
v : σ
T : (k : K) → List (Γ k)
hs : SupportsStmt (Γ := Γ) S (pop (Γ := Γ) k a a_1)
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
    ((stepAux (Γ := Γ) (pop (Γ := Γ) k a a_1) v T).l (Γ := Γ))

Tactic:
exact IH _ _ hs
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : Inhabited Λ
inst_1 : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports (Γ := Γ) M S
l₁ : Λ
v : σ
T : (k : K) → List (Γ k)
induction :
  ∀ (x : Stmt Γ Λ σ) (h₂ : SupportsStmt (Γ := Γ) S x),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
      ((stepAux (Γ := Γ) x v T).l (Γ := Γ))
⊢ ∀ (h₂ : SupportsStmt (Γ := Γ) S (M l₁)),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
      ((stepAux (Γ := Γ) (M l₁) v T).l (Γ := Γ))

Tactic:
induction M l₁ generalizing v T with intro hs
    | branch p q₁' q₂' IH₁ IH₂ =>
      unfold stepAux; cases p v
      · exact IH₂ _ _ hs.2
      · exact IH₁ _ _ hs.1
    | goto => exact Finset.some_mem_insertNone.2 (hs _)
    | halt => apply Multiset.mem_cons_self
    | load _ _ IH | _ _ _ _ IH => exact IH _ _ hs

Premises used: Turing.TM2.stepAux, Turing.TM2.Stmt.branch, Turing.TM2.Stmt.load, Turing.TM2.Stmt.goto, Turing.TM2.Stmt.halt, Multiset.mem_cons_self
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : Inhabited Λ
inst_1 : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports (Γ := Γ) M S
l₁ : Λ
v : σ
T : (k : K) → List (Γ k)
⊢ ∀ (h₂ : SupportsStmt (Γ := Γ) S (M l₁)),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
      ((stepAux (Γ := Γ) (M l₁) v T).l (Γ := Γ))

Tactic:
induction M l₁ generalizing v T with intro hs
    | branch p q₁' q₂' IH₁ IH₂ =>
      unfold stepAux; cases p v
      · exact IH₂ _ _ hs.2
      · exact IH₁ _ _ hs.1
    | goto => exact Finset.some_mem_insertNone.2 (hs _)
    | halt => apply Multiset.mem_cons_self
    | load _ _ IH | _ _ _ _ IH => exact IH _ _ hs

Premises used: Turing.TM2.stepAux, Turing.TM2.Stmt.branch, Turing.TM2.Stmt.load, Turing.TM2.Stmt.goto, Turing.TM2.Stmt.halt, Multiset.mem_cons_self
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
k : K
S : List (Γ k)
n : ℕ
hL : ListBlank.map (proj (Γ := fun (i : K) ↦ Option (Γ i)) k) L = ListBlank.mk (List.map some S).reverse
rw :
  (Option.map some (getElem? (valid := fun (as : List (Γ k)) (i : ℕ) ↦ i < as.length) S.reverse n)).getD default =
    getElem? (valid := fun (as : List (Γ k)) (i : ℕ) ↦ i < as.length) S.reverse n
⊢ L.nth n k = getElem? (valid := fun (as : List (Γ k)) (i : ℕ) ↦ i < as.length) S.reverse n

Tactic:
rw [← proj_map_nth, hL, ← List.map_reverse, ListBlank.nth_mk,
    List.getI_eq_getElem?_getD, List.getElem?_map]

Premises used: List.getElem?_map, List.getI_eq_getElem?_getD, List.map_reverse, Turing.ListBlank.nth_mk, Turing.proj_map_nth
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
k : K
S : List (Γ k)
n : ℕ
hL : ListBlank.map (proj (Γ := fun (i : K) ↦ Option (Γ i)) k) L = ListBlank.mk (List.map Option.some S).reverse
none : Eq.{u_2 + 1} (α := Option (Γ k)) (Option.getD (Option.map Option.some Option.none) default) Option.none
some : ∀ (val : Γ k), (Option.map Option.some (Option.some val)).getD default = Option.some val
⊢ (Option.map Option.some (getElem? (valid := fun (as : List (Γ k)) (i : ℕ) ↦ i < as.length) S.reverse n)).getD
      default =
    getElem? (valid := fun (as : List (Γ k)) (i : ℕ) ↦ i < as.length) S.reverse n

Tactic:
cases S.reverse[n]?

Premises used: List.reverse
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
k : K
S : List (Γ k)
n : ℕ
hL : ListBlank.map (proj (Γ := fun (i : K) ↦ Option (Γ i)) k) L = ListBlank.mk (List.map some S).reverse
⊢ Eq.{u_2 + 1} (α := Option (Γ k)) (Option.getD (Option.map some none) default) none

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
k : K
S : List (Γ k)
n : ℕ
hL : ListBlank.map (proj (Γ := fun (i : K) ↦ Option (Γ i)) k) L = ListBlank.mk (List.map some S).reverse
val : Γ k
⊢ (Option.map some (some val)).getD default = some val

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
L : ListBlank ((k : K) → Option (Γ k))
⊢ Eq (α := (k : K) → Option (Γ k)) default.2 default

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
simp :
  ListBlank.cons L.head
      (ListBlank.map
        { f := Prod.snd, map_pt' := ⋯ : PointedMap (Bool × ((k : K) → Option (Γ k))) ((k : K) → Option (Γ k)) }
        (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ : PointedMap ((k : K) → Option (Γ k)) (Γ' K Γ) } L.tail)) =
    L
⊢ ListBlank.map { f := Prod.snd, map_pt' := ⋯ : PointedMap (Bool × ((k : K) → Option (Γ k))) ((k : K) → Option (Γ k)) }
      (addBottom (Γ := Γ) L) =
    L

Tactic:
simp only [addBottom, ListBlank.map_cons]

Premises used: Turing.TM2to1.addBottom, Turing.ListBlank.map_cons
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
⊢ ListBlank.cons L.head L.tail = L

Tactic:
ListBlank.cons_head_tail L

Premises used: Turing.ListBlank.cons_head_tail
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
h :
  ListBlank.map { f := Prod.snd, map_pt' := ⋯ : PointedMap (Bool × ((k : K) → Option (Γ k))) ((k : K) → Option (Γ k)) }
      (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ : PointedMap ((k : K) → Option (Γ k)) (Γ' K Γ) } L.tail) =
    L.tail
⊢ ListBlank.cons L.head
      (ListBlank.map
        { f := Prod.snd, map_pt' := ⋯ : PointedMap (Bool × ((k : K) → Option (Γ k))) ((k : K) → Option (Γ k)) }
        (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ : PointedMap ((k : K) → Option (Γ k)) (Γ' K Γ) } L.tail)) =
    L

Tactic:
convert! ListBlank.cons_head_tail L

Premises used: Turing.ListBlank.cons_head_tail
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
h :
  ∀ (L' : ListBlank ((k : K) → Option (Γ k))),
    ListBlank.map
        { f := Prod.snd, map_pt' := ⋯ : PointedMap (Bool × ((k : K) → Option (Γ k))) ((k : K) → Option (Γ k)) }
        (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ : PointedMap ((k : K) → Option (Γ k)) (Γ' K Γ) } L') =
      L'
⊢ ListBlank.map { f := Prod.snd, map_pt' := ⋯ : PointedMap (Bool × ((k : K) → Option (Γ k))) ((k : K) → Option (Γ k)) }
      (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ : PointedMap ((k : K) → Option (Γ k)) (Γ' K Γ) } L.tail) =
    L.tail

Tactic:
generalize ListBlank.tail L = L'

Premises used: Turing.ListBlank.tail
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
L L' : ListBlank ((k : K) → Option (Γ k))
⊢ ListBlank.map { f := Prod.snd, map_pt' := ⋯ : PointedMap (Bool × ((k : K) → Option (Γ k))) ((k : K) → Option (Γ k)) }
      (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ : PointedMap ((k : K) → Option (Γ k)) (Γ' K Γ) } L') =
    L'

Tactic:
L'.induction_on fun l ↦ ?_

Premises used: Turing.ListBlank.induction_on
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
L L' : ListBlank ((k : K) → Option (Γ k))
h :
  ∀ (l : List ((k : K) → Option (Γ k))),
    ListBlank.map
        { f := Prod.snd, map_pt' := ⋯ : PointedMap (Bool × ((k : K) → Option (Γ k))) ((k : K) → Option (Γ k)) }
        (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ : PointedMap ((k : K) → Option (Γ k)) (Γ' K Γ) }
          (ListBlank.mk l)) =
      ListBlank.mk l
⊢ ListBlank.map { f := Prod.snd, map_pt' := ⋯ : PointedMap (Bool × ((k : K) → Option (Γ k))) ((k : K) → Option (Γ k)) }
      (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ : PointedMap ((k : K) → Option (Γ k)) (Γ' K Γ) } L') =
    L'

Tactic:
refine L'.induction_on fun l ↦ ?_
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
L L' : ListBlank ((k : K) → Option (Γ k))
l : List ((k : K) → Option (Γ k))
⊢ ListBlank.map { f := Prod.snd, map_pt' := ⋯ : PointedMap (Bool × ((k : K) → Option (Γ k))) ((k : K) → Option (Γ k)) }
      (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ : PointedMap ((k : K) → Option (Γ k)) (Γ' K Γ) }
        (ListBlank.mk l)) =
    ListBlank.mk l

Tactic:
simp
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
zero :
  ListBlank.modifyNth (fun (a : Bool × ((k : K) → Option (Γ k))) ↦ (a.1, f a.2)) 0 (addBottom (Γ := Γ) L) =
    addBottom (Γ := Γ) (ListBlank.modifyNth f 0 L)
succ :
  ∀ (n : ℕ),
    ListBlank.modifyNth (fun (a : Bool × ((k : K) → Option (Γ k))) ↦ (a.1, f a.2)) (n + 1) (addBottom (Γ := Γ) L) =
      addBottom (Γ := Γ) (ListBlank.modifyNth f (n + 1) L)
⊢ ListBlank.modifyNth (fun (a : Bool × ((k : K) → Option (Γ k))) ↦ (a.1, f a.2)) n (addBottom (Γ := Γ) L) =
    addBottom (Γ := Γ) (ListBlank.modifyNth f n L)

Tactic:
cases n
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
⊢ ListBlank.modifyNth (fun (a : Bool × ((k : K) → Option (Γ k))) ↦ (a.1, f a.2)) 0 (addBottom (Γ := Γ) L) =
    addBottom (Γ := Γ) (ListBlank.modifyNth f 0 L)

Tactic:
simp only [addBottom, ListBlank.head_cons, ListBlank.modifyNth, ListBlank.tail_cons]

Premises used: Turing.TM2to1.addBottom, Turing.ListBlank.modifyNth, Turing.ListBlank.head_cons, Turing.ListBlank.tail_cons
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
succ :
  Eq (α := ListBlank (Bool × ((k : K) → Option (Γ k))))
    (ListBlank.cons (true, L.head)
      (ListBlank.modifyNth (fun (a : Bool × ((k : K) → Option (Γ k))) ↦ (a.1, f a.2)) n
        (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } L.tail)))
    (ListBlank.cons (true, L.head)
      (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } (ListBlank.modifyNth f n L.tail)))
⊢ ListBlank.modifyNth (fun (a : Bool × ((k : K) → Option (Γ k))) ↦ (a.1, f a.2)) (n + 1) (addBottom (Γ := Γ) L) =
    addBottom (Γ := Γ) (ListBlank.modifyNth f (n + 1) L)

Tactic:
simp only [addBottom, ListBlank.head_cons, ListBlank.modifyNth, ListBlank.tail_cons]

Premises used: Turing.TM2to1.addBottom, Turing.ListBlank.modifyNth, Turing.ListBlank.head_cons, Turing.ListBlank.tail_cons
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
succ :
  Eq (α := ListBlank (Bool × ((k : K) → Option (Γ k))))
    (ListBlank.modifyNth (fun (a : Bool × ((k : K) → Option (Γ k))) ↦ (a.1, f a.2)) n
      (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } L.tail))
    (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } (ListBlank.modifyNth f n L.tail))
⊢ Eq (α := ListBlank (Bool × ((k : K) → Option (Γ k))))
    (ListBlank.cons (true, L.head)
      (ListBlank.modifyNth (fun (a : Bool × ((k : K) → Option (Γ k))) ↦ (a.1, f a.2)) n
        (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } L.tail)))
    (ListBlank.cons (true, L.head)
      (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } (ListBlank.modifyNth f n L.tail)))

Tactic:
congr
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
succ :
  Eq (α := ListBlank (Bool × ((k : K) → Option (Γ k))))
    (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } (ListBlank.modifyNth f n L.tail))
    (ListBlank.modifyNth (fun (a : Bool × ((k : K) → Option (Γ k))) ↦ (a.1, f a.2)) n
      (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } L.tail))
⊢ Eq (α := ListBlank (Bool × ((k : K) → Option (Γ k))))
    (ListBlank.modifyNth (fun (a : Bool × ((k : K) → Option (Γ k))) ↦ (a.1, f a.2)) n
      (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } L.tail))
    (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } (ListBlank.modifyNth f n L.tail))

Tactic:
symm
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
succ :
  ∀ (x : (k : K) → Option (Γ k)),
    PointedMap.f { f := Prod.mk false, map_pt' := ⋯ : PointedMap ((k : K) → Option (Γ k)) (Γ' K Γ) } (f x) =
      ((PointedMap.f { f := Prod.mk false, map_pt' := ⋯ : PointedMap ((k : K) → Option (Γ k)) (Γ' K Γ) } x).1,
        f (PointedMap.f { f := Prod.mk false, map_pt' := ⋯ : PointedMap ((k : K) → Option (Γ k)) (Γ' K Γ) } x).2)
⊢ Eq (α := ListBlank (Bool × ((k : K) → Option (Γ k))))
    (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } (ListBlank.modifyNth f n L.tail))
    (ListBlank.modifyNth (fun (a : Bool × ((k : K) → Option (Γ k))) ↦ (a.1, f a.2)) n
      (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } L.tail))

Tactic:
apply ListBlank.map_modifyNth

Premises used: Turing.ListBlank.map_modifyNth
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
x : (k : K) → Option (Γ k)
⊢ PointedMap.f { f := Prod.mk false, map_pt' := ⋯ : PointedMap ((k : K) → Option (Γ k)) (Γ' K Γ) } (f x) =
    ((PointedMap.f { f := Prod.mk false, map_pt' := ⋯ : PointedMap ((k : K) → Option (Γ k)) (Γ' K Γ) } x).1,
      f (PointedMap.f { f := Prod.mk false, map_pt' := ⋯ : PointedMap ((k : K) → Option (Γ k)) (Γ' K Γ) } x).2)

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
rhs : L.nth n
| ((addBottom (Γ := Γ) L).nth n).2 = L.nth n

Tactic:
rhs
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
rw :
  PointedMap.f { f := Prod.snd, map_pt' := ⋯ : PointedMap (Bool × ((k : K) → Option (Γ k))) ((k : K) → Option (Γ k)) }
    ((addBottom (Γ := Γ) L).nth n)
| L.nth n

Tactic:
rw [← addBottom_map L, ListBlank.nth_map]

Premises used: Turing.TM2to1.addBottom_map, Turing.ListBlank.nth_map
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
rw :
  PointedMap.f { f := Prod.snd, map_pt' := ⋯ : PointedMap (Bool × ((k : K) → Option (Γ k))) ((k : K) → Option (Γ k)) }
    ((addBottom (Γ := Γ) L).nth n)
| ((addBottom (Γ := Γ) L).nth n).2 = L.nth n

Tactic:
rhs; rw [← addBottom_map L, ListBlank.nth_map]

Premises used: Turing.TM2to1.addBottom_map, Turing.ListBlank.nth_map