-- Mathlib/Computability/PartrecCode.lean
theorem hG : Primrec G

Proof state:
case hpc
a : Primrec fun a => ofNat (ℕ × Code) a.length
k✝¹ : Primrec fun a => (ofNat (ℕ × Code) a.1.length).1
n✝¹ : Primrec Prod.snd
k✝ : Primrec fun a => (ofNat (ℕ × Code) a.1.1.length).1
n✝ : Primrec fun a => a.1.2
k' : Primrec Prod.snd
c : Primrec fun a => (ofNat (ℕ × Code) a.1.1.length).2
L✝ : Primrec fun a => a.1.1.1
k : Primrec fun a => (ofNat (ℕ × Code) a.1.1.1.length).1
n : Primrec fun a => a.1.1.2
cf : Primrec fun a => a.2.1
cg : Primrec fun a => a.2.2.1
z✝ : Primrec fun a => (unpair a.1.1.2).1
L : Primrec fun a => a.1.1.1.1
z : Primrec fun a => (unpair a.1.1.1.2).1
y : Primrec Prod.snd
⊢ Primrec fun p =>
    (fun a y => do
        let i ←
          Nat.Partrec.Code.lup a.1.1.1 (a.1.2, (ofNat (ℕ × Code) a.1.1.1.length).2) (Nat.pair (unpair a.1.1.2).1 y)
        Nat.Partrec.Code.lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.2.1)
            (Nat.pair (unpair a.1.1.2).1 (Nat.pair y i)))
      p.1 p.2

Tactic:
have h₁ := hlup.comp <| L.pair <| (((k'.pair c).comp Primrec.fst).comp Primrec.fst).pair
  (Primrec₂.natPair.comp z y)

Result:
case hpc
a : Primrec fun a => ofNat (ℕ × Code) a.length
k✝¹ : Primrec fun a => (ofNat (ℕ × Code) a.1.length).1
n✝¹ : Primrec Prod.snd
k✝ : Primrec fun a => (ofNat (ℕ × Code) a.1.1.length).1
n✝ : Primrec fun a => a.1.2
k' : Primrec Prod.snd
c : Primrec fun a => (ofNat (ℕ × Code) a.1.1.length).2
L✝ : Primrec fun a => a.1.1.1
k : Primrec fun a => (ofNat (ℕ × Code) a.1.1.1.length).1
n : Primrec fun a => a.1.1.2
cf : Primrec fun a => a.2.1
cg : Primrec fun a => a.2.2.1
z✝ : Primrec fun a => (unpair a.1.1.2).1
L : Primrec fun a => a.1.1.1.1
z : Primrec fun a => (unpair a.1.1.1.2).1
y : Primrec Prod.snd
h₁ :
  Primrec fun a =>
    Nat.Partrec.Code.lup
      (a.1.1.1.1, (a.1.1.2, (ofNat (ℕ × Code) a.1.1.1.1.length).2), Nat.pair (unpair a.1.1.1.2).1 a.2).1
      (a.1.1.1.1, (a.1.1.2, (ofNat (ℕ × Code) a.1.1.1.1.length).2), Nat.pair (unpair a.1.1.1.2).1 a.2).2.1
      (a.1.1.1.1, (a.1.1.2, (ofNat (ℕ × Code) a.1.1.1.1.length).2), Nat.pair (unpair a.1.1.1.2).1 a.2).2.2
⊢ Primrec fun p =>
    (fun a y => do
        let i ←
          Nat.Partrec.Code.lup a.1.1.1 (a.1.2, (ofNat (ℕ × Code) a.1.1.1.length).2) (Nat.pair (unpair a.1.1.2).1 y)
        Nat.Partrec.Code.lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.2.1)
            (Nat.pair (unpair a.1.1.2).1 (Nat.pair y i)))
      p.1 p.2

Proof state:
case hrf
a : Primrec fun a => ofNat (ℕ × Code) a.length
k✝¹ : Primrec fun a => (ofNat (ℕ × Code) a.1.length).1
n✝ : Primrec Prod.snd
k✝ : Primrec fun a => (ofNat (ℕ × Code) a.1.1.length).1
n : Primrec fun a => a.1.2
k' : Primrec Prod.snd
c : Primrec fun a => (ofNat (ℕ × Code) a.1.1.length).2
L : Primrec fun a => a.1.1.1
k : Primrec fun a => (ofNat (ℕ × Code) a.1.1.1.length).1
⊢ Primrec fun a =>
    let z := (unpair a.1.1.2).1;
    let m := (unpair a.1.1.2).2;
    do
    let x ← Nat.Partrec.Code.lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) (Nat.pair z m)
    Nat.casesOn x (some m) fun x =>
        Nat.Partrec.Code.lup a.1.1.1 (a.1.2, (ofNat (ℕ × Code) a.1.1.1.length).2) (Nat.pair z (m + 1))

Tactic:
have n := n.comp (Primrec.fst (β := Code × Option ℕ))

Result:
case hrf
a : Primrec fun a => ofNat (ℕ × Code) a.length
k✝¹ : Primrec fun a => (ofNat (ℕ × Code) a.1.length).1
n✝¹ : Primrec Prod.snd
k✝ : Primrec fun a => (ofNat (ℕ × Code) a.1.1.length).1
n✝ : Primrec fun a => a.1.2
k' : Primrec Prod.snd
c : Primrec fun a => (ofNat (ℕ × Code) a.1.1.length).2
L : Primrec fun a => a.1.1.1
k : Primrec fun a => (ofNat (ℕ × Code) a.1.1.1.length).1
n : Primrec fun a => a.1.1.2
⊢ Primrec fun a =>
    let z := (unpair a.1.1.2).1;
    let m := (unpair a.1.1.2).2;
    do
    let x ← Nat.Partrec.Code.lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) (Nat.pair z m)
    Nat.casesOn x (some m) fun x =>
        Nat.Partrec.Code.lup a.1.1.1 (a.1.2, (ofNat (ℕ × Code) a.1.1.1.length).2) (Nat.pair z (m + 1))

