awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ
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)
⊢ 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₁ : ∀ (val_1 : ℕ),
  Eq (α := Option ℕ) ((some val).bind fun (a : ℕ) ↦ (some val_1).bind fun (y : ℕ) ↦ some (Nat.pair a y))
    ((Option.map Nat.pair (some val)).bind fun (a : ℕ → ℕ) ↦ Option.map a (some val_1))
Tactic: cases evaln k cg 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.comp 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.comp 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.comp cg)))))
          (k' + 1, cg) n).bind
      fun (x : ℕ) ↦
      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.comp cg)))))
        (k' + 1, cf) x)
    ((evaln (k' + 1) cg n).bind fun (x : ℕ) ↦ evaln (k' + 1) cf x)
have lf : encode cf < encode (cf.comp cg)
Tactic: obtain ⟨lf, lg⟩ := encode_lt_comp 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.comp 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.comp cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.comp 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.comp cg)))))
          (k' + 1, cg) n).bind
      fun (x : ℕ) ↦
      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.comp cg)))))
        (k' + 1, cf) x)
    ((evaln (k' + 1) cg n).bind fun (x : ℕ) ↦ evaln (k' + 1) cf x)
have lg : encode cg < encode (cf.comp cg)
Tactic: obtain ⟨lf, lg⟩ := encode_lt_comp 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.comp 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.comp cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.comp cg)
lg : encode cg < encode (cf.comp 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.comp cg)))))
          (k' + 1, cg) n).bind
      fun (x : ℕ) ↦
      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.comp cg)))))
        (k' + 1, cf) x)
    ((evaln (k' + 1) cg n).bind fun (x : ℕ) ↦ evaln (k' + 1) cf x)
have succ : Eq (α := Option ℕ)
  ((evaln k cg n).bind fun (x : ℕ) ↦
    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.comp cg)))))
      (k' + 1, cf) x)
  ((evaln (k' + 1) cg n).bind fun (x : ℕ) ↦ evaln (k' + 1) cf x)
Tactic: rw [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.comp 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.comp cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.comp cg)
lg : encode cg < encode (cf.comp cg)
⊢ Eq (α := Option ℕ)
    ((evaln k cg n).bind fun (x : ℕ) ↦
      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.comp cg)))))
        (k' + 1, cf) x)
    ((evaln (k' + 1) cg n).bind fun (x : ℕ) ↦ evaln (k' + 1) cf x)
have succ : Eq (α := Option ℕ)
  (Option.bind Option.none fun (x : ℕ) ↦
    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.comp cg)))))
      (k' + 1, cf) x)
  (Option.bind Option.none fun (x : ℕ) ↦ evaln (k' + 1) cf x)
Tactic: cases evaln k cg 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.comp 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.comp cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.comp cg)
lg : encode cg < encode (cf.comp cg)
succ :
  Eq (α := Option ℕ)
    (Option.bind Option.none fun (x : ℕ) ↦
      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.comp cg)))))
        (k' + 1, cf) x)
    (Option.bind Option.none fun (x : ℕ) ↦ evaln (k' + 1) cf x)
⊢ Eq (α := Option ℕ)
    ((evaln k cg n).bind fun (x : ℕ) ↦
      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.comp cg)))))
        (k' + 1, cf) x)
    ((evaln (k' + 1) cg n).bind fun (x : ℕ) ↦ evaln (k' + 1) cf x)
have succ₁ : ∀ (val : ℕ),
  Eq (α := Option ℕ)
    ((some val).bind fun (x : ℕ) ↦
      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.comp cg)))))
        (k' + 1, cf) x)
    ((some val).bind fun (x : ℕ) ↦ evaln (k' + 1) cf x)
Tactic: cases evaln k cg 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.prec 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.prec cg)))))
          (k', c') n =
        evaln k' c' n
