-- Module: Mathlib.Computability.PartrecCode
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
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
⊢ 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

Tactic:
refine Primrec.nat_casesOn k (_root_.Primrec.const Option.none) (?_ : Primrec _)

Premises used: Primrec.const, Option.none, Primrec.nat_casesOn