-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
a : Primrec (β := ℕ × Code) fun (a : List (List (Option ℕ))) ↦ ofNat (ℕ × Code) a.length
k : Primrec (β := ℕ) fun (a : List (List (Option ℕ)) × ℕ) ↦ (ofNat (ℕ × Code) a.1.length).1
n : Primrec (α := List (List (Option ℕ)) × ℕ) Prod.snd
⊢ Primrec (β := Option ℕ) fun (p : List (List (Option ℕ)) × ℕ) ↦
    (fun (a : List (List (Option ℕ))) (n : ℕ) ↦
        (Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) (ofNat (ℕ × Code) a.length).1 Option.none fun (k' : ℕ) ↦
            Code.recOn (motive := fun (x : Code) ↦ Option ℕ) (ofNat (ℕ × Code) a.length).2 (some 0) (some n.succ)
              (some (unpair n).1) (some (unpair n).2)
              (fun (cf cg : Code) (x x_1 : Option ℕ) ↦ do
                let x ← lup a ((ofNat (ℕ × Code) a.length).1, cf) n
                let y ← lup a ((ofNat (ℕ × Code) a.length).1, cg) n
                some (Nat.pair x y))
              (fun (cf cg : Code) (x x_1 : Option ℕ) ↦ do
                let x ← lup a ((ofNat (ℕ × Code) a.length).1, cg) n
                lup a ((ofNat (ℕ × Code) a.length).1, cf) x)
              (fun (cf cg : Code) (x x_1 : Option ℕ) ↦
                have z := (unpair n).1;
                Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) (unpair n).2
                  (lup a ((ofNat (ℕ × Code) a.length).1, cf) z) fun (y : ℕ) ↦ do
                  let i ← lup a (k', (ofNat (ℕ × Code) a.length).2) (Nat.pair z y)
                  lup a ((ofNat (ℕ × Code) a.length).1, cg) (Nat.pair z (Nat.pair y i)))
              fun (cf : Code) (x : Option ℕ) ↦
              have z := (unpair n).1;
              have m := (unpair n).2;
              do
              let x ← lup a ((ofNat (ℕ × Code) a.length).1, cf) (Nat.pair z m)
              Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) x (some m) fun (x : ℕ) ↦
                  lup a (k', (ofNat (ℕ × Code) a.length).2) (Nat.pair z (m + 1)) :
          Option ℕ))
      p.1 p.2
have refine : Primrec (β := Option ℕ) fun (p : (List (List (Option ℕ)) × ℕ) × ℕ) ↦
  (fun (p : List (List (Option ℕ)) × ℕ) (k' : ℕ) ↦
      (Code.recOn (motive := fun (x : Code) ↦ Option ℕ) (ofNat (ℕ × Code) p.1.length).2 (some 0) (some p.2.succ)
          (some (unpair p.2).1) (some (unpair p.2).2)
          (fun (cf cg : Code) (x x_1 : Option ℕ) ↦ do
            let x ← lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) p.2
            let y ← lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) p.2
            some (Nat.pair x y))
          (fun (cf cg : Code) (x x_1 : Option ℕ) ↦ do
            let x ← lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) p.2
            lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) x)
          (fun (cf cg : Code) (x x_1 : Option ℕ) ↦
            have z := (unpair p.2).1;
            Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) (unpair p.2).2
              (lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) z) fun (y : ℕ) ↦ do
              let i ← lup p.1 (k', (ofNat (ℕ × Code) p.1.length).2) (Nat.pair z y)
              lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) (Nat.pair z (Nat.pair y i)))
          fun (cf : Code) (x : Option ℕ) ↦
          have z := (unpair p.2).1;
          have m := (unpair p.2).2;
          do
          let x ← lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) (Nat.pair z m)
          Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) x (some m) fun (x : ℕ) ↦
              lup p.1 (k', (ofNat (ℕ × Code) p.1.length).2) (Nat.pair z (m + 1)) :
        Option ℕ))
    p.1 p.2
Tactic: refine Primrec.nat_casesOn k (_root_.Primrec.const Option.none) (?_ : Primrec _)