-- Mathlib/Computability/TMToPartrec.lean
theorem head_main_ok {q s L} {c d : List Γ'} :
    Reaches₁ (TM2.step tr) ⟨some (head main q), s, K'.elim (trList L) [] c d⟩
      ⟨some q, none, K'.elim (trList [L.headI]) [] c d⟩

Proof state:
case refine_2.refine_2
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn L none fun x x => some Γ'.cons
⊢ TransGen (fun a b => b ∈ TM2.step tr a)
    { l := some (unrev q), var := none,
      stk := update (elim (trList L.tail) ((some Γ'.cons).iget :: (trNat L.headI).reverseAux []) c d) main [] }
    { l := some q, var := none, stk := elim (trNat L.headI ++ [Γ'.cons]) [] c d }

Tactic:
convert unrev_ok using 2

Result:
case h.e'_2.h.e'_7
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn L none fun x x => some Γ'.cons
⊢ elim (trNat L.headI ++ [Γ'.cons]) [] c d =
    update
      (update (update (elim (trList L.tail) ((some Γ'.cons).iget :: (trNat L.headI).reverseAux []) c d) main []) rev [])
      main
      ((update (elim (trList L.tail) ((some Γ'.cons).iget :: (trNat L.headI).reverseAux []) c d) main [] rev).reverseAux
        (update (elim (trList L.tail) ((some Γ'.cons).iget :: (trNat L.headI).reverseAux []) c d) main [] main))

Proof state:
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn L none fun x x => some Γ'.cons
⊢ main ≠ rev

Tactic:
decide

Result:
no goals

Proof state:
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn L none fun x x => some Γ'.cons
⊢ Reaches₁ (TM2.step tr) { l := some (head main q), var := s, stk := elim (trList L) [] c d }
    { l := some q, var := none, stk := elim (trList [L.headI]) [] c d }

Tactic:
refine
  (move_ok (by decide)
        (splitAtPred_eq _ _ (trNat L.headI) o (trList L.tail) (trNat_natEnd _) ?_)).trans
    (TransGen.head rfl (TransGen.head rfl ?_))

Result:
case refine_1
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn L none fun x x => some Γ'.cons
⊢ Option.elim' (elim (trList L) [] c d main = trNat L.headI ∧ trList L.tail = [])
    (fun a => natEnd a = true ∧ elim (trList L) [] c d main = trNat L.headI ++ a :: trList L.tail) o

case refine_2
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn L none fun x x => some Γ'.cons
⊢ 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ₗ)) main) (unrev q))
          o))
      o
      (update
        (update (update (elim (trList L) [] c d) main (trList L.tail)) rev
          ((trNat L.headI).reverseAux (elim (trList L) [] c d rev)))
        rev
        ((fun s => ((fun x => some Γ'.cons) s).iget) o ::
          update (update (elim (trList L) [] c d) main (trList L.tail)) rev
            ((trNat L.headI).reverseAux (elim (trList L) [] c d rev)) rev)))
    { l := some q, var := none, stk := elim (trList [L.headI]) [] c d }

Proof state:
case h.e'_2.h.e'_7
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn L none fun x x => some Γ'.cons
⊢ elim (trNat L.headI ++ [Γ'.cons]) [] c d =
    update
      (update (update (elim (trList L.tail) ((some Γ'.cons).iget :: (trNat L.headI).reverseAux []) c d) main []) rev [])
      main
      ((update (elim (trList L.tail) ((some Γ'.cons).iget :: (trNat L.headI).reverseAux []) c d) main [] rev).reverseAux
        (update (elim (trList L.tail) ((some Γ'.cons).iget :: (trNat L.headI).reverseAux []) c d) main [] main))

Tactic:
simp [List.reverseAux_eq]

Result:
no goals