awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.PartrecCode
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)))
      x =
    if x = 0 then some (unpair n).2 else evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))
⊢ 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:
simp only [Option.bind_some]

Premises used: Option.bind_some
-- Module: Mathlib.Computability.PartrecCode
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))
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))
⊢ 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:
cases x
-- Module: Mathlib.Computability.PartrecCode
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'
⊢ 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:
simp
-- Module: Mathlib.Computability.PartrecCode
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 : ℕ
succ 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))
⊢ 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))

Tactic:
rw [hg (Nat.pair_lt_pair_left _ k'.lt_succ_self)]

Premises used: Nat.lt_succ_self, Nat.pair_lt_pair_left
-- Module: Mathlib.Computability.PartrecCode
Goal:
this :
  Primrec₂ (σ := List (Option ℕ)) fun (x : Unit) (n : ℕ) ↦
    let a : ℕ × Code := ofNat (ℕ × Code) n;
    List.map (evaln a.1 a.2) (List.range a.1)
x : (ℕ × Code) × ℕ
k : ℕ
c : Code
n : ℕ
⊢ ((getElem? (valid := fun (as : List (Option ℕ)) (i : ℕ) ↦ i < as.length)
          (let a : ℕ × Code := ofNat (ℕ × Code) (encode ((k, c), n).1);
          List.map (evaln a.1 a.2) (List.range a.1))
          ((k, c), n).2).bind
      fun (b : Option ℕ) ↦ (((k, c), n), b).2) =
    evaln ((k, c), n).1.1 ((k, c), n).1.2 ((k, c), n).2

Tactic:
simp [evaln_map, Option.bind_map]

Premises used: _private.0.Nat.Partrec.Code.evaln_map, Option.bind_map
-- Module: Mathlib.Computability.PartrecCode
Goal:
c : Code
n x : ℕ
⊢ x ∈ c.eval n ↔ Membership.mem (γ := Part ℕ) (rfindOpt fun (k : ℕ) ↦ evaln k c n) x

Tactic:
evaln_complete.trans (Nat.rfindOpt_mono ?_).symm

Premises used: Nat.rfindOpt_mono, Iff.trans, Nat.Partrec.Code.evaln_complete, Iff.symm
-- Module: Mathlib.Computability.PartrecCode
Goal:
c : Code
n x : ℕ
refine : ∀ {a m n_1 : ℕ}, m ≤ n_1 → a ∈ evaln m c n → a ∈ evaln n_1 c n
⊢ x ∈ c.eval n ↔ Membership.mem (γ := Part ℕ) (rfindOpt fun (k : ℕ) ↦ evaln k c n) x

Tactic:
refine evaln_complete.trans (Nat.rfindOpt_mono ?_).symm

Premises used: Nat.rfindOpt_mono, Iff.trans, Nat.Partrec.Code.evaln_complete, Iff.symm
-- Module: Mathlib.Computability.PartrecCode
Goal:
c : Code
n_1 x a m n : ℕ
hl : m ≤ n
⊢ a ∈ evaln m c n_1 → a ∈ evaln n c n_1

Tactic:
apply evaln_mono hl

Premises used: Nat.Partrec.Code.evaln_mono
-- Module: Mathlib.Computability.PartrecCode
Goal:
a : Code × ℕ
⊢ (rfindOpt fun (b : ℕ) ↦
      evaln (((a, b).2, (a, b).1.1), (a, b).1.2).1.1 (((a, b).2, (a, b).1.1), (a, b).1.2).1.2
        (((a, b).2, (a, b).1.1), (a, b).1.2).2) =
    a.1.eval a.2

Tactic:
simp [eval_eq_rfindOpt]

Premises used: Nat.Partrec.Code.eval_eq_rfindOpt
-- Module: Mathlib.Computability.PartrecCode
Goal:
f : Code → Code
hf : Computable f
g : (x y : ℕ) → Part ℕ :=
  fun (x y : ℕ) ↦ do
    let b ← (ofNat Code x).eval x
    (ofNat Code b).eval y
this : Partrec₂ g
cg : Code
eg :
  cg.eval = fun (n : ℕ) ↦
    Part.bind (↑(decode n) : Part (ℕ × ℕ)) fun (a : ℕ × ℕ) ↦ Part.map (α := ℕ) encode ((fun (p : ℕ × ℕ) ↦ g p.1 p.2) a)
⊢ ∀ (a n : ℕ), cg.eval (Nat.pair a n) = Part.map encode (g a n)

Tactic:
simp [eg]
-- Module: Mathlib.Computability.PartrecCode
Goal:
f : Code → Code
hf : Computable f
g : (x y : ℕ) → Part ℕ :=
  fun (x y : ℕ) ↦ do
    let b ← (ofNat Code x).eval x
    (ofNat Code b).eval y
this_1 : Partrec₂ g
cg : Code
eg :
  cg.eval = fun (n : ℕ) ↦
    Part.bind (↑(decode n) : Part (ℕ × ℕ)) fun (a : ℕ × ℕ) ↦ Part.map (α := ℕ) encode ((fun (p : ℕ × ℕ) ↦ g p.1 p.2) a)
eg' : ∀ (a n : ℕ), cg.eval (Nat.pair a n) = Part.map encode (g a n)
F : (x : ℕ) → Code := fun (x : ℕ) ↦ f (cg.curry x)
this : Computable F
cF : Code
eF : cF.eval = fun (n : ℕ) ↦ Part.bind (↑(decode n) : Part ℕ) fun (a : ℕ) ↦ Part.map encode ((↑F : ℕ →. Code) a)
⊢ cF.eval (encode cF) = Part.some (encode (F (encode cF)))

Tactic:
simp [eF]
-- Module: Mathlib.Computability.PartrecCode
Goal:
f : Code → Code
hf : Computable f
g : (x y : ℕ) → Part ℕ :=
  fun (x y : ℕ) ↦ do
    let b ← (ofNat Code x).eval x
    (ofNat Code b).eval y
this_1 : Partrec₂ g
cg : Code
eg :
  cg.eval = fun (n : ℕ) ↦
    Part.bind (↑(decode n) : Part (ℕ × ℕ)) fun (a : ℕ × ℕ) ↦ Part.map (α := ℕ) encode ((fun (p : ℕ × ℕ) ↦ g p.1 p.2) a)
eg' : ∀ (a n : ℕ), cg.eval (Nat.pair a n) = Part.map encode (g a n)
F : (x : ℕ) → Code := fun (x : ℕ) ↦ f (cg.curry x)
this : Computable F
cF : Code
eF : cF.eval = fun (n : ℕ) ↦ Part.bind (↑(decode n) : Part ℕ) fun (a : ℕ) ↦ Part.map encode ((↑F : ℕ →. Code) a)
eF' : cF.eval (encode cF) = Part.some (encode (F (encode cF)))
n : ℕ
⊢ (f (cg.curry (encode cF))).eval n = (cg.curry (encode cF)).eval n

Tactic:
simp [F, g, eg', eF', Part.map_id']

Premises used: Part.map_id'
-- Module: Mathlib.Computability.PartrecCode
Goal:
f : Code → ℕ →. ℕ
hf : Partrec₂ f
cf : Code
ef :
  cf.eval = fun (n : ℕ) ↦
    Part.bind (↑(decode n) : Part (Code × ℕ)) fun (a : Code × ℕ) ↦
      Part.map (α := ℕ) encode ((fun (p : Code × ℕ) ↦ f p.1 p.2) a)
c : Code
e : (cf.curry (encode c)).eval = c.eval
n : ℕ
⊢ c.eval n = f c n

Tactic:
simp [e.symm, ef, Part.map_id']

Premises used: Part.map_id', Eq.symm
-- Module: Mathlib.Computability.PartrecCode
Goal:
apply :
  Function.Surjective (β := { f : ℕ →. ℕ // Partrec f }) fun (c : Code) ↦
    Subtype.mk (p := fun (f : ℕ →. ℕ) ↦ Partrec f) c.eval ⋯
⊢ Countable { f : ℕ →. ℕ // Partrec f }

Tactic:
apply Function.Surjective.countable (f := fun c => ⟨eval c, eval_part.comp (.const c) .id⟩)

Premises used: Function.Surjective.countable
-- Module: Mathlib.Computability.PartrecCode
Goal:
f : ℕ →. ℕ
hf : Partrec f
⊢ ∃ (a : Code),
    (fun (c : Code) ↦ Subtype.mk (p := fun (f : ℕ →. ℕ) ↦ Partrec f) c.eval ⋯) a =
      Subtype.mk (p := fun (f : ℕ →. ℕ) ↦ Partrec f) f hf

Tactic:
simpa using exists_code.1 hf

Premises used: Iff.mp, Nat.Partrec.Code.exists_code
-- Module: Mathlib.Computability.PartrecCode
Goal:
x x_1 : { f : ℕ → ℕ // Computable f }
h :
  Eq (α := { f : ℕ →. ℕ // Partrec f })
    ((fun (f : { f : ℕ → ℕ // Computable f }) ↦
        Subtype.mk (p := fun (f : ℕ →. ℕ) ↦ Partrec f) (↑(↑f : ℕ → ℕ) : ℕ →. ℕ) ⋯)
      x)
    ((fun (f : { f : ℕ → ℕ // Computable f }) ↦
        Subtype.mk (p := fun (f : ℕ →. ℕ) ↦ Partrec f) (↑(↑f : ℕ → ℕ) : ℕ →. ℕ) ⋯)
      x_1)
⊢ (↑(↑x : ℕ → ℕ) : ℕ →. ℕ) = (↑(↑x_1 : ℕ → ℕ) : ℕ →. ℕ)

Tactic:
simpa using h
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
f g : ℕ → ℕ
hf : Nat.Primrec f
H : ∀ (n : ℕ), f n = g n
⊢ Nat.Primrec g

Tactic:
(funext H : f = g) ▸ hf

Premises used: Eq.rec, funext
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
n : ℕ
⊢ Nat.pair (unpair n).1 (unpair n).2 = id n

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
f : ℕ → ℕ
m : ℕ
hf : Nat.Primrec f
n : ℕ
⊢ Eq (α := ℕ)
    (unpaired
        (fun (z n : ℕ) ↦
          Nat.rec (motive := fun (x : ℕ) ↦ ℕ) m (fun (y IH : ℕ) ↦ f (unpair (Nat.pair z (Nat.pair y IH))).2) n)
        (Nat.pair 0 (id n)) :
      ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) m (fun (y IH : ℕ) ↦ f (Nat.pair y IH)) n : ℕ)

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
f : ℕ → ℕ
m : ℕ
hf : Nat.Primrec f
⊢ ∀ (n : ℕ),
    Eq (α := ℕ) (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) m (fun (y IH : ℕ) ↦ f (unpair (Nat.pair y IH)).1) n : ℕ)
      (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) n m f : ℕ)

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
n : ℕ
⊢ Eq (α := ℕ)
    (unpaired
      (fun (z n : ℕ) ↦
        Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f z)
          (fun (y IH : ℕ) ↦
            g (Nat.pair (unpair (Nat.pair z (Nat.pair y IH))).1 (unpair (unpair (Nat.pair z (Nat.pair y IH))).2).1))
          n)
      n)
    (unpaired (fun (z n : ℕ) ↦ Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) n (f z) fun (y : ℕ) ↦ g (Nat.pair z y)) n)

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
n : ℕ
⊢ Nat.pair (unpair n).2 (unpair n).1 = unpaired (swap (φ := fun (a a_1 : ℕ) ↦ ℕ) Nat.pair) n

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
f : ℕ → ℕ → ℕ
hf : Nat.Primrec (unpaired f)
n : ℕ
⊢ unpaired f (unpaired (swap (φ := fun (a a_1 : ℕ) ↦ ℕ) Nat.pair) n) = unpaired (swap (φ := fun (a a_1 : ℕ) ↦ ℕ) f) n

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
n : ℕ
zero : Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) 0 0 id = Nat.pred 0
succ : ∀ (n : ℕ), Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (n + 1) 0 id = (n + 1).pred
⊢ Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) n 0 id = n.pred

Tactic:
cases n
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
⊢ Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) 0 0 id = Nat.pred 0

Tactic:
simp [*]
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
n : ℕ
⊢ Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (n + 1) 0 id = (n + 1).pred

Tactic:
simp [*]
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
p : ℕ
simp :
  Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (unpair p).1 (fun (y IH : ℕ) ↦ IH + 1) (unpair p).2 = (unpair p).1 + (unpair p).2
⊢ 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)

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
p : ℕ
zero : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (unpair p).1 (fun (y IH : ℕ) ↦ IH + 1) 0 = (unpair p).1 + 0
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)
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (unpair p).1 (fun (y IH : ℕ) ↦ IH + 1) (unpair p).2 = (unpair p).1 + (unpair p).2

Tactic:
induction p.unpair.2

Premises used: Nat.unpair, Prod.snd
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
p : ℕ
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (unpair p).1 (fun (y IH : ℕ) ↦ IH + 1) 0 = (unpair p).1 + 0

Tactic:
simp [*, Nat.add_assoc]

Premises used: Nat.add_assoc
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
p n : ℕ
h : 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:
simp [*, Nat.add_assoc]

Premises used: Nat.add_assoc
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
p : ℕ
simp :
  Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (unpair p).1 (fun (y IH : ℕ) ↦ IH - 1) (unpair p).2 = (unpair p).1 - (unpair p).2
⊢ 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)

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
p : ℕ
zero : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (unpair p).1 (fun (y IH : ℕ) ↦ IH - 1) 0 = (unpair p).1 - 0
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)
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (unpair p).1 (fun (y IH : ℕ) ↦ IH - 1) (unpair p).2 = (unpair p).1 - (unpair p).2

Tactic:
induction p.unpair.2

Premises used: Nat.unpair, Prod.snd
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
p : ℕ
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (unpair p).1 (fun (y IH : ℕ) ↦ IH - 1) 0 = (unpair p).1 - 0

Tactic:
simp [*, Nat.sub_add_eq]

Premises used: Nat.sub_add_eq
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
p n : ℕ
h : 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:
simp [*, Nat.sub_add_eq]

Premises used: Nat.sub_add_eq
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
p : ℕ
simp :
  Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (y IH : ℕ) ↦ (unpair p).1 + IH) (unpair p).2 = (unpair p).1 * (unpair p).2
⊢ 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)

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
p : ℕ
zero : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (y IH : ℕ) ↦ (unpair p).1 + IH) 0 = (unpair p).1 * 0
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)
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (y IH : ℕ) ↦ (unpair p).1 + IH) (unpair p).2 = (unpair p).1 * (unpair p).2

