awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.PartrecCode
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
c : α → Code
hc : Computable c
z : α → σ
hz : Computable z
s : α → σ
hs : Computable s
l : α → σ
hl : Computable l
r : α → σ
hr : Computable r
pr : α → Code × Code × σ × σ → σ
hpr : Computable₂ pr
co : α → Code × Code × σ × σ → σ
hco : Computable₂ co
pc : α → Code × Code × σ × σ → σ
hpc : Computable₂ pc
rf : α → Code × σ → σ
hrf : Computable₂ rf
PR : (a : α) → (cf cg : Code) → (hf hg : σ) → σ := fun (a : α) (cf cg : Code) (hf hg : σ) ↦ pr a (cf, cg, hf, hg)
CO : (a : α) → (cf cg : Code) → (hf hg : σ) → σ := fun (a : α) (cf cg : Code) (hf hg : σ) ↦ co a (cf, cg, hf, hg)
PC : (a : α) → (cf cg : Code) → (hf hg : σ) → σ := fun (a : α) (cf cg : Code) (hf hg : σ) ↦ pc a (cf, cg, hf, hg)
RF : (a : α) → (cf : Code) → (hf : σ) → σ := fun (a : α) (cf : Code) (hf : σ) ↦ rf a (cf, hf)
F : (a : α) → (c : Code) → σ :=
  fun (a : α) (c : Code) ↦
    Code.recOn (motive := fun (x : Code) ↦ σ) c (z a) (s a) (l a) (r a) (PR a) (CO a) (PC a) (RF a)
G₁ : Prod.{u_1, u_2} α (List σ) × ℕ × ℕ → Option σ :=
  fun (p : Prod.{u_1, u_2} α (List σ) × ℕ × ℕ) ↦
    (getElem? (valid := fun (as : List σ) (i : ℕ) ↦ i < as.length) p.1.2 p.2.2).bind fun (s : σ) ↦
      (getElem? (valid := fun (as : List σ) (i : ℕ) ↦ i < as.length) p.1.2 (unpair p.2.2).1).bind fun (s₁ : σ) ↦
        Option.map
          (fun (s₂ : σ) ↦
            bif p.2.1.bodd then
              bif p.2.1.div2.bodd then rf p.1.1 (ofNat Code p.2.2, s)
              else pc p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)
            else
              bif p.2.1.div2.bodd then co p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)
              else pr p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂))
          (getElem? (valid := fun (as : List σ) (i : ℕ) ↦ i < as.length) p.1.2 (unpair p.2.2).2)
this_1 : Computable G₁
G : α → List σ → Option σ :=
  fun (a : α) (IH : List σ) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ Option σ) IH.length (some (z a)) fun (n : ℕ) ↦
      Nat.casesOn (motive := fun (x : ℕ) ↦ Option σ) n (some (s a)) fun (n : ℕ) ↦
        Nat.casesOn (motive := fun (x : ℕ) ↦ Option σ) n (some (l a)) fun (n : ℕ) ↦
          Nat.casesOn (motive := fun (x : ℕ) ↦ Option σ) n (some (r a)) fun (n : ℕ) ↦ G₁ ((a, IH), n, n.div2.div2)
this : Computable₂ G
a : α
n : ℕ
m : ℕ := n.div2.div2
⊢ n / 2 / 2 < n + 4

Tactic:
lt_of_le_of_lt
      (le_trans (Nat.div_le_self ..) (Nat.div_le_self ..))
      (Nat.succ_le_succ (Nat.le_add_right ..))

