awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  Primrec (β := ℕ) fun (a : (((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ) ↦
    (unpair a.1.1.1.2).1
y : 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
⊢ Primrec (β := Option ℕ) fun (p : (((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ) ↦
    (fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) (y : ℕ) ↦
        (do
          let i ← 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)
          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)) :
          Option ℕ))
      p.1 p.2

Tactic:
Primrec.option_bind h₁ (?_ : Primrec _)

Premises used: Primrec.option_bind
-- 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 :
  Primrec (β := ℕ) fun (a : (((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ) ↦
    (unpair a.1.1.1.2).1
y : 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
⊢ Primrec (β := ℕ) fun (a : ((((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ) × ℕ) ↦
    (unpair a.1.1.1.1.2).1

Tactic:
have z := z.comp (Primrec.fst (β := ℕ))
-- 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 : 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
⊢ Primrec (β := ℕ) fun (a : ((((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ) × ℕ) ↦ a.1.2

Tactic:
have y := y.comp (Primrec.fst (β := ℕ))
-- 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
⊢ Primrec (α := ((((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ) × ℕ) Prod.snd

Tactic:
have i := Primrec.snd
      (α := (((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ)
      (β := ℕ)
-- 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 : 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
⊢ Primrec (β := List (List (Option ℕ))) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ a.1.1.1

Tactic:
have L := (Primrec.fst.comp Primrec.fst).comp
      (Primrec.fst (α := (List (List (Option ℕ)) × ℕ) × ℕ)
        (β := Code × Option ℕ))
-- 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 : 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
L : Primrec (β := List (List (Option ℕ))) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ a.1.1.1
⊢ Primrec (β := ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ (ofNat (ℕ × Code) a.1.1.1.length).1

Tactic:
have k := k.comp (Primrec.fst (β := Code × Option ℕ))
-- 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 : 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 : Primrec (β := List (List (Option ℕ))) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ a.1.1.1
k :
  Primrec (β := ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ (ofNat (ℕ × Code) a.1.1.1.length).1
⊢ Primrec (β := ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ a.1.1.2

Tactic:
have n := n.comp (Primrec.fst (β := Code × Option ℕ))
-- 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 : Primrec (β := List (List (Option ℕ))) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ a.1.1.1
k :
  Primrec (β := ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ (ofNat (ℕ × Code) a.1.1.1.length).1
n : Primrec (β := ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ a.1.1.2
⊢ Primrec (β := Code) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ a.2.1

Tactic:
have cf := Primrec.fst.comp (Primrec.snd (α := (List (List (Option ℕ)) × ℕ) × ℕ)
        (β := Code × Option ℕ))
-- 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 : Primrec (β := List (List (Option ℕ))) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ a.1.1.1
k :
  Primrec (β := ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ (ofNat (ℕ × Code) a.1.1.1.length).1
n : Primrec (β := ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ a.1.1.2
cf : Primrec (β := Code) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ a.2.1
⊢ Primrec (β := ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ (unpair a.1.1.2).1

Tactic:
have z := Primrec.fst.comp (Primrec.unpair.comp n)
-- 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 : Primrec (β := List (List (Option ℕ))) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ a.1.1.1
k :
  Primrec (β := ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ (ofNat (ℕ × Code) a.1.1.1.length).1
n : Primrec (β := ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ a.1.1.2
cf : Primrec (β := Code) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ a.2.1
z : Primrec (β := ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ (unpair a.1.1.2).1
⊢ Primrec (β := ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ (unpair a.1.1.2).2

Tactic:
have m := Primrec.snd.comp (Primrec.unpair.comp n)
-- 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 : Primrec (β := List (List (Option ℕ))) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ a.1.1.1
k :
  Primrec (β := ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ (ofNat (ℕ × Code) a.1.1.1.length).1
n : Primrec (β := ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ a.1.1.2
cf : Primrec (β := Code) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ a.2.1
z : Primrec (β := ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ (unpair a.1.1.2).1
m : Primrec (β := ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ (unpair a.1.1.2).2
⊢ Primrec (β := Option ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦
    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

Tactic:
have h₁ := hlup.comp <| L.pair <| (k.pair cf).pair (Primrec₂.natPair.comp z m)
-- 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 : Primrec (β := List (List (Option ℕ))) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ a.1.1.1
k :
  Primrec (β := ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ (ofNat (ℕ × Code) a.1.1.1.length).1
n : Primrec (β := ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ a.1.1.2
cf : Primrec (β := Code) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ a.2.1
z : Primrec (β := ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ (unpair a.1.1.2).1
m : Primrec (β := ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ (unpair a.1.1.2).2
h₁ :
  Primrec (β := Option ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦
    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
⊢ Primrec (β := Option ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦
    have z := (unpair a.1.1.2).1;
    have m := (unpair a.1.1.2).2;
    do
    let x ← lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) (Nat.pair z m)
    Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) x (some m) fun (x : ℕ) ↦
        lup a.1.1.1 (a.1.2, (ofNat (ℕ × Code) a.1.1.1.length).2) (Nat.pair z (m + 1))

Tactic:
Primrec.option_bind h₁ (?_ : Primrec _)

Premises used: Primrec.option_bind
-- 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 : Primrec (β := List (List (Option ℕ))) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ a.1.1.1
k :
  Primrec (β := ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ (ofNat (ℕ × Code) a.1.1.1.length).1
n : Primrec (β := ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ a.1.1.2
cf : Primrec (β := Code) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ a.2.1
z : Primrec (β := ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ (unpair a.1.1.2).1
m : Primrec (β := ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ (unpair a.1.1.2).2
h₁ :
  Primrec (β := Option ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦
    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
hrf :
  Primrec (β := Option ℕ) fun (p : (((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) × ℕ) ↦
    (fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) (x : ℕ) ↦
        (Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) x (some (unpair a.1.1.2).2) fun (x : ℕ) ↦
            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)) :
          Option ℕ))
      p.1 p.2
⊢ Primrec (β := Option ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦
    have z := (unpair a.1.1.2).1;
    have m := (unpair a.1.1.2).2;
    do
    let x ← lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) (Nat.pair z m)
    Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) x (some m) fun (x : ℕ) ↦
        lup a.1.1.1 (a.1.2, (ofNat (ℕ × Code) a.1.1.1.length).2) (Nat.pair z (m + 1))

Tactic:
refine Primrec.option_bind h₁ (?_ : Primrec _)

Premises used: Primrec.option_bind