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

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
n : Primrec fun a => a.1.1.2
cf : Primrec fun a => a.2.1
z : Primrec fun a => (unpair a.1.1.2).1
m✝ : Primrec fun a => (unpair a.1.1.2).2
h₁ :
  Primrec fun a =>
    Nat.Partrec.Code.lup
      (a.1.1.1, ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1), Nat.pair (unpair a.1.1.2).1 (unpair a.1.1.2).2).1
      (a.1.1.1, ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1), Nat.pair (unpair a.1.1.2).1 (unpair a.1.1.2).2).2.1
      (a.1.1.1, ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1), Nat.pair (unpair a.1.1.2).1 (unpair a.1.1.2).2).2.2
m : Primrec fun a => (unpair a.1.1.1.2).2
⊢ Primrec fun p =>
    (fun a x =>
        Nat.casesOn x (some (unpair a.1.1.2).2) fun x =>
          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 ((unpair a.1.1.2).2 + 1)))
      p.1 p.2

Tactic:
refine Primrec.nat_casesOn Primrec.snd (Primrec.option_some.comp m) ?_

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
cf : Primrec fun a => a.2.1
z : Primrec fun a => (unpair a.1.1.2).1
m✝ : Primrec fun a => (unpair a.1.1.2).2
h₁ :
  Primrec fun a =>
    Nat.Partrec.Code.lup
      (a.1.1.1, ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1), Nat.pair (unpair a.1.1.2).1 (unpair a.1.1.2).2).1
      (a.1.1.1, ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1), Nat.pair (unpair a.1.1.2).1 (unpair a.1.1.2).2).2.1
      (a.1.1.1, ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1), Nat.pair (unpair a.1.1.2).1 (unpair a.1.1.2).2).2.2
m : Primrec fun a => (unpair a.1.1.1.2).2
⊢ Primrec₂ fun p x =>
    Nat.Partrec.Code.lup p.1.1.1.1 (p.1.1.2, (ofNat (ℕ × Code) p.1.1.1.1.length).2)
      (Nat.pair (unpair p.1.1.1.2).1 ((unpair p.1.1.1.2).2 + 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 p =>
    Option.map (Nat.pair p.2)
      (Nat.Partrec.Code.lup p.1.1.1.1 ((ofNat (ℕ × Code) p.1.1.1.1.length).1, p.1.2.2.1) p.1.1.1.2)

Tactic:
refine Primrec.option_map ((hlup.comp <| L.pair <| (k.pair cg).pair n).comp Primrec.fst) ?_

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 p => Nat.pair p.2

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
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
z : Primrec fun a => (unpair a.1.1.1.1.2).1
y : Primrec fun a => a.1.2
i : Primrec Prod.snd
h₂ :
  Primrec fun a =>
    Nat.Partrec.Code.lup
      (a.1.1.1.1.1, ((ofNat (ℕ × Code) a.1.1.1.1.1.length).1, a.1.1.2.2.1),
          Nat.pair (unpair a.1.1.1.1.2).1 (Nat.pair a.1.2 a.2)).1
      (a.1.1.1.1.1, ((ofNat (ℕ × Code) a.1.1.1.1.1.length).1, a.1.1.2.2.1),
            Nat.pair (unpair a.1.1.1.1.2).1 (Nat.pair a.1.2 a.2)).2.1
      (a.1.1.1.1.1, ((ofNat (ℕ × Code) a.1.1.1.1.1.length).1, a.1.1.2.2.1),
            Nat.pair (unpair a.1.1.1.1.2).1 (Nat.pair a.1.2 a.2)).2.2
⊢ Primrec fun p =>
    (fun p i =>
        Nat.Partrec.Code.lup p.1.1.1.1 ((ofNat (ℕ × Code) p.1.1.1.1.length).1, p.1.2.2.1)
          (Nat.pair (unpair p.1.1.1.2).1 (Nat.pair p.2 i)))
      p.1 p.2

Tactic:
exact h₂

Result:
no goals