-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
⊢ elim (Γ'.cons :: trList v) [] c d =
    update (β := fun (k : K') ↦ List Γ')
      (update (β := fun (a : K') ↦ List Γ')
        ((bif decide ((elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head? = some Γ'.bit0) then
              TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂))
                (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?
                (update (β := fun (k : K') ↦ List Γ')
                  (update (β := fun (k : K') ↦ List Γ') (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                    (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail)
                  rev
                  (Γ'.bit1 ::
                    update (β := fun (k : K') ↦ List Γ') (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                      (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail rev))
            else
              bif natEnd ((elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?.getD default) then
                TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?
                  (update (β := fun (k : K') ↦ List Γ') (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                    (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail)
              else
                TM2.stepAux (Γ := fun (x : K') ↦ Γ')
                  (peek' main
                    (branch (Γ := fun (x : K') ↦ Γ') (fun (s : Option Γ') ↦ natEnd (s.getD default))
                      (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ unrev q₂)
                      (push (Γ := fun (x : K') ↦ Γ') rev (fun (x : Option Γ') ↦ Γ'.bit0)
                        (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ unrev q₂))))
                  (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?
                  (update (β := fun (k : K') ↦ List Γ') (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                    (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail)).stk
          (Γ := fun (x : K') ↦ Γ'))
        rev [])
      main
      (((bif decide ((elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head? = some Γ'.bit0) then
                TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂))
                  (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?
                  (update (β := fun (k : K') ↦ List Γ')
                    (update (β := fun (k : K') ↦ List Γ') (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                      (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail)
                    rev
                    (Γ'.bit1 ::
                      update (β := fun (k : K') ↦ List Γ') (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                        (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail rev))
              else
                bif natEnd ((elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?.getD default) then
                  TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁)
                    (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?
                    (update (β := fun (k : K') ↦ List Γ') (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                      (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail)
                else
                  TM2.stepAux (Γ := fun (x : K') ↦ Γ')
                    (peek' main
                      (branch (Γ := fun (x : K') ↦ Γ') (fun (s : Option Γ') ↦ natEnd (s.getD default))
                        (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ unrev q₂)
                        (push (Γ := fun (x : K') ↦ Γ') rev (fun (x : Option Γ') ↦ Γ'.bit0)
                          (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ unrev q₂))))
                    (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?
                    (update (β := fun (k : K') ↦ List Γ') (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                      (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail)).stk
            (Γ := fun (x : K') ↦ Γ') rev).reverseAux
        ((bif decide ((elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head? = some Γ'.bit0) then
              TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂))
                (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?
                (update (β := fun (k : K') ↦ List Γ')
                  (update (β := fun (k : K') ↦ List Γ') (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                    (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail)
                  rev
                  (Γ'.bit1 ::
                    update (β := fun (k : K') ↦ List Γ') (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                      (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail rev))
            else
              bif natEnd ((elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?.getD default) then
                TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?
                  (update (β := fun (k : K') ↦ List Γ') (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                    (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail)
              else
                TM2.stepAux (Γ := fun (x : K') ↦ Γ')
                  (peek' main
                    (branch (Γ := fun (x : K') ↦ Γ') (fun (s : Option Γ') ↦ natEnd (s.getD default))
                      (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ unrev q₂)
                      (push (Γ := fun (x : K') ↦ Γ') rev (fun (x : Option Γ') ↦ Γ'.bit0)
                        (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ unrev q₂))))
                  (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?
                  (update (β := fun (k : K') ↦ List Γ') (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                    (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail)).stk
          (Γ := fun (x : K') ↦ Γ') main))

Tactic:
simp