-- 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 : 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) → σ
⊢ ∃ (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')))
have 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')))
Tactic: rcases e : S k with - | ⟨hd, tl⟩