awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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
z :
  Primrec (β := ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) ↦ (unpair a.1.1.2).1
⊢ Primrec (β := Option ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) ↦
    have z := (unpair a.1.1.2).1;
    Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) (unpair a.1.1.2).2
      (lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) z) fun (y : ℕ) ↦ do
      let i ← lup a.1.1.1 (a.1.2, (ofNat (ℕ × Code) a.1.1.1.length).2) (Nat.pair z y)
      lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.2.1) (Nat.pair z (Nat.pair y i))
have hpc : 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: refine
      Primrec.nat_casesOn (Primrec.snd.comp (Primrec.unpair.comp n))
        (hlup.comp <| L.pair <| (k.pair cf).pair z)
        (?_ : Primrec _)
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
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
z :
  Primrec (β := ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) ↦ (unpair a.1.1.2).1
⊢ 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
have L₁ : Primrec (β := List (List (Option ℕ)))
  fun (a : (((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ) ↦ a.1.1.1.1
Tactic: have L := L.comp (Primrec.fst (β := ℕ))
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
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 :
  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
⊢ 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
have z₁ : Primrec (β := ℕ) fun (a : (((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ) ↦
  (unpair a.1.1.1.2).1
Tactic: have z := z.comp (Primrec.fst (β := ℕ))
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
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
⊢ 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
have y : Primrec (α := (((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ) Prod.snd
Tactic: have y := Primrec.snd
      (α := ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) (β := ℕ)
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
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
⊢ 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
have 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
Tactic: have h₁ := hlup.comp <| L.pair <| (((k'.pair c).comp Primrec.fst).comp Primrec.fst).pair
      (Primrec₂.natPair.comp z y)
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
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 (p : (((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ) (i : ℕ) ↦
        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
have z₁ : 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 (β := ℕ))
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
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 (β := Option ℕ) fun (p : ((((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ) × ℕ) ↦
    (fun (p : (((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ) (i : ℕ) ↦
        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
have y₁ : Primrec (β := ℕ) fun (a : ((((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ) × ℕ) ↦ a.1.2
Tactic: have y := y.comp (Primrec.fst (β := ℕ))
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
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 (β := Option ℕ) fun (p : ((((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ) × ℕ) ↦
    (fun (p : (((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ) (i : ℕ) ↦
        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
have i : Primrec (α := ((((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ) × ℕ) Prod.snd
Tactic: have i := Primrec.snd
      (α := (((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ)
      (β := ℕ)
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
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 (β := 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))
have L : 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 ℕ))
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
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 (β := 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))
have k₁ : 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 ℕ))