awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode cf.rfind') →
      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.rfind'))))
          (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.rfind'))))
          (k' + 1, cf) n).bind
      fun (x : ℕ) ↦
      Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (some (unpair n).2)
        (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.rfind'))))
            (k', cf.rfind') (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
        x)
    ((evaln (k' + 1) cf n).bind fun (a : ℕ) ↦
      if a = 0 then some (unpair n).2 else evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
have lf : encode cf < encode cf.rfind'
Tactic: have lf := encode_lt_rfind' cf
-- 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 : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode cf.rfind') →
      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.rfind'))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode cf.rfind'
⊢ 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.rfind'))))
          (k' + 1, cf) n).bind
      fun (x : ℕ) ↦
      Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (some (unpair n).2)
        (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.rfind'))))
            (k', cf.rfind') (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
        x)
    ((evaln (k' + 1) cf n).bind fun (a : ℕ) ↦
      if a = 0 then some (unpair n).2 else evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
have succ : Eq (α := Option ℕ)
  ((evaln k cf n).bind fun (x : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (some (unpair n).2)
      (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.rfind'))))
          (k', cf.rfind') (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
      x)
  ((evaln (k' + 1) cf n).bind fun (a : ℕ) ↦
    if a = 0 then some (unpair n).2 else evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
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 : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode cf.rfind') →
      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.rfind'))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode cf.rfind'
⊢ Eq (α := Option ℕ)
    ((evaln k cf n).bind fun (x : ℕ) ↦
      Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (some (unpair n).2)
        (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.rfind'))))
            (k', cf.rfind') (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
        x)
    ((evaln (k' + 1) cf n).bind fun (a : ℕ) ↦
      if a = 0 then some (unpair n).2 else evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
have succ : Eq (α := Option ℕ)
  (Option.bind Option.none fun (x : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (some (unpair n).2)
      (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.rfind'))))
          (k', cf.rfind') (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
      x)
  (Option.bind Option.none fun (a : ℕ) ↦
    if a = 0 then some (unpair n).2 else evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
Tactic: rcases evaln k cf n with - | x
-- 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 : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode cf.rfind') →
      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.rfind'))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode cf.rfind'
succ :
  Eq (α := Option ℕ)
    (Option.bind Option.none fun (x : ℕ) ↦
      Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (some (unpair n).2)
        (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.rfind'))))
            (k', cf.rfind') (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
        x)
    (Option.bind Option.none fun (a : ℕ) ↦
      if a = 0 then some (unpair n).2 else evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
⊢ Eq (α := Option ℕ)
    ((evaln k cf n).bind fun (x : ℕ) ↦
      Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (some (unpair n).2)
        (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.rfind'))))
            (k', cf.rfind') (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
        x)
    ((evaln (k' + 1) cf n).bind fun (a : ℕ) ↦
      if a = 0 then some (unpair n).2 else evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
have succ₁ : ∀ (x : ℕ),
  Eq (α := Option ℕ)
    ((some x).bind fun (x : ℕ) ↦
      Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (some (unpair n).2)
        (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.rfind'))))
            (k', cf.rfind') (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
        x)
    ((some x).bind fun (a : ℕ) ↦
      if a = 0 then some (unpair n).2 else evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
Tactic: rcases evaln k cf n with - | x
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
x_1 : 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 : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode cf.rfind') →
      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.rfind'))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode cf.rfind'
x : ℕ
⊢ Eq (α := Option ℕ)
    ((some x).bind fun (x : ℕ) ↦
      Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (some (unpair n).2)
        (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.rfind'))))
            (k', cf.rfind') (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
        x)
    ((some x).bind fun (a : ℕ) ↦
      if a = 0 then some (unpair n).2 else evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
have succ : Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (some (unpair n).2)
    (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.rfind'))))
        (k', cf.rfind') (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
    x =
  if x = 0 then some (unpair n).2 else evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))
Tactic: simp only [Option.bind_some]
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
x_1 : 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 : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode cf.rfind') →
      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.rfind'))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode cf.rfind'
x : ℕ
⊢ Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (some (unpair n).2)
      (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.rfind'))))
          (k', cf.rfind') (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
      x =
    if x = 0 then some (unpair n).2 else evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))
have succ : Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (some (unpair n).2)
    (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.rfind'))))
        (k', cf.rfind') (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
    0 =
  if Eq (α := ℕ) 0 0 then some (unpair n).2 else evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
x_1 : 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 : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode cf.rfind') →
      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.rfind'))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode cf.rfind'
x : ℕ
succ :
  Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (some (unpair n).2)
      (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.rfind'))))
          (k', cf.rfind') (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
      0 =
    if Eq (α := ℕ) 0 0 then some (unpair n).2 else evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))
⊢ Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (some (unpair n).2)
      (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.rfind'))))
          (k', cf.rfind') (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
      x =
    if x = 0 then some (unpair n).2 else evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))
have succ₁ : ∀ (n_1 : ℕ),
  Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (some (unpair n).2)
      (fun (n_2 : ℕ) (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.rfind'))))
          (k', cf.rfind') (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
      (n_1 + 1) =
    if n_1 + 1 = 0 then some (unpair n).2 else evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))
Tactic: cases x
Cleared hypotheses: x
-- 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 : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode cf.rfind') →
      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.rfind'))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode cf.rfind'
n_1 : ℕ
⊢ 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.rfind'))))
      (k', cf.rfind') (Nat.pair (unpair n).1 ((unpair n).2 + 1)) =
    evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))
have succ : evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)) =
  evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))
Tactic: rw [hg (Nat.pair_lt_pair_left _ k'.lt_succ_self)]
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
c : Code
n x : ℕ
⊢ x ∈ c.eval n ↔ Membership.mem (γ := Part ℕ) (rfindOpt fun (k : ℕ) ↦ evaln k c n) x
have refine : ∀ {a m n_1 : ℕ}, m ≤ n_1 → a ∈ evaln m c n → a ∈ evaln n_1 c n
Tactic: refine evaln_complete.trans (Nat.rfindOpt_mono ?_).symm
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
⊢ Countable { f : ℕ →. ℕ // Partrec f }
have apply : Function.Surjective (β := { f : ℕ →. ℕ // Partrec f }) fun (c : Code) ↦
  Subtype.mk (p := fun (f : ℕ →. ℕ) ↦ Partrec f) c.eval sorry
Tactic: apply Function.Surjective.countable (f := fun c => ⟨eval c, eval_part.comp (.const c) .id⟩)
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
n : ℕ
⊢ Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) n 0 id = n.pred
have zero : Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) 0 0 id = Nat.pred 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
n : ℕ
zero : Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) 0 0 id = Nat.pred 0
⊢ Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) n 0 id = n.pred
have succ : ∀ (n : ℕ), Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (n + 1) 0 id = (n + 1).pred
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
p : ℕ
⊢ Eq (α := ℕ)
    (unpaired
      (fun (z n : ℕ) ↦
        Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (id z)
          (fun (y IH : ℕ) ↦ (unpair (unpair (Nat.pair z (Nat.pair y IH))).2).2.succ) n)
      p)
    (unpaired (fun (x1 x2 : ℕ) ↦ x1 + x2) p)
have simp : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (unpair p).1 (fun (y IH : ℕ) ↦ IH + 1) (unpair p).2 = (unpair p).1 + (unpair p).2
Tactic: simp
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
p : ℕ
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (unpair p).1 (fun (y IH : ℕ) ↦ IH + 1) (unpair p).2 = (unpair p).1 + (unpair p).2
have zero : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (unpair p).1 (fun (y IH : ℕ) ↦ IH + 1) 0 = (unpair p).1 + 0
Tactic: induction p.unpair.2
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
p : ℕ
zero : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (unpair p).1 (fun (y IH : ℕ) ↦ IH + 1) 0 = (unpair p).1 + 0
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (unpair p).1 (fun (y IH : ℕ) ↦ IH + 1) (unpair p).2 = (unpair p).1 + (unpair p).2
have succ : ∀ (n : ℕ),
  Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (unpair p).1 (fun (y IH : ℕ) ↦ IH + 1) n = (unpair p).1 + n →
    Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (unpair p).1 (fun (y IH : ℕ) ↦ IH + 1) (n + 1) = (unpair p).1 + (n + 1)
Tactic: induction p.unpair.2
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
p : ℕ
⊢ Eq (α := ℕ)
    (unpaired
      (fun (z n : ℕ) ↦
        Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (id z)
          (fun (y IH : ℕ) ↦ (unpair (unpair (Nat.pair z (Nat.pair y IH))).2).2.pred) n)
      p)
    (unpaired (fun (x1 x2 : ℕ) ↦ x1 - x2) p)
have simp : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (unpair p).1 (fun (y IH : ℕ) ↦ IH - 1) (unpair p).2 = (unpair p).1 - (unpair p).2
Tactic: simp
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
p : ℕ
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (unpair p).1 (fun (y IH : ℕ) ↦ IH - 1) (unpair p).2 = (unpair p).1 - (unpair p).2
have zero : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (unpair p).1 (fun (y IH : ℕ) ↦ IH - 1) 0 = (unpair p).1 - 0
Tactic: induction p.unpair.2
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
p : ℕ
zero : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (unpair p).1 (fun (y IH : ℕ) ↦ IH - 1) 0 = (unpair p).1 - 0
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (unpair p).1 (fun (y IH : ℕ) ↦ IH - 1) (unpair p).2 = (unpair p).1 - (unpair p).2
have succ : ∀ (n : ℕ),
  Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (unpair p).1 (fun (y IH : ℕ) ↦ IH - 1) n = (unpair p).1 - n →
    Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (unpair p).1 (fun (y IH : ℕ) ↦ IH - 1) (n + 1) = (unpair p).1 - (n + 1)
Tactic: induction p.unpair.2
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
p : ℕ
⊢ Eq (α := ℕ)
    (unpaired
      (fun (z n : ℕ) ↦
        Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0
          (fun (y IH : ℕ) ↦
            unpaired (fun (x1 x2 : ℕ) ↦ x1 + x2)
              (Nat.pair (unpair (Nat.pair z (Nat.pair y IH))).1 (unpair (unpair (Nat.pair z (Nat.pair y IH))).2).2))
          n)
      p)
    (unpaired (fun (x1 x2 : ℕ) ↦ x1 * x2) p)
have simp : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (y IH : ℕ) ↦ (unpair p).1 + IH) (unpair p).2 = (unpair p).1 * (unpair p).2
Tactic: simp
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
p : ℕ
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (y IH : ℕ) ↦ (unpair p).1 + IH) (unpair p).2 = (unpair p).1 * (unpair p).2
have zero : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (y IH : ℕ) ↦ (unpair p).1 + IH) 0 = (unpair p).1 * 0
Tactic: induction p.unpair.2
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
p : ℕ
zero : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (y IH : ℕ) ↦ (unpair p).1 + IH) 0 = (unpair p).1 * 0
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (y IH : ℕ) ↦ (unpair p).1 + IH) (unpair p).2 = (unpair p).1 * (unpair p).2
have succ : ∀ (n : ℕ),
  Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (y IH : ℕ) ↦ (unpair p).1 + IH) n = (unpair p).1 * n →
    Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (y IH : ℕ) ↦ (unpair p).1 + IH) (n + 1) = (unpair p).1 * (n + 1)
Tactic: induction p.unpair.2
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
p : ℕ
⊢ Eq (α := ℕ)
    (unpaired
      (fun (z n : ℕ) ↦
        Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 1
          (fun (y IH : ℕ) ↦
            unpaired (fun (x1 x2 : ℕ) ↦ x1 * x2)
              (Nat.pair (unpair (unpair (Nat.pair z (Nat.pair y IH))).2).2 (unpair (Nat.pair z (Nat.pair y IH))).1))
          n)
      p)
    (unpaired (fun (x1 x2 : ℕ) ↦ x1 ^ x2) p)
have simp : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 1 (fun (y IH : ℕ) ↦ IH * (unpair p).1) (unpair p).2 = (unpair p).1 ^ (unpair p).2
Tactic: simp
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
p : ℕ
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 1 (fun (y IH : ℕ) ↦ IH * (unpair p).1) (unpair p).2 = (unpair p).1 ^ (unpair p).2
have zero : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 1 (fun (y IH : ℕ) ↦ IH * (unpair p).1) 0 = HPow.hPow (β := ℕ) (unpair p).1 0
Tactic: induction p.unpair.2
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
p : ℕ
zero : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 1 (fun (y IH : ℕ) ↦ IH * (unpair p).1) 0 = HPow.hPow (β := ℕ) (unpair p).1 0
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 1 (fun (y IH : ℕ) ↦ IH * (unpair p).1) (unpair p).2 = (unpair p).1 ^ (unpair p).2
have succ : ∀ (n : ℕ),
  Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 1 (fun (y IH : ℕ) ↦ IH * (unpair p).1) n = (unpair p).1 ^ n →
    Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 1 (fun (y IH : ℕ) ↦ IH * (unpair p).1) (n + 1) = (unpair p).1 ^ (n + 1)
Tactic: induction p.unpair.2
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
e : β ≃ α
n : ℕ
⊢ encode.{u_1} (α := Option α) (decode n) = encode.{u_2} (α := Option β) (decode n)
have rw : encode.{u_1} (α := Option α) (decode n) =
  encode.{u_2} (α := Option β) (Option.map.{u_1, u_2} (α := α) (⇑e.symm : (a : α) → β) (decode n))
Tactic: rw [decode_ofEquiv]
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
e : β ≃ α
n : ℕ
⊢ encode.{u_1} (α := Option α) (decode n) =
    encode.{u_2} (α := Option β) (Option.map.{u_1, u_2} (α := α) (⇑e.symm : (a : α) → β) (decode n))
have none : encode.{u_1} (α := Option α) none =
  encode.{u_2} (α := Option β) (Option.map.{u_1, u_2} (α := α) (⇑e.symm : (a : α) → β) none)
Tactic: cases (@decode α _ n)
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
e : β ≃ α
n : ℕ
none :
  encode.{u_1} (α := Option α) Option.none =
    encode.{u_2} (α := Option β) (Option.map.{u_1, u_2} (α := α) (⇑e.symm : (a : α) → β) Option.none)
⊢ encode.{u_1} (α := Option α) (decode n) =
    encode.{u_2} (α := Option β) (Option.map.{u_1, u_2} (α := α) (⇑e.symm : (a : α) → β) (decode n))
have some : ∀ (val : α), encode (some val) = encode.{u_2} (α := Option β) (Option.map (⇑e.symm : (a : α) → β) (some val))
Tactic: cases (@decode α _ n)
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
n : ℕ
⊢ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) n 1 fun (x : ℕ) ↦ 0) = encode.{u_1} (α := Option PUnit.{u_1 + 1}) (decode n)
have zero : (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) 0 1 fun (x : ℕ) ↦ 0) = encode.{u_1} (α := Option PUnit.{u_1 + 1}) (decode 0)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
n : ℕ
zero :
  (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) 0 1 fun (x : ℕ) ↦ 0) = encode.{u_1} (α := Option PUnit.{u_1 + 1}) (decode 0)
⊢ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) n 1 fun (x : ℕ) ↦ 0) = encode.{u_1} (α := Option PUnit.{u_1 + 1}) (decode n)
have succ : ∀ (n : ℕ),
  (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (n + 1) 1 fun (x : ℕ) ↦ 0) =
    encode.{u_1} (α := Option PUnit.{u_1 + 1}) (decode (n + 1))
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
h : Primcodable α
n : ℕ
⊢ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (n + 1) 1 fun (n : ℕ) ↦
      Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode.{u_1} (α := Option α) (decode n)) 0 fun (n : ℕ) ↦ n.succ.succ) =
    encode.{u_1} (α := Option (Option α)) (decode (n + 1))
have succ : (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (n + 1) 1 fun (n : ℕ) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode.{u_1} (α := Option α) (decode n)) 0 fun (n : ℕ) ↦ n.succ.succ) =
  encode.{u_1} (α := Option (Option α)) (Option.map some (decode n))
Tactic: rw [decode_option_succ]