-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f_2 : List.Vector ℕ n_2 → ℕ
n_3 : ℕ
f : List.Vector ℕ n_3 → ℕ
g : List.Vector ℕ (n_3 + 2) → ℕ
h : Nat.Primrec' f
h_1 : Nat.Primrec' g
cf cg : Code
v : List.Vector ℕ (n_3 + 1)
hf : cf.eval (↑v : List ℕ).tail = pure (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (a :: b :: (↑v : List ℕ).tail) = pure (pure (g (a ::ᵥ b ::ᵥ v.tail)))
n : ℕ
h_2 :
  (cf.prec cg).eval (n :: (↑v : List ℕ).tail) =
    pure (pure (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n))
a : ℕ
e : a + 0 = n
prim :
  Part.some
      (if
          Eq (α := ℕ)
            (List.headI
                (0 ::
                  Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a ::
                    (↑v : List ℕ).tail) :
              ℕ)
            (0 : ℕ) then
        Sum.inl
          ((a ::
                  0 ::
                    Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a ::
                      (↑v : List ℕ).tail).headI.succ ::
            Nat.pred
                (List.headI
                  (0 ::
                    Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a ::
                      (↑v : List ℕ).tail)) ::
              [g
                      ((a ::
                            0 ::
                              Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail))
                                  a ::
                                (↑v : List ℕ).tail).headI ::ᵥ
                        Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a ::ᵥ
                          v.tail)].headI ::
                (↑v : List ℕ).tail)
      else
        Sum.inr
          ((a ::
                  0 ::
                    Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a ::
                      (↑v : List ℕ).tail).headI.succ ::
            Nat.pred
                (List.headI
                  (0 ::
                    Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a ::
                      (↑v : List ℕ).tail)) ::
              [g
                      ((a ::
                            0 ::
                              Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail))
                                  a ::
                                (↑v : List ℕ).tail).headI ::ᵥ
                        Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a ::ᵥ
                          v.tail)].headI ::
                (↑v : List ℕ).tail)) =
    Part.some
      (Sum.inl
        ((a + 0).succ ::
          0 ::
            g
                ((a + 0) ::ᵥ
                  Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) (a + 0) ::ᵥ
                    v.tail) ::
              (↑v : List ℕ).tail))
⊢ Eq (α := Part (List ℕ ⊕ List ℕ))
    ((cg.eval
          ((a ::
                0 ::
                  Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a ::
                    (↑v : List ℕ).tail).headI ::
            (a ::
                  0 ::
                    Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a ::
                      (↑v : List ℕ).tail).tail.tail)).bind
      fun (x : List ℕ) ↦
      Part.some
        (if
            (a ::
                    0 ::
                      Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a ::
                        (↑v : List ℕ).tail).tail.headI =
              0 then
          Sum.inl
            ((a ::
                    0 ::
                      Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a ::
                        (↑v : List ℕ).tail).headI.succ ::
              (a ::
                        0 ::
                          Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a ::
                            (↑v : List ℕ).tail).tail.headI.pred ::
                x.headI ::
                  (a ::
                          0 ::
                            Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail))
                                a ::
                              (↑v : List ℕ).tail).tail.tail.tail)
        else
          Sum.inr
            ((a ::
                    0 ::
                      Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a ::
                        (↑v : List ℕ).tail).headI.succ ::
              (a ::
                        0 ::
                          Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a ::
                            (↑v : List ℕ).tail).tail.headI.pred ::
                x.headI ::
                  (a ::
                          0 ::
                            Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail))
                                a ::
                              (↑v : List ℕ).tail).tail.tail.tail)))
    (Part.some
      (Sum.inl
        (n.succ ::
          0 ::
            g
                (n ::ᵥ
                  Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ
                    v.tail) ::
              (↑v : List ℕ).tail)))

Tactic:
simp only [hg, ← e, Part.bind_some, List.tail_cons, pure]

Premises used: Pure.pure, Part.bind_some, List.tail_cons