-- Mathlib/Computability/TMConfig.lean
theorem exists_code {n} {f : List.Vector ℕ n →. ℕ} (hf : Nat.Partrec' f) :
    ∃ c : Code, ∀ v : List.Vector ℕ n, c.eval v.1 = pure <$> f v

Proof state:
case neg
n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ →. ℕ
n✝ : ℕ
f : List.Vector ℕ (n✝ + 1) → ℕ
a✝ : Nat.Partrec' ↑f
cf : Code
v : List.Vector ℕ n✝
hf : ∀ (a : ℕ), cf.eval (a :: ↑v) = Part.some [f (a ::ᵥ v)]
v' v₀ : List ℕ
n : ℕ
h2 :
  v' ∈
    PFun.fix
      (fun v =>
        (cf.eval v).bind fun y =>
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      (n :: ↑v)
IH :
  ∀ (a'' : List ℕ),
    (Sum.inr a'' ∈
        (cf.eval (n :: ↑v)).bind fun y =>
          Part.some
            (if y.headI = 0 then Sum.inl ((n :: ↑v).headI.succ :: (n :: ↑v).tail)
            else Sum.inr ((n :: ↑v).headI.succ :: (n :: ↑v).tail))) →
      ∀ (n : ℕ),
        a'' = n :: ↑v →
          (∀ m < n, ¬f (m ::ᵥ v) = 0) →
            ∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]
hm : ∀ m < n, ¬f (m ::ᵥ v) = 0
h : ¬[f (n ::ᵥ v)].headI = 0
this :
  Sum.inl v' ∈ Part.some (Sum.inr ((n :: ↑v).headI.succ :: (n :: ↑v).tail)) ∨
    ∃ a',
      Sum.inr a' ∈ Part.some (Sum.inr ((n :: ↑v).headI.succ :: (n :: ↑v).tail)) ∧
        v' ∈
          PFun.fix
            (fun v =>
              (cf.eval v).bind fun y =>
                Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
            a'
⊢ ∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]

Tactic:
refine IH (n.succ::v.val) (by simp_all) _ rfl fun m h' => ?_

Result:
case neg
n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ →. ℕ
n✝ : ℕ
f : List.Vector ℕ (n✝ + 1) → ℕ
a✝ : Nat.Partrec' ↑f
cf : Code
v : List.Vector ℕ n✝
hf : ∀ (a : ℕ), cf.eval (a :: ↑v) = Part.some [f (a ::ᵥ v)]
v' v₀ : List ℕ
n : ℕ
h2 :
  v' ∈
    PFun.fix
      (fun v =>
        (cf.eval v).bind fun y =>
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      (n :: ↑v)
IH :
  ∀ (a'' : List ℕ),
    (Sum.inr a'' ∈
        (cf.eval (n :: ↑v)).bind fun y =>
          Part.some
            (if y.headI = 0 then Sum.inl ((n :: ↑v).headI.succ :: (n :: ↑v).tail)
            else Sum.inr ((n :: ↑v).headI.succ :: (n :: ↑v).tail))) →
      ∀ (n : ℕ),
        a'' = n :: ↑v →
          (∀ m < n, ¬f (m ::ᵥ v) = 0) →
            ∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]
hm : ∀ m < n, ¬f (m ::ᵥ v) = 0
h : ¬[f (n ::ᵥ v)].headI = 0
this :
  Sum.inl v' ∈ Part.some (Sum.inr ((n :: ↑v).headI.succ :: (n :: ↑v).tail)) ∨
    ∃ a',
      Sum.inr a' ∈ Part.some (Sum.inr ((n :: ↑v).headI.succ :: (n :: ↑v).tail)) ∧
        v' ∈
          PFun.fix
            (fun v =>
              (cf.eval v).bind fun y =>
                Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
            a'
m : ℕ
h' : m < n.succ
⊢ ¬f (m ::ᵥ v) = 0

Proof state:
case prim.prec.intro.intro.succ.zero
n✝² : ℕ
f✝¹ : List.Vector ℕ n✝² →. ℕ
n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ → ℕ
n✝ : ℕ
f : List.Vector ℕ n✝ → ℕ
g : List.Vector ℕ (n✝ + 2) → ℕ
a✝² : Nat.Primrec' f
a✝¹ : Nat.Primrec' g
cf cg : Code
v : List.Vector ℕ (n✝ + 1)
hf : cf.eval (↑v).tail = pure (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (a :: b :: (↑v).tail) = pure (pure (g (a ::ᵥ b ::ᵥ v.tail)))
n : ℕ
a✝ : (cf.prec cg).eval (n :: (↑v).tail) = pure (pure (Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) n))
a : ℕ
e : a + 0 = n
⊢ ((cg.eval
          ((a :: 0 :: Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail).headI ::
            (a :: 0 :: Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail).tail.tail)).bind
      fun x =>
      Part.some
        (if (a :: 0 :: Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail).tail.headI = 0 then
          Sum.inl
            ((a :: 0 :: Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail).headI.succ ::
              (a :: 0 :: Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail).tail.headI.pred ::
                x.headI ::
                  (a :: 0 :: Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail).tail.tail.tail)
        else
          Sum.inr
            ((a :: 0 :: Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail).headI.succ ::
              (a :: 0 :: Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail).tail.headI.pred ::
                x.headI ::
                  (a ::
                          0 ::
                            Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail).tail.tail.tail))) =
    Part.some
      (Sum.inl
        (n.succ :: 0 :: g (n ::ᵥ Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ v.tail) :: (↑v).tail))

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

Result:
case prim.prec.intro.intro.succ.zero
n✝² : ℕ
f✝¹ : List.Vector ℕ n✝² →. ℕ
n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ → ℕ
n✝ : ℕ
f : List.Vector ℕ n✝ → ℕ
g : List.Vector ℕ (n✝ + 2) → ℕ
a✝² : Nat.Primrec' f
a✝¹ : Nat.Primrec' g
cf cg : Code
v : List.Vector ℕ (n✝ + 1)
hf : cf.eval (↑v).tail = pure (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (a :: b :: (↑v).tail) = pure (pure (g (a ::ᵥ b ::ᵥ v.tail)))
n : ℕ
a✝ : (cf.prec cg).eval (n :: (↑v).tail) = pure (pure (Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) n))
a : ℕ
e : a + 0 = n
⊢ Part.some
      (if (0 :: Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail).headI = 0 then
        Sum.inl
          ((a :: 0 :: Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail).headI.succ ::
            (0 :: Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail).headI.pred ::
              [g
                      ((a :: 0 :: Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail).headI ::ᵥ
                        Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a ::ᵥ v.tail)].headI ::
                (↑v).tail)
      else
        Sum.inr
          ((a :: 0 :: Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail).headI.succ ::
            (0 :: Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail).headI.pred ::
              [g
                      ((a :: 0 :: Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail).headI ::ᵥ
                        Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a ::ᵥ v.tail)].headI ::
                (↑v).tail)) =
    Part.some
      (Sum.inl
        ((a + 0).succ ::
          0 ::
            g ((a + 0) ::ᵥ Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) (a + 0) ::ᵥ v.tail) :: (↑v).tail))

Proof state:
case rfind
n✝ : ℕ
f✝ : List.Vector ℕ n✝ →. ℕ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
a✝ : Nat.Partrec' ↑f
IHf : ∃ c, ∀ (v : List.Vector ℕ (n + 1)), c.eval ↑v = pure <$> ↑f v
⊢ ∃ c,
    ∀ (v : List.Vector ℕ n),
      c.eval ↑v = pure <$> (fun v => Nat.rfind fun n_1 => Part.some (decide (f (n_1 ::ᵥ v) = 0))) v

Tactic:
obtain ⟨cf, hf⟩ := IHf

Result:
case rfind.intro
n✝ : ℕ
f✝ : List.Vector ℕ n✝ →. ℕ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
a✝ : Nat.Partrec' ↑f
cf : Code
hf : ∀ (v : List.Vector ℕ (n + 1)), cf.eval ↑v = pure <$> ↑f v
⊢ ∃ c,
    ∀ (v : List.Vector ℕ n),
      c.eval ↑v = pure <$> (fun v => Nat.rfind fun n_1 => Part.some (decide (f (n_1 ::ᵥ v) = 0))) v