Tactic:
induction p.unpair.2

Premises used: Nat.unpair, Prod.snd
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
p : ℕ
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (y IH : ℕ) ↦ (unpair p).1 + IH) 0 = (unpair p).1 * 0

Tactic:
simp [*, mul_succ, add_comm _ (unpair p).fst]

Premises used: Nat.mul_succ, Nat.unpair, add_comm, Prod.fst
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
p n : ℕ
h : 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:
simp [*, mul_succ, add_comm _ (unpair p).fst]

Premises used: Nat.mul_succ, Nat.unpair, add_comm, Prod.fst
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
p : ℕ
simp :
  Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 1 (fun (y IH : ℕ) ↦ IH * (unpair p).1) (unpair p).2 = (unpair p).1 ^ (unpair p).2
⊢ 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)

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
p : ℕ
zero : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 1 (fun (y IH : ℕ) ↦ IH * (unpair p).1) 0 = HPow.hPow (β := ℕ) (unpair p).1 0
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)
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 1 (fun (y IH : ℕ) ↦ IH * (unpair p).1) (unpair p).2 = (unpair p).1 ^ (unpair p).2

Tactic:
induction p.unpair.2

Premises used: Nat.unpair, Prod.snd
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
p : ℕ
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 1 (fun (y IH : ℕ) ↦ IH * (unpair p).1) 0 = HPow.hPow (β := ℕ) (unpair p).1 0

