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 : 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 (Γ := Γ))
have revert : ∀ (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: revert h₂
Cleared hypotheses: 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 : Inhabited Λ
inst_1 : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports (Γ := Γ) M S
l₁ : Λ
p : σ → Bool
q₁' q₂' : Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ) (T : (k : K) → List (Γ k)) (h₂ : SupportsStmt (Γ := Γ) S q₁'),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
      ((stepAux (Γ := Γ) q₁' v T).l (Γ := Γ))
IH₂ :
  ∀ (v : σ) (T : (k : K) → List (Γ k)) (h₂ : SupportsStmt (Γ := Γ) S q₂'),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
      ((stepAux (Γ := Γ) q₂' v T).l (Γ := Γ))
v : σ
T : (k : K) → List (Γ k)
hs : SupportsStmt (Γ := Γ) S (branch (Γ := Γ) p q₁' q₂')
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
    ((bif p v then stepAux (Γ := Γ) q₁' v T else stepAux (Γ := Γ) q₂' v T).l (Γ := Γ))
have branch : Membership.mem (γ := Finset (Option Λ)) ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
  ((bif false then stepAux (Γ := Γ) q₁' v T else stepAux (Γ := Γ) q₂' v T).l (Γ := Γ))
Tactic: cases p v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : Inhabited Λ
inst_1 : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports (Γ := Γ) M S
l₁ : Λ
p : σ → Bool
q₁' q₂' : Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ) (T : (k : K) → List (Γ k)) (h₂ : SupportsStmt (Γ := Γ) S q₁'),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
      ((stepAux (Γ := Γ) q₁' v T).l (Γ := Γ))
IH₂ :
  ∀ (v : σ) (T : (k : K) → List (Γ k)) (h₂ : SupportsStmt (Γ := Γ) S q₂'),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
      ((stepAux (Γ := Γ) q₂' v T).l (Γ := Γ))
v : σ
T : (k : K) → List (Γ k)
hs : SupportsStmt (Γ := Γ) S (Stmt.branch (Γ := Γ) p q₁' q₂')
branch :
  Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
    ((bif false then stepAux (Γ := Γ) q₁' v T else stepAux (Γ := Γ) q₂' v T).l (Γ := Γ))
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
    ((bif p v then stepAux (Γ := Γ) q₁' v T else stepAux (Γ := Γ) q₂' v T).l (Γ := Γ))
have branch₁ : Membership.mem (γ := Finset (Option Λ)) ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
  ((bif true then stepAux (Γ := Γ) q₁' v T else stepAux (Γ := Γ) q₂' v T).l (Γ := Γ))
Tactic: cases p v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : 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 (Γ := Γ))
have 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 (Γ := Γ))
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
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
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
⊢ L.nth n k = getElem? (valid := fun (as : List (Γ k)) (i : ℕ) ↦ i < as.length) S.reverse n
have 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
Tactic: rw [← proj_map_nth, hL, ← List.map_reverse, ListBlank.nth_mk,
    List.getI_eq_getElem?_getD, List.getElem?_map]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
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
⊢ (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
have none : Eq.{u_2 + 1} (α := Option (Γ k)) (Option.getD (Option.map some none) default) none
Tactic: cases S.reverse[n]?
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
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
none : Eq.{u_2 + 1} (α := Option (Γ k)) (Option.getD (Option.map some Option.none) default) Option.none
⊢ (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
have some : ∀ (val : Γ k), (Option.map some (some val)).getD default = some val
Tactic: cases S.reverse[n]?
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
⊢ ListBlank.map { f := Prod.snd, map_pt' := ⋯ : PointedMap (Bool × ((k : K) → Option (Γ k))) ((k : K) → Option (Γ k)) }
      (addBottom (Γ := Γ) L) =
    L
have simp : ListBlank.cons L.head
    (ListBlank.map
      { f := Prod.snd, map_pt' := sorry : PointedMap (Bool × ((k : K) → Option (Γ k))) ((k : K) → Option (Γ k)) }
      (ListBlank.map { f := Prod.mk false, map_pt' := sorry : PointedMap ((k : K) → Option (Γ k)) (Γ' K Γ) } L.tail)) =
  L
Tactic: simp only [addBottom, ListBlank.map_cons]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
⊢ 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
have h : ListBlank.map { f := Prod.snd, map_pt' := sorry : PointedMap (Bool × ((k : K) → Option (Γ k))) ((k : K) → Option (Γ k)) }
    (ListBlank.map { f := Prod.mk false, map_pt' := sorry : PointedMap ((k : K) → Option (Γ k)) (Γ' K Γ) } L.tail) =
  L.tail
Tactic: convert! ListBlank.cons_head_tail L
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
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.tail) =
    L.tail
have h : ∀ (L' : ListBlank ((k : K) → Option (Γ k))),
  ListBlank.map { f := Prod.snd, map_pt' := sorry : PointedMap (Bool × ((k : K) → Option (Γ k))) ((k : K) → Option (Γ k)) }
      (ListBlank.map { f := Prod.mk false, map_pt' := sorry : PointedMap ((k : K) → Option (Γ k)) (Γ' K Γ) } L') =
    L'
Tactic: generalize ListBlank.tail L = L'
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
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'
have h : ∀ (l : List ((k : K) → Option (Γ k))),
  ListBlank.map { f := Prod.snd, map_pt' := sorry : PointedMap (Bool × ((k : K) → Option (Γ k))) ((k : K) → Option (Γ k)) }
      (ListBlank.map { f := Prod.mk false, map_pt' := sorry : PointedMap ((k : K) → Option (Γ k)) (Γ' K Γ) }
        (ListBlank.mk l)) =
    ListBlank.mk l
Tactic: refine L'.induction_on fun l ↦ ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
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 : ℕ
⊢ ListBlank.modifyNth (fun (a : Bool × ((k : K) → Option (Γ k))) ↦ (a.1, f a.2)) n (addBottom (Γ := Γ) L) =
    addBottom (Γ := Γ) (ListBlank.modifyNth f n L)
have zero : ListBlank.modifyNth (fun (a : Bool × ((k : K) → Option (Γ k))) ↦ (a.1, f a.2)) 0 (addBottom (Γ := Γ) L) =
  addBottom (Γ := Γ) (ListBlank.modifyNth f 0 L)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
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)
⊢ ListBlank.modifyNth (fun (a : Bool × ((k : K) → Option (Γ k))) ↦ (a.1, f a.2)) n (addBottom (Γ := Γ) L) =
    addBottom (Γ := Γ) (ListBlank.modifyNth f n L)
have 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)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
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 : ℕ
⊢ 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)
have 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' := sorry } L.tail)))
  (ListBlank.cons (true, L.head) (ListBlank.map { f := Prod.mk false, map_pt' := sorry } (ListBlank.modifyNth f n L.tail)))
Tactic: simp only [addBottom, ListBlank.head_cons, ListBlank.modifyNth, ListBlank.tail_cons]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
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 : ℕ
⊢ 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)))
have 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' := sorry } L.tail))
  (ListBlank.map { f := Prod.mk false, map_pt' := sorry } (ListBlank.modifyNth f n L.tail))
Tactic: congr
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
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 : ℕ
⊢ 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))
have succ : Eq (α := ListBlank (Bool × ((k : K) → Option (Γ k))))
  (ListBlank.map { f := Prod.mk false, map_pt' := sorry } (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' := sorry } L.tail))
Tactic: symm
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
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 : ℕ
⊢ 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))
have succ : ∀ (x : (k : K) → Option (Γ k)),
  PointedMap.f { f := Prod.mk false, map_pt' := sorry : PointedMap ((k : K) → Option (Γ k)) (Γ' K Γ) } (f x) =
    ((PointedMap.f { f := Prod.mk false, map_pt' := sorry : PointedMap ((k : K) → Option (Γ k)) (Γ' K Γ) } x).1,
      f (PointedMap.f { f := Prod.mk false, map_pt' := sorry : PointedMap ((k : K) → Option (Γ k)) (Γ' K Γ) } x).2)
Tactic: apply ListBlank.map_modifyNth
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
| ((addBottom (Γ := Γ) L).nth n).2 = L.nth n
have rhs : L.nth n
Tactic: rhs
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
| L.nth n
have rw : PointedMap.f { f := Prod.snd, map_pt' := sorry : PointedMap (Bool × ((k : K) → Option (Γ k))) ((k : K) → Option (Γ k)) }
  ((addBottom (Γ := Γ) L).nth n)
Tactic: rw [← addBottom_map L, ListBlank.nth_map]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
| ((addBottom (Γ := Γ) L).nth n).2 = L.nth n
have rw : PointedMap.f { f := Prod.snd, map_pt' := sorry : PointedMap (Bool × ((k : K) → Option (Γ k))) ((k : K) → Option (Γ k)) }
  ((addBottom (Γ := Γ) L).nth n)
Tactic: rhs; rw [← addBottom_map L, ListBlank.nth_map]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
⊢ ((addBottom (Γ := Γ) L).nth n).2 = L.nth n
have conv : ((addBottom (Γ := Γ) L).nth n).2 = L.nth n
Tactic: conv => rhs; rw [← addBottom_map L, ListBlank.nth_map]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
conv : ((addBottom (Γ := Γ) L).nth n).2 = L.nth n
⊢ ((addBottom (Γ := Γ) L).nth n).2 = L.nth n
have conv₁ : ((addBottom (Γ := Γ) L).nth n).2 =
  PointedMap.f { f := Prod.snd, map_pt' := sorry : PointedMap (Bool × ((k : K) → Option (Γ k))) ((k : K) → Option (Γ k)) }
    ((addBottom (Γ := Γ) L).nth n)
Tactic: conv => rhs; rw [← addBottom_map L, ListBlank.nth_map]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
⊢ ((addBottom (Γ := Γ) L).nth (n + 1)).1 = false
have rw : ((addBottom (Γ := Γ) L).tail.nth n).1 = false
Tactic: rw [ListBlank.nth_succ, addBottom, ListBlank.tail_cons, ListBlank.nth_map]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
rw : ((addBottom (Γ := Γ) L).tail.nth n).1 = false
⊢ ((addBottom (Γ := Γ) L).nth (n + 1)).1 = false
have rw₁ : (ListBlank.nth
      (ListBlank.tail
        (ListBlank.cons (true, L.head)
          (ListBlank.map { f := Prod.mk false, map_pt' := sorry : PointedMap ((k : K) → Option (Γ k)) (Γ' K Γ) } L.tail)))
      n).1 =
  false
Tactic: rw [ListBlank.nth_succ, addBottom, ListBlank.tail_cons, ListBlank.nth_map]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
rw : ((addBottom (Γ := Γ) L).tail.nth n).1 = false
rw₁ :
  (ListBlank.nth
        (ListBlank.tail
          (ListBlank.cons (true, L.head)
            (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ : PointedMap ((k : K) → Option (Γ k)) (Γ' K Γ) } L.tail)))
        n).1 =
    false
⊢ ((addBottom (Γ := Γ) L).nth (n + 1)).1 = false
have rw₂ : (ListBlank.nth
      (ListBlank.map { f := Prod.mk false, map_pt' := sorry : PointedMap ((k : K) → Option (Γ k)) (Γ' K Γ) } L.tail) n).1 =
  false
Tactic: rw [ListBlank.nth_succ, addBottom, ListBlank.tail_cons, ListBlank.nth_map]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
rw : ((addBottom (Γ := Γ) L).tail.nth n).1 = false
rw₁ :
  (ListBlank.nth
        (ListBlank.tail
          (ListBlank.cons (true, L.head)
            (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ : PointedMap ((k : K) → Option (Γ k)) (Γ' K Γ) } L.tail)))
        n).1 =
    false
rw₂ :
  (ListBlank.nth
        (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ : PointedMap ((k : K) → Option (Γ k)) (Γ' K Γ) } L.tail)
        n).1 =
    false
⊢ ((addBottom (Γ := Γ) L).nth (n + 1)).1 = false
have rw₃ : (PointedMap.f { f := Prod.mk false, map_pt' := sorry : PointedMap ((k : K) → Option (Γ k)) (Γ' K Γ) } (L.tail.nth n)).1 =
  false
Tactic: rw [ListBlank.nth_succ, addBottom, ListBlank.tail_cons, ListBlank.nth_map]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
⊢ (addBottom (Γ := Γ) L).head.1 = true
have rw : (ListBlank.head
      (ListBlank.cons (true, L.head)
        (ListBlank.map { f := Prod.mk false, map_pt' := sorry : PointedMap ((k : K) → Option (Γ k)) (Γ' K Γ) } L.tail))).1 =
  true
Tactic: rw [addBottom, ListBlank.head_cons]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
rw :
  (ListBlank.head
        (ListBlank.cons (true, L.head)
          (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ : PointedMap ((k : K) → Option (Γ k)) (Γ' K Γ) }
            L.tail))).1 =
    true
⊢ (addBottom (Γ := Γ) L).head.1 = true
have rw₁ : (true, L.head).1 = true
Tactic: rw [addBottom, ListBlank.head_cons]
-- 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
S : Finset Λ
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
⊢ TM2.SupportsStmt (Γ := Γ) S (stRun (Γ := Γ) s q) ↔ TM2.SupportsStmt (Γ := Γ) S q
have push : ∀ (a : σ → Γ k), TM2.SupportsStmt (Γ := Γ) S (stRun (Γ := Γ) (push (Γ := Γ) a) q) ↔ TM2.SupportsStmt (Γ := Γ) S q
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
push :
  ∀ (a : σ → Γ k),
    TM2.SupportsStmt (Γ := Γ) S (stRun (Γ := Γ) (StAct.push (Γ := Γ) a) q) ↔ TM2.SupportsStmt (Γ := Γ) S q
⊢ TM2.SupportsStmt (Γ := Γ) S (stRun (Γ := Γ) s q) ↔ TM2.SupportsStmt (Γ := Γ) S q
have peek : ∀ (a : σ → Option (Γ k) → σ),
  TM2.SupportsStmt (Γ := Γ) S (stRun (Γ := Γ) (peek (Γ := Γ) a) q) ↔ TM2.SupportsStmt (Γ := Γ) S q
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
push :
  ∀ (a : σ → Γ k),
    TM2.SupportsStmt (Γ := Γ) S (stRun (Γ := Γ) (StAct.push (Γ := Γ) a) q) ↔ TM2.SupportsStmt (Γ := Γ) S q
peek :
  ∀ (a : σ → Option (Γ k) → σ),
    TM2.SupportsStmt (Γ := Γ) S (stRun (Γ := Γ) (StAct.peek (Γ := Γ) a) q) ↔ TM2.SupportsStmt (Γ := Γ) S q
⊢ TM2.SupportsStmt (Γ := Γ) S (stRun (Γ := Γ) s q) ↔ TM2.SupportsStmt (Γ := Γ) S q
have pop : ∀ (a : σ → Option (Γ k) → σ),
  TM2.SupportsStmt (Γ := Γ) S (stRun (Γ := Γ) (pop (Γ := Γ) a) q) ↔ TM2.SupportsStmt (Γ := Γ) S q
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
k : K
q : TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
f : σ → Option (Γ k) → σ
⊢ TM2.stepAux (Γ := Γ) (stRun (Γ := Γ) (StAct.peek (Γ := Γ) f) q) v S =
    TM2.stepAux (Γ := Γ) q (stVar (Γ := Γ) v (S k) (StAct.peek (Γ := Γ) f))
      (update (β := fun (k : K) ↦ List (Γ k)) S k (stWrite (Γ := Γ) v (S k) (StAct.peek (Γ := Γ) f)))
have unfold : TM2.stepAux (Γ := Γ) (stRun (Γ := Γ) (StAct.peek (Γ := Γ) f) q) v S =
  TM2.stepAux (Γ := Γ) q (stVar (Γ := Γ) v (S k) (StAct.peek (Γ := Γ) f))
    (update (β := fun (k : K) ↦ List (Γ k)) S k
      (match (motive := StAct K Γ σ k → List (Γ k)) StAct.peek (Γ := Γ) f with
      | StAct.push f => f v :: S k
      | StAct.peek a => S k
      | StAct.pop a => (S k).tail))
Tactic: unfold stWrite
-- 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 : TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
f : σ → Option (Γ k) → σ
⊢ TM2.stepAux (Γ := Γ) (stRun (Γ := Γ) (StAct.peek (Γ := Γ) f) q) v S =
    TM2.stepAux (Γ := Γ) q (stVar (Γ := Γ) v (S k) (StAct.peek (Γ := Γ) f))
      (update (β := fun (k : K) ↦ List (Γ k)) S k
        (match (motive := StAct K Γ σ k → List (Γ k)) StAct.peek (Γ := Γ) f with
        | StAct.push f => f v :: S k
        | StAct.peek a => S k
        | StAct.pop a => (S k).tail))
have rw : TM2.stepAux (Γ := Γ) (stRun (Γ := Γ) (StAct.peek (Γ := Γ) f) q) v S =
  TM2.stepAux (Γ := Γ) q (stVar (Γ := Γ) v (S k) (StAct.peek (Γ := Γ) f)) S
Tactic: rw [Function.update_eq_self]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
⊢ trNormal (Γ := Γ) (stRun (Γ := Γ) s q) = goto fun (x : Γ' K Γ) (x_1 : σ) ↦ go (Γ := Γ) k s q
have push : ∀ (a : σ → Γ k),
  trNormal (Γ := Γ) (stRun (Γ := Γ) (StAct.push (Γ := Γ) a) q) =
    goto fun (x : Γ' K Γ) (x_1 : σ) ↦ go (Γ := Γ) k (StAct.push (Γ := Γ) a) q
Tactic: cases s
Cleared hypotheses: s