Premises used: lt_of_le_of_lt, Nat.le_add_right, Nat.div_le_self, Nat.succ_le_succ, le_trans
-- Module: Mathlib.Computability.PartrecCode
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
c : α → Code
hc : Computable c
z : α → σ
hz : Computable z
s : α → σ
hs : Computable s
l : α → σ
hl : Computable l
r : α → σ
hr : Computable r
pr : α → Code × Code × σ × σ → σ
hpr : Computable₂ pr
co : α → Code × Code × σ × σ → σ
hco : Computable₂ co
pc : α → Code × Code × σ × σ → σ
hpc : Computable₂ pc
rf : α → Code × σ → σ
hrf : Computable₂ rf
PR : (a : α) → (cf cg : Code) → (hf hg : σ) → σ := fun (a : α) (cf cg : Code) (hf hg : σ) ↦ pr a (cf, cg, hf, hg)
CO : (a : α) → (cf cg : Code) → (hf hg : σ) → σ := fun (a : α) (cf cg : Code) (hf hg : σ) ↦ co a (cf, cg, hf, hg)
PC : (a : α) → (cf cg : Code) → (hf hg : σ) → σ := fun (a : α) (cf cg : Code) (hf hg : σ) ↦ pc a (cf, cg, hf, hg)
RF : (a : α) → (cf : Code) → (hf : σ) → σ := fun (a : α) (cf : Code) (hf : σ) ↦ rf a (cf, hf)
F : (a : α) → (c : Code) → σ :=
  fun (a : α) (c : Code) ↦
    Code.recOn (motive := fun (x : Code) ↦ σ) c (z a) (s a) (l a) (r a) (PR a) (CO a) (PC a) (RF a)
G₁ : Prod.{u_1, u_2} α (List σ) × ℕ × ℕ → Option σ :=
  fun (p : Prod.{u_1, u_2} α (List σ) × ℕ × ℕ) ↦
    (getElem? (valid := fun (as : List σ) (i : ℕ) ↦ i < as.length) p.1.2 p.2.2).bind fun (s : σ) ↦
      (getElem? (valid := fun (as : List σ) (i : ℕ) ↦ i < as.length) p.1.2 (unpair p.2.2).1).bind fun (s₁ : σ) ↦
        Option.map
          (fun (s₂ : σ) ↦
            bif p.2.1.bodd then
              bif p.2.1.div2.bodd then rf p.1.1 (ofNat Code p.2.2, s)
              else pc p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)
            else
              bif p.2.1.div2.bodd then co p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)
              else pr p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂))
          (getElem? (valid := fun (as : List σ) (i : ℕ) ↦ i < as.length) p.1.2 (unpair p.2.2).2)
this_1 : Computable G₁
G : α → List σ → Option σ :=
  fun (a : α) (IH : List σ) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ Option σ) IH.length (some (z a)) fun (n : ℕ) ↦
      Nat.casesOn (motive := fun (x : ℕ) ↦ Option σ) n (some (s a)) fun (n : ℕ) ↦
        Nat.casesOn (motive := fun (x : ℕ) ↦ Option σ) n (some (l a)) fun (n : ℕ) ↦
          Nat.casesOn (motive := fun (x : ℕ) ↦ Option σ) n (some (r a)) fun (n : ℕ) ↦ G₁ ((a, IH), n, n.div2.div2)
this : Computable₂ G
a : α
n : ℕ
m : ℕ := n.div2.div2
⊢ n / 2 / 2 < n + 4

Tactic:
exact lt_of_le_of_lt
      (le_trans (Nat.div_le_self ..) (Nat.div_le_self ..))
      (Nat.succ_le_succ (Nat.le_add_right ..))

Premises used: lt_of_le_of_lt, Nat.le_add_right, Nat.div_le_self, Nat.succ_le_succ, le_trans
-- Module: Mathlib.Computability.PartrecCode
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
c : α → Code
hc : Computable c
z : α → σ
hz : Computable z
s : α → σ
hs : Computable s
l : α → σ
hl : Computable l
r : α → σ
hr : Computable r
pr : α → Code × Code × σ × σ → σ
hpr : Computable₂ pr
co : α → Code × Code × σ × σ → σ
hco : Computable₂ co
pc : α → Code × Code × σ × σ → σ
hpc : Computable₂ pc
rf : α → Code × σ → σ
hrf : Computable₂ rf
PR : (a : α) → (cf cg : Code) → (hf hg : σ) → σ := fun (a : α) (cf cg : Code) (hf hg : σ) ↦ pr a (cf, cg, hf, hg)
CO : (a : α) → (cf cg : Code) → (hf hg : σ) → σ := fun (a : α) (cf cg : Code) (hf hg : σ) ↦ co a (cf, cg, hf, hg)
PC : (a : α) → (cf cg : Code) → (hf hg : σ) → σ := fun (a : α) (cf cg : Code) (hf hg : σ) ↦ pc a (cf, cg, hf, hg)
RF : (a : α) → (cf : Code) → (hf : σ) → σ := fun (a : α) (cf : Code) (hf : σ) ↦ rf a (cf, hf)
F : (a : α) → (c : Code) → σ :=
  fun (a : α) (c : Code) ↦
    Code.recOn (motive := fun (x : Code) ↦ σ) c (z a) (s a) (l a) (r a) (PR a) (CO a) (PC a) (RF a)
