-- Mathlib/Computability/TMToPartrec.lean
theorem head_stack_ok {q s L₁ L₂ L₃} :
    Reaches₁ (TM2.step tr)
      ⟨some (head stack q), s, K'.elim (trList L₁) [] [] (trList L₂ ++ Γ'.consₗ :: L₃)⟩
      ⟨some q, none, K'.elim (trList (L₂.headI :: L₁)) [] [] L₃⟩

Proof state:
case cons
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
a : ℕ
L₂ : List ℕ
⊢ Reaches₁ (TM2.step tr)
    { l := some (head stack q), var := s, stk := elim (trList L₁) [] [] (trList (a :: L₂) ++ Γ'.consₗ :: L₃) }
    { l := some q, var := none, stk := elim (trList ((a :: L₂).headI :: L₁)) [] [] L₃ }

Tactic:
refine
  TransGen.trans
    (move_ok (by decide)
      (splitAtPred_eq _ _ (trNat a) (some Γ'.cons) (trList L₂ ++ Γ'.consₗ :: L₃)
        (trNat_natEnd _) ⟨rfl, by simp⟩))
    (TransGen.head rfl (TransGen.head rfl ?_))

Result:
case cons
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
a : ℕ
L₂ : List ℕ
⊢ TransGen (fun a b => b ∈ TM2.step tr a)
    (TM2.stepAux
      (tr
        ((fun x =>
            Λ'.read fun s =>
              (if s = some Γ'.consₗ then id else Λ'.clear (fun x => decide (x = Γ'.consₗ)) stack) (unrev q))
          (some Γ'.cons)))
      (some Γ'.cons)
      (update
        (update
          (update (elim (trList L₁) [] [] (trList (a :: L₂) ++ Γ'.consₗ :: L₃)) stack (trList L₂ ++ Γ'.consₗ :: L₃)) rev
          ((trNat a).reverseAux (elim (trList L₁) [] [] (trList (a :: L₂) ++ Γ'.consₗ :: L₃) rev)))
        rev
        ((fun s => ((fun x => some Γ'.cons) s).iget) (some Γ'.cons) ::
          update
            (update (elim (trList L₁) [] [] (trList (a :: L₂) ++ Γ'.consₗ :: L₃)) stack (trList L₂ ++ Γ'.consₗ :: L₃))
            rev ((trNat a).reverseAux (elim (trList L₁) [] [] (trList (a :: L₂) ++ Γ'.consₗ :: L₃) rev)) rev)))
    { l := some q, var := none, stk := elim (trList ((a :: L₂).headI :: L₁)) [] [] L₃ }

Proof state:
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
a : ℕ
L₂ : List ℕ
⊢ elim (trList L₁) ((some Γ'.cons).iget :: (trNat a).reverseAux []) [] (trList L₂ ++ Γ'.consₗ :: L₃) stack =
    trList L₂ ++ Γ'.consₗ :: L₃

Tactic:
simp

Result:
no goals

Proof state:
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
a : ℕ
L₂ : List ℕ
⊢ stack ≠ rev

Tactic:
decide

Result:
no goals

Proof state:
case cons
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
a : ℕ
L₂ : List ℕ
⊢ TransGen
    (fun a b =>
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    { l := some (unrev q), var := some Γ'.consₗ,
      stk :=
        update (elim (trList L₁) ((some Γ'.cons).iget :: (trNat a).reverseAux []) [] (trList L₂ ++ Γ'.consₗ :: L₃))
          stack L₃ }
    { l := some q, var := none, stk := elim (trNat a ++ Γ'.cons :: trList L₁) [] [] L₃ }

Tactic:
convert unrev_ok using 2

Result:
case h.e'_2.h.e'_7
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
a : ℕ
L₂ : List ℕ
⊢ elim (trNat a ++ Γ'.cons :: trList L₁) [] [] L₃ =
    update
      (update
        (update (elim (trList L₁) ((some Γ'.cons).iget :: (trNat a).reverseAux []) [] (trList L₂ ++ Γ'.consₗ :: L₃))
          stack L₃)
        rev [])
      main
      ((update (elim (trList L₁) ((some Γ'.cons).iget :: (trNat a).reverseAux []) [] (trList L₂ ++ Γ'.consₗ :: L₃))
            stack L₃ rev).reverseAux
        (update (elim (trList L₁) ((some Γ'.cons).iget :: (trNat a).reverseAux []) [] (trList L₂ ++ Γ'.consₗ :: L₃))
          stack L₃ main))

Proof state:
case nil
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
⊢ TransGen (fun a b => b ∈ TM2.step tr a)
    (TM2.stepAux
      (goto fun s => (if s = some Γ'.consₗ then id else Λ'.clear (fun x => decide (x = Γ'.consₗ)) stack) (unrev q))
      (some Γ'.consₗ)
      (update
        (update (update (elim (trList L₁) [] [] (trList [] ++ Γ'.consₗ :: L₃)) stack L₃) rev
          ([].reverseAux (elim (trList L₁) [] [] (trList [] ++ Γ'.consₗ :: L₃) rev)))
        rev
        ((fun s => ((fun x => some Γ'.cons) s).iget) (some Γ'.consₗ) ::
          update (update (elim (trList L₁) [] [] (trList [] ++ Γ'.consₗ :: L₃)) stack L₃) rev
            ([].reverseAux (elim (trList L₁) [] [] (trList [] ++ Γ'.consₗ :: L₃) rev)) rev)))
    { l := some q, var := none, stk := elim (trList ([].headI :: L₁)) [] [] L₃ }

Tactic:
simp only [TM2.step, Option.mem_def, TM2.stepAux, ite_true, id_eq, trList, List.nil_append,
  elim_update_stack, elim_rev, List.reverseAux_nil, elim_update_rev, Function.update_self,
  List.headI_nil, trNat_default]

Result:
case nil
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
⊢ TransGen
    (fun a b =>
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    { l := some (unrev q), var := some Γ'.consₗ, stk := elim (trList L₁) [(some Γ'.cons).iget] [] L₃ }
    { l := some q, var := none, stk := elim (Γ'.cons :: trList L₁) [] [] L₃ }

Proof state:
q : Λ'
s : Option Γ'
L₁ L₂ : List ℕ
L₃ : List Γ'
⊢ Reaches₁ (TM2.step tr)
    { l := some (head stack q), var := s, stk := elim (trList L₁) [] [] (trList L₂ ++ Γ'.consₗ :: L₃) }
    { l := some q, var := none, stk := elim (trList (L₂.headI :: L₁)) [] [] L₃ }

Tactic:
rcases L₂ with - | ⟨a, L₂⟩

Result:
case nil
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
⊢ Reaches₁ (TM2.step tr)
    { l := some (head stack q), var := s, stk := elim (trList L₁) [] [] (trList [] ++ Γ'.consₗ :: L₃) }
    { l := some q, var := none, stk := elim (trList ([].headI :: L₁)) [] [] L₃ }

case cons
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
a : ℕ
L₂ : List ℕ
⊢ Reaches₁ (TM2.step tr)
    { l := some (head stack q), var := s, stk := elim (trList L₁) [] [] (trList (a :: L₂) ++ Γ'.consₗ :: L₃) }
    { l := some q, var := none, stk := elim (trList ((a :: L₂).headI :: L₁)) [] [] L₃ }

Proof state:
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
⊢ ∀ x ∈ [], natEnd x = false

Tactic:
rintro _ ⟨⟩

Result:
no goals

Proof state:
case h.e'_2.h.e'_7
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
a : ℕ
L₂ : List ℕ
⊢ elim (trNat a ++ Γ'.cons :: trList L₁) [] [] L₃ =
    update
      (update
        (update (elim (trList L₁) ((some Γ'.cons).iget :: (trNat a).reverseAux []) [] (trList L₂ ++ Γ'.consₗ :: L₃))
          stack L₃)
        rev [])
      main
      ((update (elim (trList L₁) ((some Γ'.cons).iget :: (trNat a).reverseAux []) [] (trList L₂ ++ Γ'.consₗ :: L₃))
            stack L₃ rev).reverseAux
        (update (elim (trList L₁) ((some Γ'.cons).iget :: (trNat a).reverseAux []) [] (trList L₂ ++ Γ'.consₗ :: L₃))
          stack L₃ main))

Tactic:
simp [List.reverseAux_eq]

Result:
no goals

Proof state:
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
⊢ stack ≠ rev

Tactic:
decide

Result:
no goals