⊢ Eq (α := Option ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ 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.prec cg)))))
          (k' + 1, cf) (unpair n).1)
        (fun (n_1 : ℕ) (n_ih : 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.prec cg)))))
                (k', cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind
            fun (i : ℕ) ↦
            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.prec cg)))))
              (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
        (unpair n).2 :
      Option ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k' + 1) cf (unpair n).1)
        (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
          (evaln k' (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun (i : ℕ) ↦
            evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
        (unpair n).2 :
      Option ℕ)
have lf : encode cf < encode (cf.prec cg)
Tactic: obtain ⟨lf, lg⟩ := encode_lt_prec 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.prec 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.prec cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.prec cg)
⊢ Eq (α := Option ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ 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.prec cg)))))
          (k' + 1, cf) (unpair n).1)
        (fun (n_1 : ℕ) (n_ih : 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.prec cg)))))
                (k', cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind
            fun (i : ℕ) ↦
            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.prec cg)))))
              (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
        (unpair n).2 :
      Option ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k' + 1) cf (unpair n).1)
        (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
          (evaln k' (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun (i : ℕ) ↦
            evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
        (unpair n).2 :
      Option ℕ)
have lg : encode cg < encode (cf.prec cg)
Tactic: obtain ⟨lf, lg⟩ := encode_lt_prec 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.prec 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.prec cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.prec cg)
lg : encode cg < encode (cf.prec cg)
⊢ Eq (α := Option ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ 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.prec cg)))))
          (k' + 1, cf) (unpair n).1)
        (fun (n_1 : ℕ) (n_ih : 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.prec cg)))))
                (k', cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind
            fun (i : ℕ) ↦
            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.prec cg)))))
              (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
        (unpair n).2 :
      Option ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k' + 1) cf (unpair n).1)
        (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
          (evaln k' (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun (i : ℕ) ↦
            evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
        (unpair n).2 :
      Option ℕ)
have succ : Eq (α := Option ℕ)
  (Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln k cf (unpair n).1)
      (fun (n_1 : ℕ) (n_ih : 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.prec cg)))))
              (k', cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind
          fun (i : ℕ) ↦
          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.prec cg)))))
            (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
      (unpair n).2 :
    Option ℕ)
  (Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k' + 1) cf (unpair n).1)
      (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
        (evaln k' (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun (i : ℕ) ↦
          evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
      (unpair n).2 :
    Option ℕ)
Tactic: rw [hg (Nat.pair_lt_pair_right _ lf)]
-- 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.prec 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.prec cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.prec cg)
lg : encode cg < encode (cf.prec cg)
⊢ Eq (α := Option ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln k cf (unpair n).1)
        (fun (n_1 : ℕ) (n_ih : 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.prec cg)))))
                (k', cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind
            fun (i : ℕ) ↦
            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.prec cg)))))
              (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
        (unpair n).2 :
      Option ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k' + 1) cf (unpair n).1)
        (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
          (evaln k' (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun (i : ℕ) ↦
            evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
        (unpair n).2 :
      Option ℕ)
have succ : Eq (α := Option ℕ)
  (Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln k cf (unpair n).1)
      (fun (n_1 : ℕ) (n_ih : 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.prec cg)))))
              (k', cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind
          fun (i : ℕ) ↦
          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.prec cg)))))
            (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
      0 :
    Option ℕ)
  (Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k' + 1) cf (unpair n).1)
      (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
        (evaln k' (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun (i : ℕ) ↦
          evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
      0 :
    Option ℕ)
Tactic: cases n.unpair.2
-- 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.prec 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.prec cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.prec cg)
lg : encode cg < encode (cf.prec cg)
n_1 : ℕ
⊢ 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.prec cg)))))
          (k', cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind
      fun (i : ℕ) ↦
      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.prec cg)))))
        (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
    ((evaln k' (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun (i : ℕ) ↦
      evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
have succ : Eq (α := Option ℕ)
  ((evaln k' (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun (i : ℕ) ↦
    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.prec cg)))))
      (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
  ((evaln k' (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun (i : ℕ) ↦
    evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
Tactic: rw [hg (Nat.pair_lt_pair_left _ k'.lt_succ_self)]
-- 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.prec 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.prec cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.prec cg)
lg : encode cg < encode (cf.prec cg)
n_1 : ℕ
⊢ Eq (α := Option ℕ)
    ((evaln k' (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun (i : ℕ) ↦
      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.prec cg)))))
        (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
    ((evaln k' (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun (i : ℕ) ↦
      evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
have succ : Eq (α := Option ℕ)
  (Option.bind Option.none fun (i : ℕ) ↦
    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.prec cg)))))
      (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
  (Option.bind Option.none fun (i : ℕ) ↦ evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
Tactic: cases evaln k' _ _
-- 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.prec 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.prec cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.prec cg)
lg : encode cg < encode (cf.prec cg)
n_1 : ℕ
succ :
  Eq (α := Option ℕ)
    (Option.bind Option.none fun (i : ℕ) ↦
      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.prec cg)))))
        (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
    (Option.bind Option.none fun (i : ℕ) ↦ evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
⊢ Eq (α := Option ℕ)
    ((evaln k' (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun (i : ℕ) ↦
      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.prec cg)))))
        (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
    ((evaln k' (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun (i : ℕ) ↦
      evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
have succ₁ : ∀ (val : ℕ),
  Eq (α := Option ℕ)
    ((some val).bind fun (i : ℕ) ↦
      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.prec cg)))))
        (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
    ((some val).bind fun (i : ℕ) ↦ evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
Tactic: cases evaln k' _ _