-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
h :
  Eq (α := TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNum Num.zero.succ ++ [Γ'.cons]) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none
      (elim (Γ'.bit1 :: Γ'.cons :: (trNum Num.zero ++ [Γ'.cons]).tail) [] c d))
⊢ Eq (α := TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNum Num.zero.succ ++ [Γ'.cons]) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none
      (update (β := fun (k : K') ↦ List Γ')
        (update (β := fun (a : K') ↦ List Γ')
          (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
            (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
              (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trNum Num.zero ++ [Γ'.cons]) [] c d)
                main (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail)
              main
              ((fun (x : Option Γ') ↦ Γ'.cons)
                  ((fun (x v : Option Γ') ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trNum Num.zero ++ [Γ'.cons]) [] c d)
                  main (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail main))
            main
            ((fun (x : Option Γ') ↦ Γ'.bit1)
                ((fun (x v : Option Γ') ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
              update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
                (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trNum Num.zero ++ [Γ'.cons]) [] c d)
                  main (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail)
                main
                ((fun (x : Option Γ') ↦ Γ'.cons)
                    ((fun (x v : Option Γ') ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                  update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trNum Num.zero ++ [Γ'.cons]) [] c d)
                    main (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail main)
                main))
          rev [])
        main
        ((update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
              (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
                (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trNum Num.zero ++ [Γ'.cons]) [] c d)
                  main (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail)
                main
                ((fun (x : Option Γ') ↦ Γ'.cons)
                    ((fun (x v : Option Γ') ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                  update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trNum Num.zero ++ [Γ'.cons]) [] c d)
                    main (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail main))
              main
              ((fun (x : Option Γ') ↦ Γ'.bit1)
                  ((fun (x v : Option Γ') ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
                  (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trNum Num.zero ++ [Γ'.cons]) [] c d)
                    main (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail)
                  main
                  ((fun (x : Option Γ') ↦ Γ'.cons)
                      ((fun (x v : Option Γ') ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                    update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
                      (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
                      (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail main)
                  main)
              rev).reverseAux
          (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
            (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
              (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trNum Num.zero ++ [Γ'.cons]) [] c d)
                main (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail)
              main
              ((fun (x : Option Γ') ↦ Γ'.cons)
                  ((fun (x v : Option Γ') ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trNum Num.zero ++ [Γ'.cons]) [] c d)
                  main (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail main))
            main
            ((fun (x : Option Γ') ↦ Γ'.bit1)
                ((fun (x v : Option Γ') ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
              update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
                (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trNum Num.zero ++ [Γ'.cons]) [] c d)
                  main (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail)
                main
                ((fun (x : Option Γ') ↦ Γ'.cons)
                    ((fun (x v : Option Γ') ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                  update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (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]

Premises used: Turing.PartrecToTM2.K'.elim_update_main, Turing.PartrecToTM2.K'.elim_rev, List.reverseAux_nil, Turing.PartrecToTM2.K'.elim_main, Turing.PartrecToTM2.K'.elim_update_rev