G₁ : Prod.{u_1, u_2} α (List σ) × ℕ × ℕ → Option σ :=
  fun (p : Prod.{u_1, u_2} α (List σ) × ℕ × ℕ) ↦
    (getElem? (valid := fun (as : List σ) (i : ℕ) ↦ i < as.length) p.1.2 p.2.2).bind fun (s : σ) ↦
      (getElem? (valid := fun (as : List σ) (i : ℕ) ↦ i < as.length) p.1.2 (unpair p.2.2).1).bind fun (s₁ : σ) ↦
        Option.map
          (fun (s₂ : σ) ↦
            bif p.2.1.bodd then
              bif p.2.1.div2.bodd then rf p.1.1 (ofNat Code p.2.2, s)
              else pc p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)
            else
              bif p.2.1.div2.bodd then co p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)
              else pr p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂))
          (getElem? (valid := fun (as : List σ) (i : ℕ) ↦ i < as.length) p.1.2 (unpair p.2.2).2)
this_1 : Computable G₁
G : α → List σ → Option σ :=
  fun (a : α) (IH : List σ) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ Option σ) IH.length (some (z a)) fun (n : ℕ) ↦
      Nat.casesOn (motive := fun (x : ℕ) ↦ Option σ) n (some (s a)) fun (n : ℕ) ↦
        Nat.casesOn (motive := fun (x : ℕ) ↦ Option σ) n (some (l a)) fun (n : ℕ) ↦
          Nat.casesOn (motive := fun (x : ℕ) ↦ Option σ) n (some (r a)) fun (n : ℕ) ↦ G₁ ((a, IH), n, n.div2.div2)
this : Computable₂ G
a : α
n : ℕ
m : ℕ := n.div2.div2
⊢ m < n + 4

Tactic:
have hm : m < n + 4 := by
    simp only [m, div2_val]
    exact lt_of_le_of_lt
      (le_trans (Nat.div_le_self ..) (Nat.div_le_self ..))
      (Nat.succ_le_succ (Nat.le_add_right ..))
-- Module: Mathlib.Computability.PartrecCode
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
c : α → Code
hc : Computable c
z : α → σ
hz : Computable z
s : α → σ
hs : Computable s
l : α → σ
hl : Computable l
r : α → σ
hr : Computable r
pr : α → Code × Code × σ × σ → σ
hpr : Computable₂ pr
co : α → Code × Code × σ × σ → σ
hco : Computable₂ co
pc : α → Code × Code × σ × σ → σ
hpc : Computable₂ pc
rf : α → Code × σ → σ
hrf : Computable₂ rf
PR : (a : α) → (cf cg : Code) → (hf hg : σ) → σ := fun (a : α) (cf cg : Code) (hf hg : σ) ↦ pr a (cf, cg, hf, hg)
CO : (a : α) → (cf cg : Code) → (hf hg : σ) → σ := fun (a : α) (cf cg : Code) (hf hg : σ) ↦ co a (cf, cg, hf, hg)
PC : (a : α) → (cf cg : Code) → (hf hg : σ) → σ := fun (a : α) (cf cg : Code) (hf hg : σ) ↦ pc a (cf, cg, hf, hg)
RF : (a : α) → (cf : Code) → (hf : σ) → σ := fun (a : α) (cf : Code) (hf : σ) ↦ rf a (cf, hf)
F : (a : α) → (c : Code) → σ :=
  fun (a : α) (c : Code) ↦
    Code.recOn (motive := fun (x : Code) ↦ σ) c (z a) (s a) (l a) (r a) (PR a) (CO a) (PC a) (RF a)
G₁ : Prod.{u_1, u_2} α (List σ) × ℕ × ℕ → Option σ :=
  fun (p : Prod.{u_1, u_2} α (List σ) × ℕ × ℕ) ↦
    (getElem? (valid := fun (as : List σ) (i : ℕ) ↦ i < as.length) p.1.2 p.2.2).bind fun (s : σ) ↦
      (getElem? (valid := fun (as : List σ) (i : ℕ) ↦ i < as.length) p.1.2 (unpair p.2.2).1).bind fun (s₁ : σ) ↦
        Option.map
          (fun (s₂ : σ) ↦
            bif p.2.1.bodd then
              bif p.2.1.div2.bodd then rf p.1.1 (ofNat Code p.2.2, s)
              else pc p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)
            else
              bif p.2.1.div2.bodd then co p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)
              else pr p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂))
          (getElem? (valid := fun (as : List σ) (i : ℕ) ↦ i < as.length) p.1.2 (unpair p.2.2).2)
