awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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 (β := 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 n₁ : Primrec (β := ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ a.1.1.2
Tactic: have n := n.comp (Primrec.fst (β := 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_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 (β := 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 cf : 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 ℕ))
-- 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 × 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 (β := 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 z : Primrec (β := ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ (unpair a.1.1.2).1
Tactic: have z := Primrec.fst.comp (Primrec.unpair.comp n)
-- 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 × 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 (β := 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 m : Primrec (β := ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) ↦ (unpair a.1.1.2).2
Tactic: have m := Primrec.snd.comp (Primrec.unpair.comp n)
-- 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 × 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 ℕ) ↦
    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 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
Tactic: have h₁ := hlup.comp <| L.pair <| (k.pair cf).pair (Primrec₂.natPair.comp z m)
-- 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 × 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))
have 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
Tactic: refine Primrec.option_bind h₁ (?_ : 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 × 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 (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
have m₁ : Primrec (β := ℕ) fun (a : (((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Option ℕ) × ℕ) ↦ (unpair a.1.1.1.2).2
Tactic: have m := m.comp (Primrec.fst (β := ℕ))
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
k : ℕ
c : Code
n : ℕ
⊢ ((getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (List.range k) n).bind fun (a : ℕ) ↦ evaln k c a) =
    evaln k c n
have pos : ∀ (kn : n < k),
  ((getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (List.range k) n).bind fun (a : ℕ) ↦ evaln k c a) =
    evaln k c n
Tactic: by_cases kn : n < k
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
k : ℕ
c : Code
n : ℕ
pos :
  ∀ (kn : n < k),
    ((getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (List.range k) n).bind fun (a : ℕ) ↦ evaln k c a) =
      evaln k c n
⊢ ((getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (List.range k) n).bind fun (a : ℕ) ↦ evaln k c a) =
    evaln k c n
have neg : ∀ (kn : ¬n < k),
  ((getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (List.range k) n).bind fun (a : ℕ) ↦ evaln k c a) =
    evaln k c n
Tactic: by_cases kn : n < k
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
k : ℕ
c : Code
n : ℕ
kn : ¬n < k
⊢ ((getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (List.range k) n).bind fun (a : ℕ) ↦ evaln k c a) =
    evaln k c n
have neg : (Option.bind Option.none fun (a : ℕ) ↦ evaln k c a) = evaln k c n
Tactic: rw [List.getElem?_eq_none]
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
k : ℕ
c : Code
n : ℕ
kn : ¬n < k
neg : (Option.bind Option.none fun (a : ℕ) ↦ evaln k c a) = evaln k c n
⊢ ((getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (List.range k) n).bind fun (a : ℕ) ↦ evaln k c a) =
    evaln k c n
have neg₁ : (List.range k).length ≤ n
Tactic: rw [List.getElem?_eq_none]
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
k : ℕ
c : Code
n : ℕ
kn : ¬n < k
⊢ (Option.bind Option.none fun (a : ℕ) ↦ evaln k c a) = evaln k c n
have neg : ∀ (e : evaln k c n = Option.none), Eq (α := Option ℕ) (Option.bind Option.none fun (a : ℕ) ↦ evaln k c a) Option.none
Tactic: cases e : evaln k c n
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
k : ℕ
c : Code
n : ℕ
kn : ¬n < k
neg :
  ∀ (e : evaln k c n = Option.none), Eq (α := Option ℕ) (Option.bind Option.none fun (a : ℕ) ↦ evaln k c a) Option.none
⊢ (Option.bind Option.none fun (a : ℕ) ↦ evaln k c a) = evaln k c n
have neg₁ : ∀ (val : ℕ) (e : evaln k c n = some val), (Option.bind Option.none fun (a : ℕ) ↦ evaln k c a) = some val
Tactic: cases e : evaln k c n
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
Goal:
x : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.pair cg)) →
      lup
          (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.pair cg)))))
          (k', c') n =
        evaln k' c' n
⊢ Eq (α := Option ℕ)
    ((lup
          (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair (k' + 1) (encode (cf.pair cg)))))
          (k' + 1, cf) n).bind
      fun (a : ℕ) ↦
      (lup
            (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
              (List.range (Nat.pair (k' + 1) (encode (cf.pair cg)))))
            (k' + 1, cg) n).bind
        fun (y : ℕ) ↦ some (Nat.pair a y))
    ((Option.map Nat.pair (evaln (k' + 1) cf n)).bind fun (a : ℕ → ℕ) ↦ Option.map a (evaln (k' + 1) cg n))
have lf : encode cf < encode (cf.pair cg)
Tactic: obtain ⟨lf, lg⟩ := encode_lt_pair cf cg
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
Goal:
x : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.pair cg)) →
      lup
          (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.pair cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.pair cg)
⊢ Eq (α := Option ℕ)
    ((lup
          (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair (k' + 1) (encode (cf.pair cg)))))
          (k' + 1, cf) n).bind
      fun (a : ℕ) ↦
      (lup
            (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
              (List.range (Nat.pair (k' + 1) (encode (cf.pair cg)))))
            (k' + 1, cg) n).bind
        fun (y : ℕ) ↦ some (Nat.pair a y))
    ((Option.map Nat.pair (evaln (k' + 1) cf n)).bind fun (a : ℕ → ℕ) ↦ Option.map a (evaln (k' + 1) cg n))
have lg : encode cg < encode (cf.pair cg)
Tactic: obtain ⟨lf, lg⟩ := encode_lt_pair cf cg
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
x : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.pair cg)) →
      lup
          (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.pair cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.pair cg)
lg : encode cg < encode (cf.pair cg)
⊢ Eq (α := Option ℕ)
    ((lup
          (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair (k' + 1) (encode (cf.pair cg)))))
          (k' + 1, cf) n).bind
      fun (a : ℕ) ↦
      (lup
            (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
              (List.range (Nat.pair (k' + 1) (encode (cf.pair cg)))))
            (k' + 1, cg) n).bind
        fun (y : ℕ) ↦ some (Nat.pair a y))
    ((Option.map Nat.pair (evaln (k' + 1) cf n)).bind fun (a : ℕ → ℕ) ↦ Option.map a (evaln (k' + 1) cg n))
have succ : Eq (α := Option ℕ) ((evaln k cf n).bind fun (a : ℕ) ↦ (evaln k cg n).bind fun (y : ℕ) ↦ some (Nat.pair a y))
  ((Option.map Nat.pair (evaln (k' + 1) cf n)).bind fun (a : ℕ → ℕ) ↦ Option.map a (evaln (k' + 1) cg n))
Tactic: rw [hg (Nat.pair_lt_pair_right _ lf), hg (Nat.pair_lt_pair_right _ lg)]
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
x : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.pair cg)) →
      lup
          (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.pair cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.pair cg)
lg : encode cg < encode (cf.pair cg)
⊢ Eq (α := Option ℕ) ((evaln k cf n).bind fun (a : ℕ) ↦ (evaln k cg n).bind fun (y : ℕ) ↦ some (Nat.pair a y))
    ((Option.map Nat.pair (evaln (k' + 1) cf n)).bind fun (a : ℕ → ℕ) ↦ Option.map a (evaln (k' + 1) cg n))
have succ : Eq (α := Option ℕ) (Option.bind Option.none fun (a : ℕ) ↦ (evaln k cg n).bind fun (y : ℕ) ↦ some (Nat.pair a y))
  ((Option.map Nat.pair Option.none).bind fun (a : ℕ → ℕ) ↦ Option.map a (evaln (k' + 1) cg n))
Tactic: cases evaln k cf n
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
x : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.pair cg)) →
      lup
          (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.pair cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.pair cg)
lg : encode cg < encode (cf.pair cg)
succ :
  Eq (α := Option ℕ) (Option.bind Option.none fun (a : ℕ) ↦ (evaln k cg n).bind fun (y : ℕ) ↦ some (Nat.pair a y))
    ((Option.map Nat.pair Option.none).bind fun (a : ℕ → ℕ) ↦ Option.map a (evaln (k' + 1) cg n))
⊢ Eq (α := Option ℕ) ((evaln k cf n).bind fun (a : ℕ) ↦ (evaln k cg n).bind fun (y : ℕ) ↦ some (Nat.pair a y))
    ((Option.map Nat.pair (evaln (k' + 1) cf n)).bind fun (a : ℕ → ℕ) ↦ Option.map a (evaln (k' + 1) cg n))
have succ₁ : ∀ (val : ℕ),
  Eq (α := Option ℕ) ((some val).bind fun (a : ℕ) ↦ (evaln k cg n).bind fun (y : ℕ) ↦ some (Nat.pair a y))
    ((Option.map Nat.pair (some val)).bind fun (a : ℕ → ℕ) ↦ Option.map a (evaln (k' + 1) cg n))
Tactic: cases evaln k cf n
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
x : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.pair cg)) →
      lup
          (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.pair cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.pair cg)
lg : encode cg < encode (cf.pair cg)
val : ℕ
⊢ Eq (α := Option ℕ) ((some val).bind fun (a : ℕ) ↦ (evaln k cg n).bind fun (y : ℕ) ↦ some (Nat.pair a y))
    ((Option.map Nat.pair (some val)).bind fun (a : ℕ → ℕ) ↦ Option.map a (evaln (k' + 1) cg n))
have succ : Eq (α := Option ℕ) ((some val).bind fun (a : ℕ) ↦ Option.bind Option.none fun (y : ℕ) ↦ some (Nat.pair a y))
  ((Option.map Nat.pair (some val)).bind fun (a : ℕ → ℕ) ↦ Option.map a Option.none)
Tactic: cases evaln k cg n