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 :
  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
⊢ Primrec (β := Code) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) ↦ a.2.1

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

Tactic:
have cg := (Primrec.fst.comp Primrec.snd).comp
      (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_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 × 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
⊢ Primrec (β := Option ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) ↦ do
    let x ← lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) a.1.1.2
    let y ← 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:
Primrec.option_bind (hlup.comp <| L.pair <| (k.pair cf).pair n) ?_

Premises used: Primrec.pair, _private.0.Nat.Partrec.Code.hlup, Primrec.comp, 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 × 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
hpr :
  Primrec₂ (σ := Option ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) (x : ℕ) ↦ do
    let y ← 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)
⊢ Primrec (β := Option ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) ↦ do
    let x ← lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) a.1.1.2
    let y ← 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) ?_

Premises used: Primrec.pair, _private.0.Nat.Partrec.Code.hlup, Primrec.comp, 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 × 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
f :
  fun (p : (((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ) ↦
    (fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) (x : ℕ) ↦
        (do
          let y ← 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) : Option ℕ))
      p.1 p.2
| Primrec (β := Option ℕ) fun (p : (((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ) ↦
    (fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) (x : ℕ) ↦
        (do
          let y ← 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) : Option ℕ))
      p.1 p.2

Tactic:
congr
-- 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 × 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
f :
  ∀ (p : (((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ),
    (fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) (x : ℕ) ↦
        (do
          let y ← 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) : Option ℕ))
      p.1 p.2
| fun (p : (((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ) ↦
    (fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) (x : ℕ) ↦
        (do
          let y ← 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) : Option ℕ))
      p.1 p.2

Tactic:
ext p
-- 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 × 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
p : (((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ
f : Option.map (Nat.pair p.2) (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)
| do
    let y ← 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
    some (Nat.pair p.2 y)

Tactic:
erw [Option.bind_eq_bind, ← Option.map_eq_bind]

Premises used: Option.map_eq_bind, Option.bind_eq_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 × 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
f :
  ∀ (p : (((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ),
    Option.map (Nat.pair p.2) (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)
| fun (p : (((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ) ↦
    (fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) (x : ℕ) ↦
        (do
          let y ← 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) : Option ℕ))
      p.1 p.2

Tactic:
ext p
        dsimp only []
        erw [Option.bind_eq_bind, ← Option.map_eq_bind]

Premises used: Option.map_eq_bind, Option.bind_eq_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 × 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
f :
  ∀ (p : (((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ),
    (fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) (x : ℕ) ↦
        (do
          let y ← 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) : Option ℕ))
      p.1 p.2
f₁ :
  ∀ (p : (((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ), do
    let y ← 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
    some (Nat.pair p.2 y)
f₂ :
  ∀ (p : (((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ),
    Option.map (Nat.pair p.2) (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)
| fun (p : (((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ) ↦
    (fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) (x : ℕ) ↦
        (do
          let y ← 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) : Option ℕ))
      p.1 p.2

Tactic:
· ext p
        dsimp only []
        erw [Option.bind_eq_bind, ← Option.map_eq_bind]

Premises used: Option.map_eq_bind, Option.bind_eq_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 × 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
f :
  fun (p : (((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ) ↦
    (fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) (x : ℕ) ↦
        (do
          let y ← 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) : Option ℕ))
      p.1 p.2
| Primrec (β := Option ℕ) fun (p : (((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ) ↦
    (fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) (x : ℕ) ↦
        (do
          let y ← 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) : Option ℕ))
      p.1 p.2

Tactic:
congr
      · ext p
        dsimp only []
        erw [Option.bind_eq_bind, ← Option.map_eq_bind]

Premises used: Option.map_eq_bind, Option.bind_eq_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 × 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
⊢ Primrec (β := Option ℕ) fun (p : (((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ) ↦
    Option.map (Nat.pair p.2) (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:
Primrec.option_map ((hlup.comp <| L.pair <| (k.pair cg).pair n).comp Primrec.fst) ?_

Premises used: Primrec.fst, Primrec.pair, _private.0.Nat.Partrec.Code.hlup, Primrec.comp, Primrec.option_map
-- 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 × 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
⊢ Primrec (β := ℕ) fun (p : ((((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ) × ℕ) ↦
    (fun (p : (((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ) ↦ Nat.pair p.2) p.1 p.2

Tactic:
Primrec₂.natPair.comp (Primrec.snd.comp Primrec.fst) Primrec.snd

Premises used: Primrec.snd, Primrec.fst, Primrec.comp, Primrec₂.natPair, Primrec₂.comp
-- 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 × 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
⊢ Primrec (β := ℕ) fun (p : ((((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ) × ℕ) ↦
    (fun (p : (((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ) ↦ Nat.pair p.2) p.1 p.2

Tactic:
exact Primrec₂.natPair.comp (Primrec.snd.comp Primrec.fst) Primrec.snd

Premises used: Primrec.snd, Primrec.fst, Primrec.comp, Primrec₂.natPair, Primrec₂.comp