this_1 : Computable G₁
G : α → List σ → Option σ :=
  fun (a : α) (IH : List σ) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ Option σ) IH.length (some (z a)) fun (n : ℕ) ↦
      Nat.casesOn (motive := fun (x : ℕ) ↦ Option σ) n (some (s a)) fun (n : ℕ) ↦
        Nat.casesOn (motive := fun (x : ℕ) ↦ Option σ) n (some (l a)) fun (n : ℕ) ↦
          Nat.casesOn (motive := fun (x : ℕ) ↦ Option σ) n (some (r a)) fun (n : ℕ) ↦ G₁ ((a, IH), n, n.div2.div2)
this : Computable₂ G
a : α
n : ℕ
m : ℕ := n.div2.div2
hm : m < n + 4
⊢ (unpair m).1 < n + 4

Tactic:
have m1 : m.unpair.1 < n + 4 := lt_of_le_of_lt m.unpair_left_le hm
-- Module: Mathlib.Computability.PartrecCode
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
c : α → Code
hc : Computable c
z : α → σ
hz : Computable z
s : α → σ
hs : Computable s
l : α → σ
hl : Computable l
r : α → σ
hr : Computable r
pr : α → Code × Code × σ × σ → σ
hpr : Computable₂ pr
co : α → Code × Code × σ × σ → σ
hco : Computable₂ co
pc : α → Code × Code × σ × σ → σ
hpc : Computable₂ pc
rf : α → Code × σ → σ
hrf : Computable₂ rf
PR : (a : α) → (cf cg : Code) → (hf hg : σ) → σ := fun (a : α) (cf cg : Code) (hf hg : σ) ↦ pr a (cf, cg, hf, hg)
CO : (a : α) → (cf cg : Code) → (hf hg : σ) → σ := fun (a : α) (cf cg : Code) (hf hg : σ) ↦ co a (cf, cg, hf, hg)
PC : (a : α) → (cf cg : Code) → (hf hg : σ) → σ := fun (a : α) (cf cg : Code) (hf hg : σ) ↦ pc a (cf, cg, hf, hg)
RF : (a : α) → (cf : Code) → (hf : σ) → σ := fun (a : α) (cf : Code) (hf : σ) ↦ rf a (cf, hf)
F : (a : α) → (c : Code) → σ :=
  fun (a : α) (c : Code) ↦
    Code.recOn (motive := fun (x : Code) ↦ σ) c (z a) (s a) (l a) (r a) (PR a) (CO a) (PC a) (RF a)
G₁ : Prod.{u_1, u_2} α (List σ) × ℕ × ℕ → Option σ :=
  fun (p : Prod.{u_1, u_2} α (List σ) × ℕ × ℕ) ↦
    (getElem? (valid := fun (as : List σ) (i : ℕ) ↦ i < as.length) p.1.2 p.2.2).bind fun (s : σ) ↦
      (getElem? (valid := fun (as : List σ) (i : ℕ) ↦ i < as.length) p.1.2 (unpair p.2.2).1).bind fun (s₁ : σ) ↦
        Option.map
          (fun (s₂ : σ) ↦
            bif p.2.1.bodd then
              bif p.2.1.div2.bodd then rf p.1.1 (ofNat Code p.2.2, s)
              else pc p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)
            else
              bif p.2.1.div2.bodd then co p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)
              else pr p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂))
          (getElem? (valid := fun (as : List σ) (i : ℕ) ↦ i < as.length) p.1.2 (unpair p.2.2).2)
this_1 : Computable G₁
G : α → List σ → Option σ :=
  fun (a : α) (IH : List σ) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ Option σ) IH.length (some (z a)) fun (n : ℕ) ↦
      Nat.casesOn (motive := fun (x : ℕ) ↦ Option σ) n (some (s a)) fun (n : ℕ) ↦
        Nat.casesOn (motive := fun (x : ℕ) ↦ Option σ) n (some (l a)) fun (n : ℕ) ↦
          Nat.casesOn (motive := fun (x : ℕ) ↦ Option σ) n (some (r a)) fun (n : ℕ) ↦ G₁ ((a, IH), n, n.div2.div2)
