Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: 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_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 (encode c))))
                  (k, 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 (encode c))))
                  (k, 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 (encode c))))
                  (k, 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 (encode c))))
                (k, 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 (encode c))))
                (k, cf) (unpair n).1)
              (fun n_2 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 (encode c))))
                      (n_1, c) (Nat.pair (unpair n).1 n_2)
                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 ←
              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 ↦
                  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:
rcases k with - | k'

Goal state after:
case zero
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
c : Code
nk : n ∈ List.range 0
⊢ 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_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 0 (encode c))))
                  (0, 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 0 (encode c))))
                  (0, 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 0 (encode c))))
                  (0, 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 0 (encode c))))
                (0, 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 0 (encode c))))
                (0, cf) (unpair n).1)
              (fun n_2 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 0 (encode c))))
                      (n_1, c) (Nat.pair (unpair n).1 n_2)
                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 0 (encode c))))
                    (0, cg) (Nat.pair (unpair n).1 (Nat.pair n_2 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 0 (encode c))))
                  (0, cf) n
            Nat.rec (some (unpair n).2)
                (fun n_2 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 0 (encode c))))
                    (n_1, c) (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
                x)
          c)
      0 =
    evaln 0 c n

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)
⊢ 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_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_2 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))))
                      (n_1, c) (Nat.pair (unpair n).1 n_2)
                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_2 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_2 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))))
                    (n_1, c) (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
                x)
          c)
      (k' + 1) =
    evaln (k' + 1) c n