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

Proof state:
case hco
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
⊢ Primrec fun a => do
    let x ← Nat.Partrec.Code.lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.2.1) a.1.1.2
    Nat.Partrec.Code.lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) x

Tactic:
have L := (Primrec.fst.comp Primrec.fst).comp
  (Primrec.fst (α := (List (List (Option ℕ)) × ℕ) × ℕ)
    (β := Code × Code × Option ℕ × Option ℕ))

Result:
case hco
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
⊢ Primrec fun a => do
    let x ← Nat.Partrec.Code.lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.2.1) a.1.1.2
    Nat.Partrec.Code.lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) x

Proof state:
case hco
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
⊢ Primrec fun a => do
    let x ← Nat.Partrec.Code.lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.2.1) a.1.1.2
    Nat.Partrec.Code.lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) x

Tactic:
have cg := (Primrec.fst.comp Primrec.snd).comp
  (Primrec.snd (α := (List (List (Option ℕ)) × ℕ) × ℕ)
    (β := Code × Code × Option ℕ × Option ℕ))

Result:
case hco
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.2.1) a.1.1.2
    Nat.Partrec.Code.lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) x

Proof state:
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
⊢ Primrec fun p =>
    (fun p k' =>
        Code.recOn (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 x x => do
            let x ← Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) p.2
            let y ← Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) p.2
            some (Nat.pair x y))
          (fun cf cg x x => do
            let x ← Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) p.2
            Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) x)
          (fun cf cg x x =>
            let z := (unpair p.2).1;
            Nat.casesOn (unpair p.2).2 (Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) z) fun y => do
              let i ← Nat.Partrec.Code.lup p.1 (k', (ofNat (ℕ × Code) p.1.length).2) (Nat.pair z y)
              Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) (Nat.pair z (Nat.pair y i)))
          fun cf x =>
          let z := (unpair p.2).1;
          let m := (unpair p.2).2;
          do
          let x ← Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) (Nat.pair z m)
          Nat.casesOn x (some m) fun x =>
              Nat.Partrec.Code.lup p.1 (k', (ofNat (ℕ × Code) p.1.length).2) (Nat.pair z (m + 1)))
      p.1 p.2

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

Result:
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
⊢ Primrec fun p =>
    (fun p k' =>
        Code.recOn (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 x x => do
            let x ← Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) p.2
            let y ← Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) p.2
            some (Nat.pair x y))
          (fun cf cg x x => do
            let x ← Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) p.2
            Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) x)
          (fun cf cg x x =>
            let z := (unpair p.2).1;
            Nat.casesOn (unpair p.2).2 (Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) z) fun y => do
              let i ← Nat.Partrec.Code.lup p.1 (k', (ofNat (ℕ × Code) p.1.length).2) (Nat.pair z y)
              Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) (Nat.pair z (Nat.pair y i)))
          fun cf x =>
          let z := (unpair p.2).1;
          let m := (unpair p.2).2;
          do
          let x ← Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) (Nat.pair z m)
          Nat.casesOn x (some m) fun x =>
              Nat.Partrec.Code.lup p.1 (k', (ofNat (ℕ × Code) p.1.length).2) (Nat.pair z (m + 1)))
      p.1 p.2