this : Computable₂ G
a : α
n : ℕ
m : ℕ := n.div2.div2
hm : m < n + 4
m1 : (unpair m).1 < n + 4
⊢ (unpair m).2 < n + 4

Tactic:
have m2 : m.unpair.2 < n + 4 := lt_of_le_of_lt m.unpair_right_le hm
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
a : ℕ
rw :
  Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval (a, 0).1)
      (fun (y : ℕ) (IH : Part ℕ) ↦ do
        let i ← IH
        cg.eval (Nat.pair (a, 0).1 (Nat.pair y i)))
      (a, 0).2 =
    cf.eval a
⊢ (cf.prec cg).eval (Nat.pair a 0) = cf.eval a

Tactic:
rw [eval, Nat.unpaired, Nat.unpair_pair]

Premises used: Nat.unpaired, Nat.Partrec.Code.eval, Nat.unpair_pair
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
a : ℕ
simp :
  Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval a)
      (fun (y : ℕ) (IH : Part ℕ) ↦ do
        let i ← IH
        cg.eval (Nat.pair a (Nat.pair y i)))
      0 =
    cf.eval a
⊢ Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval (a, 0).1)
      (fun (y : ℕ) (IH : Part ℕ) ↦ do
        let i ← IH
        cg.eval (Nat.pair (a, 0).1 (Nat.pair y i)))
      (a, 0).2 =
    cf.eval a

Tactic:
simp (config := { Lean.Meta.Simp.neutralConfig with proj := true }) only []

Premises used: Lean.Meta.Simp.neutralConfig
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
a : ℕ
rw rw₁ : cf.eval a = cf.eval a
⊢ Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval a)
      (fun (y : ℕ) (IH : Part ℕ) ↦ do
        let i ← IH
        cg.eval (Nat.pair a (Nat.pair y i)))
      0 =
    cf.eval a

Tactic:
rw [Nat.rec_zero]

Premises used: Nat.rec_zero
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
a k : ℕ
rw :
  Eq (α := Part ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval (a, k.succ).1)
        (fun (y : ℕ) (IH : Part ℕ) ↦ do
          let i ← IH
          cg.eval (Nat.pair (a, k.succ).1 (Nat.pair y i)))
        (a, k.succ).2 :
      Part ℕ)
    (Part.bind
        (unpaired
          (fun (a n : ℕ) ↦
            Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval a)
              (fun (y : ℕ) (IH : Part ℕ) ↦ do
                let i ← IH
                cg.eval (Nat.pair a (Nat.pair y i)))
              n)
          (Nat.pair a k))
        fun (ih : ℕ) ↦ cg.eval (Nat.pair a (Nat.pair k ih)) :
      Part ℕ)
⊢ (cf.prec cg).eval (Nat.pair a k.succ) = do
    let ih ← (cf.prec cg).eval (Nat.pair a k)
    cg.eval (Nat.pair a (Nat.pair k ih))

Tactic:
rw [eval, Nat.unpaired, Part.bind_eq_bind, Nat.unpair_pair]

Premises used: Nat.unpaired, Nat.Partrec.Code.eval, Nat.unpair_pair, Part.bind_eq_bind
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
a k : ℕ
⊢ Eq (α := Part ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval (a, k.succ).1)
        (fun (y : ℕ) (IH : Part ℕ) ↦ do
          let i ← IH
          cg.eval (Nat.pair (a, k.succ).1 (Nat.pair y i)))
        (a, k.succ).2 :
      Part ℕ)
    (Part.bind
        (unpaired
          (fun (a n : ℕ) ↦
            Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval a)
              (fun (y : ℕ) (IH : Part ℕ) ↦ do
                let i ← IH
                cg.eval (Nat.pair a (Nat.pair y i)))
              n)
          (Nat.pair a k))
        fun (ih : ℕ) ↦ cg.eval (Nat.pair a (Nat.pair k ih)) :
      Part ℕ)

Tactic:
simp
-- Module: Mathlib.Computability.PartrecCode
Goal:
n m : ℕ
⊢ (Code.const (n + 1)).eval m = Part.some (n + 1)

Tactic:
simp! [eval_const n m]
-- Module: Mathlib.Computability.PartrecCode
Goal:
n : ℕ
⊢ Code.id.eval n = Part.some n