Tactic:
simp [*, Nat.pow_succ]

Premises used: Nat.pow_succ
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
p n : ℕ
h : 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:
simp [*, Nat.pow_succ]

Premises used: Nat.pow_succ
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Denumerable α
⊢ ∀ (n : ℕ), n.succ = encode.{u_1} (α := Option α) (decode n)

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
e : β ≃ α
n : ℕ
rw :
  encode.{u_1} (α := Option α) (decode n) =
    encode.{u_2} (α := Option β) (Option.map.{u_1, u_2} (α := α) (⇑e.symm : (a : α) → β) (decode n))
⊢ encode.{u_1} (α := Option α) (decode n) = encode.{u_2} (α := Option β) (decode n)

Tactic:
rw [decode_ofEquiv]

Premises used: Encodable.decode_ofEquiv
-- Module: Mathlib.Computability.Primrec.Basic
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)
some :
  ∀ (val : α),
    encode (Option.some val) = encode.{u_2} (α := Option β) (Option.map (⇑e.symm : (a : α) → β) (Option.some val))
⊢ encode.{u_1} (α := Option α) (decode n) =
    encode.{u_2} (α := Option β) (Option.map.{u_1, u_2} (α := α) (⇑e.symm : (a : α) → β) (decode n))

Tactic:
cases (@decode α _ n)

