-- Mathlib/Computability/PartrecCode.lean
theorem evaln_prim : Primrec fun a : (ℕ × Code) × ℕ => evaln a.1.1 a.1.2 a.2 :=
  have :
    Primrec₂ fun (_ : Unit) (n : ℕ) =>
      let a := ofNat (ℕ × Code) n
      (List.range a.1).map (evaln a.1 a.2) :=
    Primrec.nat_strong_rec _ (hG.comp Primrec.snd).to₂ fun _ p => by
      simp only [G, prod_ofNat_val, ofNat_nat, List.length_map, List.length_range,
        Nat.pair_unpair, Option.some_inj]
      refine List.map_congr_left fun n => ?_
      have : List.range p = List.range (Nat.pair p.unpair.1 (encode (ofNat Code p.unpair.2)))

Proof state:
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k : ℕ
c : Code
⊢ n ∈ List.range k →
    Nat.rec Option.none
        (fun n_1 n_ih =>
          rec (some 0) (some n.succ) (some (unpair n).1) (some (unpair n).2)
            (fun cf cg x x => do
              let x ←
                Nat.Partrec.Code.lup
                    (List.map
                      (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                      (List.range (Nat.pair k (encode c))))
                    (k, cf) n
              let y ←
                Nat.Partrec.Code.lup
                    (List.map
                      (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                      (List.range (Nat.pair k (encode c))))
                    (k, cg) n
              some (Nat.pair x y))
            (fun cf cg x x => do
              let x ←
                Nat.Partrec.Code.lup
                    (List.map
                      (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                      (List.range (Nat.pair k (encode c))))
                    (k, cg) n
              Nat.Partrec.Code.lup
                  (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                    (List.range (Nat.pair k (encode c))))
                  (k, cf) x)
            (fun cf cg x x =>
              Nat.rec
                (Nat.Partrec.Code.lup
                  (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                    (List.range (Nat.pair k (encode c))))
                  (k, cf) (unpair n).1)
                (fun n_2 n_ih => do
                  let i ←
                    Nat.Partrec.Code.lup
                        (List.map
                          (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                          (List.range (Nat.pair k (encode c))))
                        (n_1, c) (Nat.pair (unpair n).1 n_2)
                  Nat.Partrec.Code.lup
                      (List.map
                        (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                        (List.range (Nat.pair k (encode c))))
                      (k, cg) (Nat.pair (unpair n).1 (Nat.pair n_2 i)))
                (unpair n).2)
            (fun cf x => do
              let x ←
                Nat.Partrec.Code.lup
                    (List.map
                      (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                      (List.range (Nat.pair k (encode c))))
                    (k, cf) n
              Nat.rec (some (unpair n).2)
                  (fun n_2 n_ih =>
                    Nat.Partrec.Code.lup
                      (List.map
                        (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                        (List.range (Nat.pair k (encode c))))
                      (n_1, c) (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
                  x)
            c)
        k =
      evaln k c n

Tactic:
intro nk

Result:
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k : ℕ
c : Code
nk : n ∈ List.range k
⊢ Nat.rec Option.none
      (fun n_1 n_ih =>
        rec (some 0) (some n.succ) (some (unpair n).1) (some (unpair n).2)
          (fun cf cg x x => do
            let x ←
              Nat.Partrec.Code.lup
                  (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                    (List.range (Nat.pair k (encode c))))
                  (k, cf) n
            let y ←
              Nat.Partrec.Code.lup
                  (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                    (List.range (Nat.pair k (encode c))))
                  (k, cg) n
            some (Nat.pair x y))
          (fun cf cg x x => do
            let x ←
              Nat.Partrec.Code.lup
                  (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                    (List.range (Nat.pair k (encode c))))
                  (k, cg) n
            Nat.Partrec.Code.lup
                (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                  (List.range (Nat.pair k (encode c))))
                (k, cf) x)
          (fun cf cg x x =>
            Nat.rec
              (Nat.Partrec.Code.lup
                (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                  (List.range (Nat.pair k (encode c))))
                (k, cf) (unpair n).1)
              (fun n_2 n_ih => do
                let i ←
                  Nat.Partrec.Code.lup
                      (List.map
                        (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                        (List.range (Nat.pair k (encode c))))
                      (n_1, c) (Nat.pair (unpair n).1 n_2)
                Nat.Partrec.Code.lup
                    (List.map
                      (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                      (List.range (Nat.pair k (encode c))))
                    (k, cg) (Nat.pair (unpair n).1 (Nat.pair n_2 i)))
              (unpair n).2)
          (fun cf x => do
            let x ←
              Nat.Partrec.Code.lup
                  (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                    (List.range (Nat.pair k (encode c))))
                  (k, cf) n
            Nat.rec (some (unpair n).2)
                (fun n_2 n_ih =>
                  Nat.Partrec.Code.lup
                    (List.map
                      (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                      (List.range (Nat.pair k (encode c))))
                    (n_1, c) (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
                x)
          c)
      k =
    evaln k c n