-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n : ℕ
f : List.Vector ℕ n →. ℕ
hf : Nat.Partrec' f
prim :
  ∀ {n : ℕ} {f : List.Vector ℕ n → ℕ} (hf : Nat.Primrec' f),
    ∃ (c : Code), ∀ (v : List.Vector ℕ n), c.eval (↑v : List ℕ) = pure <$> (↑f : List.Vector ℕ n →. ℕ) v
comp :
  ∀ {m n : ℕ} {f : List.Vector ℕ n →. ℕ} (g : Fin n → List.Vector ℕ m →. ℕ),
    Nat.Partrec' f →
      (∀ (i : Fin n), Nat.Partrec' (g i)) →
        ∀ (IHf : ∃ (c : Code), ∀ (v : List.Vector ℕ n), c.eval (↑v : List ℕ) = pure <$> f v)
          (IHg : ∀ (i : Fin n), ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> g i v),
          ∃ (c : Code),
            ∀ (v : List.Vector ℕ m),
              c.eval (↑v : List ℕ) =
                pure <$> (fun (v : List.Vector ℕ m) ↦ (Vector.mOfFn fun (i : Fin n) ↦ g i v) >>= f) v
rfind :
  ∀ {n : ℕ} {f : List.Vector ℕ (n + 1) → ℕ},
    Nat.Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ) →
      ∀
        (IHf :
          ∃ (c : Code),
            ∀ (v : List.Vector ℕ (n + 1)), c.eval (↑v : List ℕ) = pure <$> (↑f : List.Vector ℕ (n + 1) →. ℕ) v),
        ∃ (c : Code),
          ∀ (v : List.Vector ℕ n),
            c.eval (↑v : List ℕ) =
              pure <$> (fun (v : List.Vector ℕ n) ↦ Nat.rfind fun (n_1 : ℕ) ↦ Part.some (decide (f (n_1 ::ᵥ v) = 0))) v
⊢ ∃ (c : Code), ∀ (v : List.Vector ℕ n), c.eval (↑v : List ℕ) = pure <$> f v

Tactic:
induction hf with
  | prim hf =>
    induction hf with
    | zero => exact ⟨zero', fun ⟨[], _⟩ => rfl⟩
    | succ => exact ⟨succ, fun ⟨[v], _⟩ => rfl⟩
    | get i =>
      refine Fin.succRec (fun n => ?_) (fun n i IH => ?_) i
      · exact ⟨head, fun ⟨List.cons a as, _⟩ => by simp; rfl⟩
      · obtain ⟨c, h⟩ := IH
        exact ⟨c.comp tail, fun v => by simpa [← Vector.get_tail, Bind.bind] using h v.tail⟩
    | comp g hf hg IHf IHg =>
      simpa [Part.bind_eq_bind] using exists_code.comp IHf IHg
    | @prec n f g _ _ IHf IHg =>
      obtain ⟨cf, hf⟩ := IHf
      obtain ⟨cg, hg⟩ := IHg
      simp only [Part.map_eq_map, Part.map_some, PFun.coe_val] at hf hg
      refine ⟨prec cf cg, fun v => ?_⟩
      rw [← v.cons_head_tail]
      specialize hf v.tail
      replace hg := fun a b => hg (a ::ᵥ b ::ᵥ v.tail)
      simp only [Vector.cons_val, Vector.tail_val] at hf hg
      simp only [Part.map_eq_map, Part.map_some, Vector.cons_val, Vector.tail_cons,
        Vector.head_cons, PFun.coe_val, Vector.tail_val]
      simp only [← Part.pure_eq_some] at hf hg ⊢
      induction v.head with
        simp [prec, hf, Part.bind_assoc, ← Part.bind_some_eq_map, Part.bind_some, Bind.bind]
      | succ n _ =>
      suffices ∀ a b, a + b = n →
        (n.succ :: 0 ::
          g (n ::ᵥ Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ v.tail) ::
              v.val.tail : List ℕ) ∈
          PFun.fix
            (fun v : List ℕ => Part.bind (cg.eval (v.headI :: v.tail.tail))
              (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 : List ℕ)
                else Sum.inr
                  (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail))))
            (a :: b :: Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a :: v.val.tail) by
        have := Part.eq_some_iff.mpr (this _ _ (zero_add _))
        simp_all
      intro a b e
      induction b generalizing a with
      | zero =>
        refine PFun.mem_fix_iff.2 (Or.inl <| Part.eq_some_iff.1 ?_)
        simp only [hg, ← e, Part.bind_some, List.tail_cons, pure]
        rfl
      | succ b IH =>
        refine PFun.mem_fix_iff.2 (Or.inr ⟨_, ?_, IH (a + 1) (by rwa [add_right_comm])⟩)
        simp only [hg, Part.bind_some, List.tail_cons, pure]
        exact Part.mem_some_iff.2 rfl
  | comp g _ _ IHf IHg => exact exists_code.comp IHf IHg
  | @rfind n f _ IHf =>
    obtain ⟨cf, hf⟩ := IHf; refine ⟨rfind cf, fun v => ?_⟩
    replace hf := fun a => hf (a ::ᵥ v)
    simp only [Part.map_eq_map, Part.map_some, Vector.cons_val, PFun.coe_val,
      show ∀ x, pure x = [x] from fun _ => rfl] at hf ⊢
    refine Part.ext fun x => ?_
    simp only [rfind, Part.bind_eq_bind, Part.pure_eq_some, Part.bind_some,
      cons_eval, comp_eval, fix_eval, tail_eval, succ_eval, zero'_eval,
      List.headI_cons, pred_eval, Part.map_some, false_eq_decide_iff,
      Part.mem_bind_iff, Part.mem_map_iff, Nat.mem_rfind,
      List.tail_cons, true_eq_decide_iff, Part.mem_some_iff, Part.map_bind]
    constructor
    · rintro ⟨v', h1, rfl⟩
      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 _ ⟨⟩)
      clear h1
      intro v₀ h1
      refine PFun.fixInduction h1 fun v₁ h2 IH => ?_
      clear h1
      rintro n rfl hm
      have := PFun.mem_fix_iff.1 h2
      simp only [hf, Part.bind_some] at this
      split_ifs at this with h
      · simp only [List.headI_cons, exists_false, or_false, Part.mem_some_iff,
          List.tail_cons, false_and, Sum.inl.injEq, reduceCtorEq] at this
        subst this
        exact ⟨_, ⟨h, @hm⟩, rfl⟩
      · refine IH (n.succ::v.val) (by simp_all) _ rfl fun m h' => ?_
        obtain h | rfl := Nat.lt_succ_iff_lt_or_eq.1 h'
        exacts [hm _ h, h]
    · rintro ⟨n, ⟨hn, hm⟩, rfl⟩
      refine ⟨n.succ::v.1, ?_, rfl⟩
      have : (n.succ::v.1 : List ℕ) ∈
        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.val) :=
        PFun.mem_fix_iff.2 (Or.inl (by simp [hf, hn]))
      generalize (n.succ :: v.1 : List ℕ) = w at this ⊢
      clear hn
      induction n with
      | zero => exact this
      | succ n IH =>
        refine IH (fun {m} h' => hm (Nat.lt_succ_of_lt h'))
          (PFun.mem_fix_iff.2 (Or.inr ⟨_, ?_, this⟩))
        simp only [hf, hm n.lt_succ_self, Part.bind_some, List.headI, if_false,
          Part.mem_some_iff, List.tail_cons]

