-- 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) → σ
pop :
  ∀ (e : S k = []),
    ∃ (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.tail [] : List (Γ k)) k_1)).reverse) ∧
        (bif ((Tape.move Dir.right)^[List.length.{u_2} (α := Γ k) []] (Tape.mk' ∅ (addBottom (Γ := Γ) L))).head.1 then
            TM1.stepAux q (f v none)
              ((Tape.move Dir.right)^[List.length.{u_2} (α := Γ k) []] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))
          else
            TM1.stepAux q
              (f v
                ((Tape.move Dir.left
                        ((Tape.move Dir.right)^[List.length.{u_2} (α := Γ k) []]
                          (Tape.mk' ∅ (addBottom (Γ := Γ) L)))).head.2
                  k))
              (Tape.write
                ((Tape.move Dir.left
                        ((Tape.move Dir.right)^[List.length.{u_2} (α := Γ k) []]
                          (Tape.mk' ∅ (addBottom (Γ := Γ) L)))).head.1,
                  update (β := fun (k : K) ↦ Option (Γ k))
                    (Tape.move Dir.left
                          ((Tape.move Dir.right)^[List.length.{u_2} (α := Γ k) []]
                            (Tape.mk' ∅ (addBottom (Γ := Γ) L)))).head.2
                    k none)
                (Tape.move Dir.left
                  ((Tape.move Dir.right)^[List.length.{u_2} (α := Γ k) []] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))))) =
          TM1.stepAux q (f v (List.head? []))
            ((Tape.move Dir.right)^[List.length.{u_2} (α := Γ k) (List.tail [])] (Tape.mk' ∅ (addBottom (Γ := Γ) L')))
pop₁ :
  ∀ (hd : Γ k) (tl : List (Γ k)) (e : S k = hd :: tl),
    ∃ (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')))
⊢ ∃ (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 (S k).tail k_1)).reverse) ∧
      (bif ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L))).head.1 then
          TM1.stepAux q (f v none) ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))
        else
          TM1.stepAux q
            (f v
              ((Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))).head.2
                k))
            (Tape.write
              ((Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))).head.1,
                update (β := fun (k : K) ↦ Option (Γ k))
                  (Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))).head.2
                  k none)
              (Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))))) =
        TM1.stepAux q (f v (S k).head?) ((Tape.move Dir.right)^[(S k).tail.length] (Tape.mk' ∅ (addBottom (Γ := Γ) L')))

Tactic:
rcases e : S k with - | ⟨hd, tl⟩