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)))
⊢ n ∈ List.range (unpair p).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 (unpair p).1 (encode (ofNat Code (unpair p).2)))))
                    ((unpair p).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 (unpair p).1 (encode (ofNat Code (unpair p).2)))))
                    ((unpair p).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 (unpair p).1 (encode (ofNat Code (unpair p).2)))))
                    ((unpair p).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 (unpair p).1 (encode (ofNat Code (unpair p).2)))))
                  ((unpair p).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 (unpair p).1 (encode (ofNat Code (unpair p).2)))))
                  ((unpair p).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 (unpair p).1 (encode (ofNat Code (unpair p).2)))))
                        (n_1, ofNat Code (unpair p).2) (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 (unpair p).1 (encode (ofNat Code (unpair p).2)))))
                      ((unpair p).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 (unpair p).1 (encode (ofNat Code (unpair p).2)))))
                    ((unpair p).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 (unpair p).1 (encode (ofNat Code (unpair p).2)))))
                      (n_1, ofNat Code (unpair p).2) (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
                  x)
            (ofNat Code (unpair p).2))
        (unpair p).1 =
      evaln (unpair p).1 (ofNat Code (unpair p).2) n

Tactic:
generalize p.unpair.1 = k

Goal state after:
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k : ℕ
⊢ 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 (ofNat Code (unpair p).2)))))
                    (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 (ofNat Code (unpair p).2)))))
                    (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 (ofNat Code (unpair p).2)))))
                    (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 (ofNat Code (unpair p).2)))))
                  (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 (ofNat Code (unpair p).2)))))
                  (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 (ofNat Code (unpair p).2)))))
                        (n_1, ofNat Code (unpair p).2) (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 (ofNat Code (unpair p).2)))))
                      (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 (ofNat Code (unpair p).2)))))
                    (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 (ofNat Code (unpair p).2)))))
                      (n_1, ofNat Code (unpair p).2) (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
                  x)
            (ofNat Code (unpair p).2))
        k =
      evaln k (ofNat Code (unpair p).2) n