-- 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.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₀ v₁ : List ℕ
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)))
      v₁
IH :
  ∀ (a'' : List ℕ),
    (Sum.inr a'' ∈
        (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_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] = [v'.headI.pred]
⊢ ∀ (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:
rintro n rfl hm

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

Proof state:
case prim.get
n : ℕ
f : List.Vector ℕ n →. ℕ
n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ → ℕ
n✝ : ℕ
i : Fin n✝
⊢ ∃ c, ∀ (v : List.Vector ℕ n✝), c.eval ↑v = pure <$> (↑fun v => v.get i) v

Tactic:
refine Fin.succRec (fun n => ?_) (fun n i IH => ?_) i

Result:
case prim.get.refine_1
n✝² : ℕ
f : List.Vector ℕ n✝² →. ℕ
n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ → ℕ
n✝ : ℕ
i : Fin n✝
n : ℕ
⊢ ∃ c, ∀ (v : List.Vector ℕ n.succ), c.eval ↑v = pure <$> (↑fun v => v.get 0) v

case prim.get.refine_2
n✝² : ℕ
f : List.Vector ℕ n✝² →. ℕ
n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ → ℕ
n✝ : ℕ
i✝ : Fin n✝
n : ℕ
i : Fin n
IH : ∃ c, ∀ (v : List.Vector ℕ n), c.eval ↑v = pure <$> (↑fun v => v.get i) v
⊢ ∃ c, ∀ (v : List.Vector ℕ n.succ), c.eval ↑v = pure <$> (↑fun v => v.get i.succ) v

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

Tactic:
simp only [Vector.cons_val, Vector.tail_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
v : List.Vector ℕ (n + 1)
hf : cf.eval (↑v).tail = Part.some (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (a :: b :: (↑v).tail) = Part.some (pure (g (a ::ᵥ b ::ᵥ v.tail)))
⊢ (cf.prec cg).eval ↑(v.head ::ᵥ v.tail) =
    pure <$> (↑fun v => Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) v.head) (v.head ::ᵥ v.tail)

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 ℕ
⊢ x ∈ cf.rfind.eval ↑v ↔ x ∈ Part.map pure (Nat.rfind fun n_1 => Part.some (decide (f (n_1 ::ᵥ v) = 0)))

Tactic:
simp only [rfind, Part.bind_eq_bind, Part.pure_eq_some, Part.map_eq_map, Part.bind_some,
  exists_prop, cons_eval, comp_eval, fix_eval, tail_eval, succ_eval, zero'_eval,
  List.headI_nil, List.headI_cons, pred_eval, Part.map_some, false_eq_decide_iff,
  Part.mem_bind_iff, List.length, Part.mem_map_iff, Nat.mem_rfind, List.tail_nil,
  List.tail_cons, true_eq_decide_iff, Part.mem_some_iff, Part.map_bind]

Result:
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

Proof state:
n✝² : ℕ
f : List.Vector ℕ n✝² →. ℕ
n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ → ℕ
n✝ : ℕ
i✝ : Fin n✝
n : ℕ
i : Fin n
c : Code
h : ∀ (v : List.Vector ℕ n), c.eval ↑v = pure <$> (↑fun v => v.get i) v
v : List.Vector ℕ n.succ
⊢ (c.comp tail).eval ↑v = pure <$> (↑fun v => v.get i.succ) v

Tactic:
simpa [← Vector.get_tail, Bind.bind] using h v.tail

Result:
no goals

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 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

Tactic:
refine ⟨prec cf cg, fun v => ?_⟩

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))
v : List.Vector ℕ (n + 1)
⊢ (cf.prec cg).eval ↑v = pure <$> (↑fun v => Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) v.head) v

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

Tactic:
replace hg := fun a b => hg (a ::ᵥ b ::ᵥ v.tail)

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