Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case e'_2
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
⊢ { l := some q, var := none, stk := elim (trNum Num.zero.succ ++ [Γ'.cons]) [] c d } =
    { l := some q, var := none,
      stk :=
        update
          (update
            (update
              (update
                (update (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
                  (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail)
                main
                ((fun x ↦ Γ'.cons) ((fun x v ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                  update (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
                    (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail main))
              main
              ((fun x ↦ Γ'.bit1) ((fun x v ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                update
                  (update (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
                    (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail)
                  main
                  ((fun x ↦ Γ'.cons) ((fun x v ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                    update (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
                      (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail main)
                  main))
            rev [])
          main
          ((update
                (update
                  (update (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
                    (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail)
                  main
                  ((fun x ↦ Γ'.cons) ((fun x v ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                    update (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
                      (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail main))
                main
                ((fun x ↦ Γ'.bit1) ((fun x v ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                  update
                    (update (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
                      (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail)
                    main
                    ((fun x ↦ Γ'.cons) ((fun x v ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                      update (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
                        (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail main)
                    main)
                rev).reverseAux
            (update
              (update
                (update (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
                  (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail)
                main
                ((fun x ↦ Γ'.cons) ((fun x v ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                  update (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
                    (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail main))
              main
              ((fun x ↦ Γ'.bit1) ((fun x v ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                update
                  (update (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
                    (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail)
                  main
                  ((fun x ↦ Γ'.cons) ((fun x v ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                    update (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
                      (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail main)
                  main)
              main)) }

Tactic:
simp only [elim_update_rev, elim_rev, elim_main, List.reverseAux_nil, elim_update_main]

Goal state after:
case e'_2
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
⊢ { l := some q, var := none, stk := elim (trNum Num.zero.succ ++ [Γ'.cons]) [] c d } =
    { l := some q, var := none, stk := elim (Γ'.bit1 :: Γ'.cons :: (trNum Num.zero ++ [Γ'.cons]).tail) [] c d }