-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
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)) →
      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)
succ :
  Eq (α := Option ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln k cf (unpair n).1)
        (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
          (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 : ℕ) ↦
            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 :
      Option ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k' + 1) cf (unpair n).1)
        (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
          (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 :
      Option ℕ)
⊢ Eq (α := Option ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln k cf (unpair n).1)
        (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
          (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 : ℕ) ↦
            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 :
      Option ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k' + 1) cf (unpair n).1)
        (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
          (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 :
      Option ℕ)
have succ₁ : ∀ (n_1 : ℕ),
  Eq (α := Option ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln k cf (unpair n).1)
        (fun (n_2 : ℕ) (n_ih : Option ℕ) ↦
          (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_2)).bind
            fun (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 (cf.prec cg)))))
              (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_2 i)))
        (n_1 + 1) :
      Option ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k' + 1) cf (unpair n).1)
        (fun (n_2 : ℕ) (n_ih : Option ℕ) ↦
          (evaln k' (cf.prec cg) (Nat.pair (unpair n).1 n_2)).bind fun (i : ℕ) ↦
            evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_2 i)))
        (n_1 + 1) :
      Option ℕ)
Tactic: cases n.unpair.2