-- 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 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
⊢ n.succ :: 0 :: g (n ::ᵥ Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ v.tail) :: (↑v).tail ∈
    PFun.fix
      (fun v =>
        (cg.eval (v.headI :: v.tail.tail)).bind fun x =>
          Part.some
            (if v.tail.headI = 0 then Sum.inl (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)
            else Sum.inr (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)))
      (a :: 0 :: Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail)

Tactic:
refine PFun.mem_fix_iff.2 (Or.inl <| Part.eq_some_iff.1 ?_)

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
⊢ ((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))

Proof state:
case prim.prec.intro.intro
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 : Code
hf : ∀ (v : List.Vector ℕ n), cf.eval ↑v = pure <$> ↑f v
cg : Code
hg : ∀ (v : List.Vector ℕ (n + 2)), cg.eval ↑v = pure <$> ↑g v
⊢ ∃ c,
    ∀ (v : List.Vector ℕ (n + 1)),
      c.eval ↑v = pure <$> (↑fun v => Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) v.head) v

Tactic:
simp only [Part.map_eq_map, Part.map_some, PFun.coe_val] at hf hg

Result:
case prim.prec.intro.intro
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
hf : ∀ (v : List.Vector ℕ n), cf.eval ↑v = Part.some (pure (f v))
hg : ∀ (v : List.Vector ℕ (n + 2)), cg.eval ↑v = Part.some (pure (g v))
⊢ ∃ c,
    ∀ (v : List.Vector ℕ (n + 1)),
      c.eval ↑v = pure <$> (↑fun v => Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) v.head) v

Proof state:
case rfind.intro.mp.intro.intro
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' : List ℕ
⊢ ∀ (v₁ : List ℕ),
    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)))
          v₁ →
      ∀ (n_1 : ℕ),
        v₁ = n_1 :: ↑v →
          (∀ m < n_1, ¬f (m ::ᵥ v) = 0) →
            ∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]

Tactic:
intro v₀ h1

Result:
case rfind.intro.mp.intro.intro
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 ℕ
h1 :
  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)))
      v₀
⊢ ∀ (n_1 : ℕ),
    v₀ = n_1 :: ↑v →
      (∀ m < n_1, ¬f (m ::ᵥ v) = 0) →
        ∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]

Proof state:
case rfind.intro.mpr.intro.intro.intro.zero
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)]
w : List ℕ
hm : ∀ {m : ℕ}, m < 0 → ¬f (m ::ᵥ v) = 0
this :
  w ∈
    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)))
      (0 :: ↑v)
⊢ w ∈
    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)))
      (0 :: ↑v)

Tactic:
exact this

Result:
no goals