Proof state:
case hpr
a : Primrec fun a => ofNat (ℕ × Code) a.length
k✝¹ : Primrec fun a => (ofNat (ℕ × Code) a.1.length).1
n✝¹ : Primrec Prod.snd
k✝ : Primrec fun a => (ofNat (ℕ × Code) a.1.1.length).1
n✝ : Primrec fun a => a.1.2
k' : Primrec Prod.snd
c : Primrec fun a => (ofNat (ℕ × Code) a.1.1.length).2
L : Primrec fun a => a.1.1.1
k : Primrec fun a => (ofNat (ℕ × Code) a.1.1.1.length).1
n : Primrec fun a => a.1.1.2
cf : Primrec fun a => a.2.1
cg : Primrec fun a => a.2.2.1
⊢ Primrec fun a => do
    let x ← Nat.Partrec.Code.lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) a.1.1.2
    let y ← Nat.Partrec.Code.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)

Tactic:
refine Primrec.option_bind (hlup.comp <| L.pair <| (k.pair cf).pair n) ?_

Result:
case hpr
a : Primrec fun a => ofNat (ℕ × Code) a.length
k✝¹ : Primrec fun a => (ofNat (ℕ × Code) a.1.length).1
n✝¹ : Primrec Prod.snd
k✝ : Primrec fun a => (ofNat (ℕ × Code) a.1.1.length).1
n✝ : Primrec fun a => a.1.2
k' : Primrec Prod.snd
c : Primrec fun a => (ofNat (ℕ × Code) a.1.1.length).2
L : Primrec fun a => a.1.1.1
k : Primrec fun a => (ofNat (ℕ × Code) a.1.1.1.length).1
n : Primrec fun a => a.1.1.2
cf : Primrec fun a => a.2.1
cg : Primrec fun a => a.2.2.1
⊢ Primrec₂ fun a x => do
    let y ← Nat.Partrec.Code.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)

Proof state:
case hpc
a : Primrec fun a => ofNat (ℕ × Code) a.length
k✝¹ : Primrec fun a => (ofNat (ℕ × Code) a.1.length).1
n✝¹ : Primrec Prod.snd
k✝ : Primrec fun a => (ofNat (ℕ × Code) a.1.1.length).1
n✝ : Primrec fun a => a.1.2
k' : Primrec Prod.snd
c : Primrec fun a => (ofNat (ℕ × Code) a.1.1.length).2
L : Primrec fun a => a.1.1.1
k : Primrec fun a => (ofNat (ℕ × Code) a.1.1.1.length).1
n : Primrec fun a => a.1.1.2
cf : Primrec fun a => a.2.1
cg : Primrec fun a => a.2.2.1
⊢ Primrec fun a =>
    let z := (unpair a.1.1.2).1;
    Nat.casesOn (unpair a.1.1.2).2 (Nat.Partrec.Code.lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) z)
      fun y => do
      let i ← Nat.Partrec.Code.lup a.1.1.1 (a.1.2, (ofNat (ℕ × Code) a.1.1.1.length).2) (Nat.pair z y)
      Nat.Partrec.Code.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:
have z := Primrec.fst.comp (Primrec.unpair.comp n)

Result:
case hpc
a : Primrec fun a => ofNat (ℕ × Code) a.length
k✝¹ : Primrec fun a => (ofNat (ℕ × Code) a.1.length).1
n✝¹ : Primrec Prod.snd
k✝ : Primrec fun a => (ofNat (ℕ × Code) a.1.1.length).1
n✝ : Primrec fun a => a.1.2
k' : Primrec Prod.snd
c : Primrec fun a => (ofNat (ℕ × Code) a.1.1.length).2
L : Primrec fun a => a.1.1.1
k : Primrec fun a => (ofNat (ℕ × Code) a.1.1.1.length).1
n : Primrec fun a => a.1.1.2
cf : Primrec fun a => a.2.1
cg : Primrec fun a => a.2.2.1
z : Primrec fun a => (unpair a.1.1.2).1
⊢ Primrec fun a =>
    let z := (unpair a.1.1.2).1;
    Nat.casesOn (unpair a.1.1.2).2 (Nat.Partrec.Code.lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) z)
      fun y => do
      let i ← Nat.Partrec.Code.lup a.1.1.1 (a.1.2, (ofNat (ℕ × Code) a.1.1.1.length).2) (Nat.pair z y)
      Nat.Partrec.Code.lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.2.1) (Nat.pair z (Nat.pair y i))