-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f_2 : List.Vector ℕ n_2 → ℕ
n_3 : ℕ
f : List.Vector ℕ n_3 → ℕ
g : List.Vector ℕ (n_3 + 2) → ℕ
h : Nat.Primrec' f
h_1 : Nat.Primrec' g
cf cg : Code
v : List.Vector ℕ (n_3 + 1)
hf : cf.eval (↑v : List ℕ).tail = pure (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (a :: b :: (↑v : List ℕ).tail) = pure (pure (g (a ::ᵥ b ::ᵥ v.tail)))
n : ℕ
h_2 :
  (cf.prec cg).eval (n :: (↑v : List ℕ).tail) =
    pure (pure (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n))
a b : ℕ
e : a + b = n
prim :
  ∀ (a : ℕ) (e : a + 0 = n),
    Membership.mem (γ := Part (List ℕ))
      (PFun.fix
        (fun (v : List ℕ) ↦
          (cg.eval (v.headI :: v.tail.tail)).bind fun (x : List ℕ) ↦
            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 (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a ::
              (↑v : List ℕ).tail))
      (n.succ ::
        0 ::
          g
              (n ::ᵥ
                Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ
                  v.tail) ::
            (↑v : List ℕ).tail)
prim₁ :
  ∀ (b : ℕ)
    (IH :
      ∀ (a : ℕ) (e : a + b = n),
        Membership.mem (γ := Part (List ℕ))
          (PFun.fix
            (fun (v : List ℕ) ↦
              (cg.eval (v.headI :: v.tail.tail)).bind fun (x : List ℕ) ↦
                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 ::
              b ::
                Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a ::
                  (↑v : List ℕ).tail))
          (n.succ ::
            0 ::
              g
                  (n ::ᵥ
                    Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ
                      v.tail) ::
                (↑v : List ℕ).tail))
    (a : ℕ) (e : a + (b + 1) = n),
    Membership.mem (γ := Part (List ℕ))
      (PFun.fix
        (fun (v : List ℕ) ↦
          (cg.eval (v.headI :: v.tail.tail)).bind fun (x : List ℕ) ↦
            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 ::
          (b + 1) ::
            Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a ::
              (↑v : List ℕ).tail))
      (n.succ ::
        0 ::
          g
              (n ::ᵥ
                Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ
                  v.tail) ::
            (↑v : List ℕ).tail)
⊢ Membership.mem (γ := Part (List ℕ))
    (PFun.fix
      (fun (v : List ℕ) ↦
        (cg.eval (v.headI :: v.tail.tail)).bind fun (x : List ℕ) ↦
          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 ::
        b ::
          Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a ::
            (↑v : List ℕ).tail))
    (n.succ ::
      0 ::
        g
            (n ::ᵥ
              Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ v.tail) ::
          (↑v : List ℕ).tail)

Tactic:
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, Part.eq_some_iff, Part.bind_some, Part.mem_some_iff, Turing.ToPartrec.Code.succ, List.tail_cons, Turing.ToPartrec.Code.zero, Iff.mp, Or.inl, PFun.mem_fix_iff, rfl