Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case succ
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
c : Code
k' : ℕ
nk : n ∈ List.range (k' + 1)
k : ℕ := k' + 1
⊢ rec (some 0) (some n.succ) (some (unpair n).1) (some (unpair n).2)
      (fun cf cg x x_1 ↦ do
        let x ←
          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 c))))
              (k' + 1, cf) n
        let y ←
          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 c))))
              (k' + 1, cg) n
        some (Nat.pair x y))
      (fun cf cg x x_1 ↦ do
        let x ←
          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 c))))
              (k' + 1, cg) n
        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 c))))
            (k' + 1, cf) x)
      (fun cf cg x x_1 ↦
        Nat.rec
          (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 c))))
            (k' + 1, cf) (unpair n).1)
          (fun n_1 n_ih ↦ do
            let i ←
              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 c))))
                  (k', c) (Nat.pair (unpair n).1 n_1)
            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 c))))
                (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
          (unpair n).2)
      (fun cf x ↦ do
        let x ←
          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 c))))
              (k' + 1, cf) n
        Nat.rec (some (unpair n).2)
            (fun n_1 n_ih ↦
              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 c))))
                (k', c) (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
            x)
      c =
    evaln (k' + 1) c n

Tactic:
simp only [List.mem_range, Nat.lt_succ_iff] at nk

Goal state after:
case succ
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'
⊢ rec (some 0) (some n.succ) (some (unpair n).1) (some (unpair n).2)
      (fun cf cg x x_1 ↦ do
        let x ←
          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 c))))
              (k' + 1, cf) n
        let y ←
          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 c))))
              (k' + 1, cg) n
        some (Nat.pair x y))
      (fun cf cg x x_1 ↦ do
        let x ←
          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 c))))
              (k' + 1, cg) n
        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 c))))
            (k' + 1, cf) x)
      (fun cf cg x x_1 ↦
        Nat.rec
          (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 c))))
            (k' + 1, cf) (unpair n).1)
          (fun n_1 n_ih ↦ do
            let i ←
              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 c))))
                  (k', c) (Nat.pair (unpair n).1 n_1)
            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 c))))
                (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
          (unpair n).2)
      (fun cf x ↦ do
        let x ←
          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 c))))
              (k' + 1, cf) n
        Nat.rec (some (unpair n).2)
            (fun n_1 n_ih ↦
              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 c))))
                (k', c) (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
            x)
      c =
    evaln (k' + 1) c n