-- Module: Mathlib.Computability.PartrecCode
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_2 : Primrec (β := ℕ) fun (a : (List (List (Option ℕ)) × ℕ) × ℕ) ↦ (ofNat (ℕ × Code) a.1.1.length).1
n_2 : 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
L_1 :
  Primrec (β := List (List (Option ℕ)))
    fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) ↦ a.1.1.1
k :
  Primrec (β := ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) ↦
    (ofNat (ℕ × Code) a.1.1.1.length).1
n : Primrec (β := ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) ↦ a.1.1.2
cf : Primrec (β := Code) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) ↦ a.2.1
cg : Primrec (β := Code) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) ↦ a.2.2.1
z_1 :
  Primrec (β := ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) ↦ (unpair a.1.1.2).1
L :
  Primrec (β := List (List (Option ℕ)))
    fun (a : (((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ) ↦ a.1.1.1.1
z_2 :
  Primrec (β := ℕ) fun (a : (((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ) ↦
    (unpair a.1.1.1.2).1
y_1 : Primrec (α := (((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ) Prod.snd
h₁ :
  Primrec (β := Option ℕ) fun (a : (((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ) ↦
    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 : ((((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ) × ℕ) ↦
    (unpair a.1.1.1.1.2).1
y :
  Primrec (β := ℕ) fun (a : ((((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ) × ℕ) ↦ a.1.2
i : Primrec (α := ((((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ) × ℕ) Prod.snd
⊢ Primrec (β := Option ℕ) fun (a : ((((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ) × ℕ) ↦
    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

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