-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n : ℕ
f : List.Vector ℕ n →. ℕ
n_1 : ℕ
f_1 : List.Vector ℕ n_1 → ℕ
hf : Nat.Primrec' f_1
prim :
  ∃ (c : Code),
    ∀ (v : List.Vector ℕ 0), c.eval (↑v : List ℕ) = pure <$> (↑fun (x : List.Vector ℕ 0) ↦ 0 : List.Vector ℕ 0 →. ℕ) v
prim₁ :
  ∃ (c : Code),
    ∀ (v : List.Vector ℕ 1),
      c.eval (↑v : List ℕ) = pure <$> (↑fun (v : List.Vector ℕ 1) ↦ v.head.succ : List.Vector ℕ 1 →. ℕ) v
prim₂ :
  ∀ {n : ℕ} (i : Fin n),
    ∃ (c : Code),
      ∀ (v : List.Vector ℕ n),
        c.eval (↑v : List ℕ) = pure <$> (↑fun (v : List.Vector ℕ n) ↦ v.get i : List.Vector ℕ n →. ℕ) v
prim₃ :
  ∀ {m n : ℕ} {f : List.Vector ℕ n → ℕ} (g : Fin n → List.Vector ℕ m → ℕ) (hf : Nat.Primrec' f)
    (hg : ∀ (i : Fin n), Nat.Primrec' (g i))
    (IHf : ∃ (c : Code), ∀ (v : List.Vector ℕ n), c.eval (↑v : List ℕ) = pure <$> (↑f : List.Vector ℕ n →. ℕ) v)
    (IHg :
      ∀ (i : Fin n),
        ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> (↑(g i) : List.Vector ℕ m →. ℕ) v),
    ∃ (c : Code),
      ∀ (v : List.Vector ℕ m),
        c.eval (↑v : List ℕ) =
          pure <$> (↑fun (a : List.Vector ℕ m) ↦ f (List.Vector.ofFn fun (i : Fin n) ↦ g i a) : List.Vector ℕ m →. ℕ) v
prim₄ :
  ∀ {n : ℕ} {f : List.Vector ℕ n → ℕ} {g : List.Vector ℕ (n + 2) → ℕ},
    Nat.Primrec' f →
      Nat.Primrec' g →
        ∀ (IHf : ∃ (c : Code), ∀ (v : List.Vector ℕ n), c.eval (↑v : List ℕ) = pure <$> (↑f : List.Vector ℕ n →. ℕ) v)
          (IHg :
            ∃ (c : Code),
              ∀ (v : List.Vector ℕ (n + 2)), c.eval (↑v : List ℕ) = pure <$> (↑g : List.Vector ℕ (n + 2) →. ℕ) v),
          ∃ (c : Code),
            ∀ (v : List.Vector ℕ (n + 1)),
              c.eval (↑v : List ℕ) =
                pure <$>
                  (↑fun (v : List.Vector ℕ (n + 1)) ↦
                        Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail))
                          v.head :
                      List.Vector ℕ (n + 1) →. ℕ)
                    v
⊢ ∃ (c : Code), ∀ (v : List.Vector ℕ n_1), c.eval (↑v : List ℕ) = pure <$> (↑f_1 : List.Vector ℕ n_1 →. ℕ) v

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

Premises used: Pure.pure, Iff.mpr, List.Vector.tail_cons, List.Vector.cons_val, Part.eq_some_iff, Part.bind_some, Part.mem_some_iff, PFun.coe_val, MonadState.get, Part.map_eq_map, Turing.ToPartrec.Code.succ, List.tail_cons, Turing.ToPartrec.Code.prec, Part.bind_some_eq_map, Turing.ToPartrec.Code.comp, Turing.ToPartrec.Code.zero, List.Vector.head_cons, Part.map_some, Part.bind_assoc, Iff.mp, Bind.bind, Or.inl, PFun.mem_fix_iff, Part.pure_eq_some, List.Vector.tail_val, Part.bind_eq_bind, rfl