-- 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 rfind.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)]
x : List ℕ
⊢ (∃
      a ∈
        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),
      x = [a.headI.pred]) ↔
    ∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ pure a = x

Tactic:
constructor

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

case rfind.intro.mpr
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)]
x : List ℕ
⊢ (∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ pure a = x) →
    ∃
      a ∈
        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),
      x = [a.headI.pred]

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 ℕ
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)))
      (0 :: ↑v)
⊢ ∀ (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:
clear 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' : 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]

Proof state:
case pos
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 ℕ
n : ℕ
hm : ∀ m < n, ¬f (m ::ᵥ v) = 0
h : [f (n ::ᵥ v)].headI = 0
h2 :
  n.succ :: ↑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_1 : ℕ),
        a'' = n_1 :: ↑v →
          (∀ m < n_1, ¬f (m ::ᵥ v) = 0) →
            ∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [(n.succ :: ↑v).headI.pred]
⊢ ∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [(n.succ :: ↑v).headI.pred]

Tactic:
exact ⟨_, ⟨h, @(hm)⟩, rfl⟩

Result:
no goals

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 ℕ
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)))
      (0 :: ↑v)
⊢ ∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ pure a = [v'.headI.pred]

Tactic:
suffices ∀ 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, (v₁ = n :: v.val) → (∀ m < n, ¬f (m ::ᵥ v) = 0) →
    ∃ a : ℕ,
      (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]
  by exact this _ h1 0 rfl (by rintro _ ⟨⟩)

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' : 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)))
      (0 :: ↑v)
⊢ ∀ (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]

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

Tactic:
rintro ⟨v', h1, rfl⟩

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' : 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)))
      (0 :: ↑v)
⊢ ∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ pure a = [v'.headI.pred]