-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
a : Primrec (β := ℕ × Code) fun (a : List (List (Option ℕ))) ↦ ofNat (ℕ × Code) a.length
k_1 : Primrec (β := ℕ) fun (a : List (List (Option ℕ)) × ℕ) ↦ (ofNat (ℕ × Code) a.1.length).1
n_1 : Primrec (α := List (List (Option ℕ)) × ℕ) Prod.snd
k : Primrec (β := ℕ) fun (a : (List (List (Option ℕ)) × ℕ) × ℕ) ↦ (ofNat (ℕ × Code) a.1.1.length).1
n : Primrec (β := ℕ) fun (a : (List (List (Option ℕ)) × ℕ) × ℕ) ↦ a.1.2
k' : Primrec (α := (List (List (Option ℕ)) × ℕ) × ℕ) Prod.snd
c : Primrec (β := Code) fun (a : (List (List (Option ℕ)) × ℕ) × ℕ) ↦ (ofNat (ℕ × Code) a.1.1.length).2
hpr :
  Primrec (β := Option ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) ↦ do
    let x ← lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) a.1.1.2
    let y ← lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.2.1) a.1.1.2
    some (Nat.pair x y)
hco :
  Primrec (β := Option ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) ↦ do
    let x ← lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.2.1) a.1.1.2
    lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) x
⊢ 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
have hpc : Primrec (β := Option ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) ↦
  have z := (unpair a.1.1.2).1;
  Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) (unpair a.1.1.2).2
    (lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) z) fun (y : ℕ) ↦ do
    let i ← lup a.1.1.1 (a.1.2, (ofNat (ℕ × Code) a.1.1.1.length).2) (Nat.pair z y)
    lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.2.1) (Nat.pair z (Nat.pair y i))
Tactic: apply
    Nat.Partrec.Code.primrec_recOn c
      (_root_.Primrec.const (some 0))
      (Primrec.option_some.comp (_root_.Primrec.succ.comp n))
      (Primrec.option_some.comp (Primrec.fst.comp <| Primrec.unpair.comp n))
      (Primrec.option_some.comp (Primrec.snd.comp <| Primrec.unpair.comp n))