Tactic:
simp! [Seq.seq, Code.id]

Premises used: Seq.seq, Nat.Partrec.Code.id
-- Module: Mathlib.Computability.PartrecCode
Goal:
c : Code
n x : ℕ
⊢ (c.curry n).eval x = c.eval (Nat.pair n x)

Tactic:
simp! [Seq.seq, curry]

Premises used: Seq.seq, Nat.Partrec.Code.curry
-- Module: Mathlib.Computability.PartrecCode
Goal:
n : ℕ
simp : (fun (b : Code) ↦ succ.comp b)^[n] zero = Code.const n
⊢ (fun (b : Code) ↦ succ.comp (n, b).2)^[id n] zero = Code.const n

Tactic:
simp
-- Module: Mathlib.Computability.PartrecCode
Goal:
n : ℕ
zero : (fun (b : Code) ↦ Code.succ.comp b)^[0] Code.zero = Code.const 0
succ :
  ∀ (n : ℕ),
    (fun (b : Code) ↦ Code.succ.comp b)^[n] Code.zero = Code.const n →
      (fun (b : Code) ↦ Code.succ.comp b)^[n + 1] Code.zero = Code.const (n + 1)
⊢ (fun (b : Code) ↦ Code.succ.comp b)^[n] Code.zero = Code.const n

Tactic:
induction n
-- Module: Mathlib.Computability.PartrecCode
Goal:
⊢ (fun (b : Code) ↦ succ.comp b)^[0] zero = Code.const 0