Premises used: Encodable.decode
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
e : β ≃ α
n : ℕ
⊢ encode.{u_1} (α := Option α) none =
    encode.{u_2} (α := Option β) (Option.map.{u_1, u_2} (α := α) (⇑e.symm : (a : α) → β) none)

Tactic:
simp [encode_ofEquiv]

Premises used: Encodable.encode_ofEquiv
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
e : β ≃ α
n : ℕ
val : α
⊢ encode (some val) = encode.{u_2} (α := Option β) (Option.map (⇑e.symm : (a : α) → β) (some val))

Tactic:
simp [encode_ofEquiv]

Premises used: Encodable.encode_ofEquiv
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
n : ℕ
zero :
  (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) 0 1 fun (x : ℕ) ↦ 0) = encode.{u_1} (α := Option PUnit.{u_1 + 1}) (decode 0)
succ :
  ∀ (n : ℕ),
    (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (n + 1) 1 fun (x : ℕ) ↦ 0) =
      encode.{u_1} (α := Option PUnit.{u_1 + 1}) (decode (n + 1))
⊢ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) n 1 fun (x : ℕ) ↦ 0) = encode.{u_1} (α := Option PUnit.{u_1 + 1}) (decode n)

Tactic:
cases n
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
⊢ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) 0 1 fun (x : ℕ) ↦ 0) = encode.{u_1} (α := Option PUnit.{u_1 + 1}) (decode 0)

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
n : ℕ
⊢ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (n + 1) 1 fun (x : ℕ) ↦ 0) =
    encode.{u_1} (α := Option PUnit.{u_1 + 1}) (decode (n + 1))

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
h : Primcodable α
⊢ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) 0 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 0)

Tactic:
rfl