-- 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:
case succ.prec.intro
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.prec cg)) →
      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 (cf.prec cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.prec cg)
lg : encode cg < encode (cf.prec cg)
⊢ Nat.rec (evaln k cf (unpair n).1)
      (fun n_1 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' + 1) (encode (cf.prec cg)))))
              (k', cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind
          fun 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' + 1) (encode (cf.prec cg)))))
            (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
      (unpair n).2 =
    Nat.rec (evaln (k' + 1) cf (unpair n).1)
      (fun n_1 n_ih =>
        (evaln k' (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun i =>
          evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
      (unpair n).2

Tactic:
cases n.unpair.2

Result:
case succ.prec.intro.zero
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.prec cg)) →
      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 (cf.prec cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.prec cg)
lg : encode cg < encode (cf.prec cg)
⊢ Nat.rec (evaln k cf (unpair n).1)
      (fun n_1 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' + 1) (encode (cf.prec cg)))))
              (k', cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind
          fun 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' + 1) (encode (cf.prec cg)))))
            (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
      0 =
    Nat.rec (evaln (k' + 1) cf (unpair n).1)
      (fun n_1 n_ih =>
        (evaln k' (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun i =>
          evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
      0

case succ.prec.intro.succ
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.prec cg)) →
      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 (cf.prec cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.prec cg)
lg : encode cg < encode (cf.prec cg)
n✝ : ℕ
⊢ Nat.rec (evaln k cf (unpair n).1)
      (fun n_1 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' + 1) (encode (cf.prec cg)))))
              (k', cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind
          fun 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' + 1) (encode (cf.prec cg)))))
            (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
      (n✝ + 1) =
    Nat.rec (evaln (k' + 1) cf (unpair n).1)
      (fun n_1 n_ih =>
        (evaln k' (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun i =>
          evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
      (n✝ + 1)

Proof state:
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
c : Code
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
k₁ : ℕ
c₁ : Code
n₁ : ℕ
hl : Nat.pair k₁ (encode c₁) < Nat.pair k (encode c)
⊢ 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₁, c₁) n₁ =
    evaln k₁ c₁ n₁

Tactic:
simp [lup, List.getElem?_range hl, evaln_map, Bind.bind, Option.bind_map]

Result:
no goals

Proof state:
case succ.pair.intro
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.pair cg)) →
      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 (cf.pair cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.pair cg)
lg : encode cg < encode (cf.pair cg)
⊢ ((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' + 1) (encode (cf.pair cg)))))
          (k' + 1, cf) n).bind
      fun a =>
      (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' + 1) (encode (cf.pair cg)))))
            (k' + 1, cg) n).bind
        fun y => some (Nat.pair a y)) =
    (Option.map Nat.pair (evaln (k' + 1) cf n)).bind fun a => Option.map a (evaln (k' + 1) cg n)

Tactic:
rw [hg (Nat.pair_lt_pair_right _ lf), hg (Nat.pair_lt_pair_right _ lg)]

Result:
case succ.pair.intro
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.pair cg)) →
      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 (cf.pair cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.pair cg)
lg : encode cg < encode (cf.pair cg)
⊢ ((evaln k cf n).bind fun a => (evaln k cg n).bind fun y => some (Nat.pair a y)) =
    (Option.map Nat.pair (evaln (k' + 1) cf n)).bind fun a => Option.map a (evaln (k' + 1) cg n)