Tactic:
simp [*, Code.const, Function.iterate_succ', -Function.iterate_succ]

Premises used: Nat.Partrec.Code.const, Function.iterate_succ, Function.iterate_succ'
-- Module: Mathlib.Computability.PartrecCode
Goal:
n : ℕ
h : (fun (b : Code) ↦ succ.comp b)^[n] zero = Code.const n
⊢ (fun (b : Code) ↦ succ.comp b)^[n + 1] zero = Code.const (n + 1)

Tactic:
simp [*, Code.const, Function.iterate_succ', -Function.iterate_succ]

Premises used: Nat.Partrec.Code.const, Function.iterate_succ, Function.iterate_succ'
-- Module: Mathlib.Computability.PartrecCode
Goal:
⊢ Primrec₂ curry

Tactic:
primrec₂_comp.comp Primrec.fst <| primrec₂_pair.comp (primrec_const.comp Primrec.snd)
    (_root_.Primrec.const Code.id)

Premises used: Primrec.snd, Nat.Partrec.Code.primrec₂_comp, Primrec.fst, Nat.Partrec.Code.primrec₂_pair, Primrec.const, Nat.Partrec.Code.id, Primrec.comp, Nat.Partrec.Code.curry, Primrec₂.comp, Nat.Partrec.Code.primrec_const, Primrec₂
-- Module: Mathlib.Computability.PartrecCode
Goal:
c₁ c₂ : Code
n₁ n₂ : ℕ
h : c₁.curry n₁ = c₂.curry n₂
⊢ c₁ = c₂

Tactic:
injection h
-- Module: Mathlib.Computability.PartrecCode
Goal:
c₁ c₂ : Code
n₁ n₂ : ℕ
h : c₁.curry n₁ = c₂.curry n₂
⊢ c₁ = c₂

Tactic:
injection h with h₁ h₂
-- Module: Mathlib.Computability.PartrecCode
Goal:
c₁ c₂ : Code
n₁ n₂ : ℕ
h : c₁.curry n₁ = c₂.curry n₂
h₁ : c₁ = c₂
⊢ (Code.const n₁).pair Code.id = (Code.const n₂).pair Code.id

Tactic:
injection h with h₁ h₂
-- Module: Mathlib.Computability.PartrecCode
Goal:
c₁ c₂ : Code
n₁ n₂ : ℕ
h₁ : c₁ = c₂
h₂ : (Code.const n₁).pair Code.id = (Code.const n₂).pair Code.id
⊢ Code.const n₁ = Code.const n₂

Tactic:
injection h₂ with h₃ h₄
-- Module: Mathlib.Computability.PartrecCode
Goal:
c₁ c₂ : Code
n₁ n₂ : ℕ
h₁ : c₁ = c₂
h₂ : (Code.const n₁).pair Code.id = (Code.const n₂).pair Code.id
h₃ : Code.const n₁ = Code.const n₂
⊢ Code.id = Code.id

Tactic:
injection h₂ with h₃ h₄
-- Module: Mathlib.Computability.PartrecCode
Goal:
c₁ c₂ : Code
n₁ n₂ : ℕ
h₁ : c₁ = c₂
h₃ : Code.const n₁ = Code.const n₂
h₄ : Code.id = Code.id
⊢ n₁ = n₂

Tactic:
const_inj h₃

Premises used: Nat.Partrec.Code.const_inj
-- Module: Mathlib.Computability.PartrecCode
Goal:
c₁ c₂ : Code
n₁ n₂ : ℕ
h₁ : c₁ = c₂
h₃ : Code.const n₁ = Code.const n₂
h₄ : Code.id = Code.id
⊢ n₁ = n₂

Tactic:
exact const_inj h₃

Premises used: Nat.Partrec.Code.const_inj
-- Module: Mathlib.Computability.PartrecCode
Goal:
⊢ ∃ (f : Code → ℕ → Code), Computable₂ f ∧ ∀ (c : Code) (n x : ℕ), (f c n).eval x = c.eval (Nat.pair n x)

Tactic:
⟨curry, Primrec₂.to_comp primrec₂_curry, eval_curry⟩

Premises used: Nat.Partrec.Code.primrec₂_curry, And.intro, Exists.intro, Nat.Partrec.Code.curry, Primrec₂.to_comp, Nat.Partrec.Code.eval_curry
-- Module: Mathlib.Computability.PartrecCode
Goal:
f : ℕ →. ℕ
⊢ Nat.Partrec f ↔ ∃ (c : Code), c.eval = f

Tactic:
⟨fun h => ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Computability.PartrecCode
Goal:
f : ℕ →. ℕ
refine_1 : ∀ (h : Nat.Partrec f), ∃ (c : Code), c.eval = f
refine_2 : (∃ (c : Code), c.eval = f) → Nat.Partrec f
⊢ Nat.Partrec f ↔ ∃ (c : Code), c.eval = f

Tactic:
refine ⟨fun h => ?_, ?_⟩
-- Module: Mathlib.Computability.PartrecCode
Goal:
f : ℕ →. ℕ
⊢ ∃ (c : Code), c.eval = pure 0

Tactic:
⟨zero, rfl⟩

Premises used: Exists.intro, Nat.Partrec.Code.zero, rfl
-- Module: Mathlib.Computability.PartrecCode
Goal:
f : ℕ →. ℕ
⊢ ∃ (c : Code), c.eval = pure 0

Tactic:
exact ⟨zero, rfl⟩
-- Module: Mathlib.Computability.PartrecCode
Goal:
f : ℕ →. ℕ
⊢ ∃ (c : Code), c.eval = (↑Nat.succ : ℕ →. ℕ)

Tactic:
⟨succ, rfl⟩

Premises used: Nat.Partrec.Code.succ, Exists.intro, rfl
-- Module: Mathlib.Computability.PartrecCode
Goal:
f : ℕ →. ℕ
⊢ ∃ (c : Code), c.eval = (↑Nat.succ : ℕ →. ℕ)

Tactic:
exact ⟨succ, rfl⟩
-- Module: Mathlib.Computability.PartrecCode
Goal:
f : ℕ →. ℕ
⊢ ∃ (c : Code), c.eval = (↑fun (n : ℕ) ↦ (unpair n).1 : ℕ →. ℕ)

Tactic:
⟨left, rfl⟩

Premises used: Nat.Partrec.Code.left, Exists.intro, rfl
-- Module: Mathlib.Computability.PartrecCode
Goal:
f : ℕ →. ℕ
⊢ ∃ (c : Code), c.eval = (↑fun (n : ℕ) ↦ (unpair n).1 : ℕ →. ℕ)

Tactic:
exact ⟨left, rfl⟩
-- Module: Mathlib.Computability.PartrecCode
Goal:
f : ℕ →. ℕ
⊢ ∃ (c : Code), c.eval = (↑fun (n : ℕ) ↦ (unpair n).2 : ℕ →. ℕ)

Tactic:
⟨right, rfl⟩

Premises used: Nat.Partrec.Code.right, Exists.intro, rfl
-- Module: Mathlib.Computability.PartrecCode
Goal:
f : ℕ →. ℕ
⊢ ∃ (c : Code), c.eval = (↑fun (n : ℕ) ↦ (unpair n).2 : ℕ →. ℕ)

Tactic:
exact ⟨right, rfl⟩
-- Module: Mathlib.Computability.PartrecCode
Goal:
f f_1 g : ℕ →. ℕ
pf : Nat.Partrec f_1
pg : Nat.Partrec g
hf : ∃ (c : Code), c.eval = f_1
hg : ∃ (c : Code), c.eval = g
refine_1 : ∀ (cf : Code) (pf : Nat.Partrec cf.eval), ∃ (c : Code), c.eval = fun (n : ℕ) ↦ Nat.pair <$> cf.eval n <*> g n
⊢ ∃ (c : Code), c.eval = fun (n : ℕ) ↦ Nat.pair <$> f_1 n <*> g n

Tactic:
rcases hf with ⟨cf, rfl⟩

Premises used: rfl
-- Module: Mathlib.Computability.PartrecCode
Goal:
f g : ℕ →. ℕ
pg : Nat.Partrec g
hg : ∃ (c : Code), c.eval = g
cf : Code
pf : Nat.Partrec cf.eval
refine_1 :
  ∀ (cg : Code) (pg : Nat.Partrec cg.eval), ∃ (c : Code), c.eval = fun (n : ℕ) ↦ Nat.pair <$> cf.eval n <*> cg.eval n
⊢ ∃ (c : Code), c.eval = fun (n : ℕ) ↦ Nat.pair <$> cf.eval n <*> g n

Tactic:
rcases hg with ⟨cg, rfl⟩

Premises used: rfl
-- Module: Mathlib.Computability.PartrecCode
Goal:
f : ℕ →. ℕ
cf : Code
pf : Nat.Partrec cf.eval
cg : Code
pg : Nat.Partrec cg.eval
⊢ ∃ (c : Code), c.eval = fun (n : ℕ) ↦ Nat.pair <$> cf.eval n <*> cg.eval n

Tactic:
⟨pair cf cg, rfl⟩

Premises used: Exists.intro, Nat.Partrec.Code.pair, rfl
-- Module: Mathlib.Computability.PartrecCode
Goal:
f : ℕ →. ℕ
cf : Code
pf : Nat.Partrec cf.eval
cg : Code
pg : Nat.Partrec cg.eval
⊢ ∃ (c : Code), c.eval = fun (n : ℕ) ↦ Nat.pair <$> cf.eval n <*> cg.eval n

Tactic:
exact ⟨pair cf cg, rfl⟩
-- Module: Mathlib.Computability.PartrecCode
Goal:
f f_1 g : ℕ →. ℕ
pf : Nat.Partrec f_1
pg : Nat.Partrec g
hf : ∃ (c : Code), c.eval = f_1
hg : ∃ (c : Code), c.eval = g
refine_1 : ∀ (cf : Code) (pf : Nat.Partrec cf.eval), ∃ (c : Code), c.eval = fun (n : ℕ) ↦ g n >>= cf.eval
⊢ ∃ (c : Code), c.eval = fun (n : ℕ) ↦ g n >>= f_1

Tactic:
rcases hf with ⟨cf, rfl⟩

Premises used: rfl
-- Module: Mathlib.Computability.PartrecCode
Goal:
f g : ℕ →. ℕ
pg : Nat.Partrec g
hg : ∃ (c : Code), c.eval = g
cf : Code
pf : Nat.Partrec cf.eval
refine_1 : ∀ (cg : Code) (pg : Nat.Partrec cg.eval), ∃ (c : Code), c.eval = fun (n : ℕ) ↦ cg.eval n >>= cf.eval
⊢ ∃ (c : Code), c.eval = fun (n : ℕ) ↦ g n >>= cf.eval

Tactic:
rcases hg with ⟨cg, rfl⟩

Premises used: rfl
-- Module: Mathlib.Computability.PartrecCode
Goal:
f : ℕ →. ℕ
cf : Code
pf : Nat.Partrec cf.eval
cg : Code
pg : Nat.Partrec cg.eval
⊢ ∃ (c : Code), c.eval = fun (n : ℕ) ↦ cg.eval n >>= cf.eval

Tactic:
⟨comp cf cg, rfl⟩

Premises used: Nat.Partrec.Code.comp, Exists.intro, rfl