Premises used: Pure.pure, reduceCtorEq, Iff.mpr, Part.mem_bind_iff, List.Vector.tail_cons, Turing.ToPartrec.Code.comp_eval, List.Vector.cons_val, Part.map_bind, Turing.ToPartrec.Code.pred_eval, Part.eq_some_iff, Part.bind_some, Part.mem_some_iff, PFun.coe_val, if_false, MonadState.get, false_and, Turing.ToPartrec.Code.zero'_eval, Turing.ToPartrec.Code.tail_eval, Nat.mem_rfind, false_eq_decide_iff, Part.map_eq_map, Turing.ToPartrec.Code.succ, List.tail_cons, Sum.inl.injEq, List.headI_cons, Turing.ToPartrec.Code.prec, Part.ext, Turing.ToPartrec.Code.cons_eval, Part.bind_some_eq_map, Turing.ToPartrec.Code.rfind, Turing.ToPartrec.Code.comp, Turing.ToPartrec.Code.zero, List.Vector.head_cons, exists_false, Part.map_some, Turing.ToPartrec.Code.succ_eval, Part.bind_assoc, Iff.mp, Bind.bind, or_false, Turing.ToPartrec.Code.fix_eval, Or.inl, PFun.mem_fix_iff, List.headI, Part.mem_map_iff, Part.pure_eq_some, List.Vector.tail_val, Part.bind_eq_bind, true_eq_decide_iff, rfl