awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact ⟨comp 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 =
        unpaired fun (a n : ℕ) ↦
          Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval a)
            (fun (y : ℕ) (IH : Part ℕ) ↦ do
              let i ← IH
              g (Nat.pair a (Nat.pair y i)))
            n
⊢ ∃ (c : Code),
    c.eval =
      unpaired fun (a n : ℕ) ↦
        Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (f_1 a)
          (fun (y : ℕ) (IH : Part ℕ) ↦ do
            let i ← IH
            g (Nat.pair a (Nat.pair y i)))
          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 =
        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
⊢ ∃ (c : Code),
    c.eval =
      unpaired fun (a n : ℕ) ↦
        Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval a)
          (fun (y : ℕ) (IH : Part ℕ) ↦ do
            let i ← IH
            g (Nat.pair a (Nat.pair y i)))
          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 =
      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

Tactic:
⟨prec cf cg, rfl⟩

Premises used: Nat.Partrec.Code.prec, Exists.intro, 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 =
      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

Tactic:
exact ⟨prec cf cg, rfl⟩
-- Module: Mathlib.Computability.PartrecCode
Goal:
f f_1 : ℕ →. ℕ
pf : Nat.Partrec f_1
hf : ∃ (c : Code), c.eval = f_1
refine_1 :
  ∀ (cf : Code) (pf : Nat.Partrec cf.eval),
    ∃ (c : Code),
      c.eval = fun (a : ℕ) ↦ Nat.rfind fun (n : ℕ) ↦ (fun (m : ℕ) ↦ decide (m = 0)) <$> cf.eval (Nat.pair a n)
⊢ ∃ (c : Code), c.eval = fun (a : ℕ) ↦ Nat.rfind fun (n : ℕ) ↦ (fun (m : ℕ) ↦ decide (m = 0)) <$> f_1 (Nat.pair a n)

Tactic:
rcases hf with ⟨cf, rfl⟩

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

Tactic:
⟨comp (rfind' cf) (pair Code.id zero), ?_⟩

Premises used: Nat.Partrec.Code.rfind', Nat.Partrec.Code.id, Nat.Partrec.Code.comp, Exists.intro, Nat.Partrec.Code.zero, Nat.Partrec.Code.pair
-- Module: Mathlib.Computability.PartrecCode
Goal:
f : ℕ →. ℕ
cf : Code
pf : Nat.Partrec cf.eval
refine_1 :
  (cf.rfind'.comp (Code.id.pair zero)).eval = fun (a : ℕ) ↦
    Nat.rfind fun (n : ℕ) ↦ (fun (m : ℕ) ↦ decide (m = 0)) <$> cf.eval (Nat.pair a n)
⊢ ∃ (c : Code), c.eval = fun (a : ℕ) ↦ Nat.rfind fun (n : ℕ) ↦ (fun (m : ℕ) ↦ decide (m = 0)) <$> cf.eval (Nat.pair a n)

Tactic:
refine ⟨comp (rfind' cf) (pair Code.id zero), ?_⟩
-- Module: Mathlib.Computability.PartrecCode
Goal:
f : ℕ →. ℕ
cf : Code
pf : Nat.Partrec cf.eval
⊢ (cf.rfind'.comp (Code.id.pair zero)).eval = fun (a : ℕ) ↦
    Nat.rfind fun (n : ℕ) ↦ (fun (m : ℕ) ↦ decide (m = 0)) <$> cf.eval (Nat.pair a n)

Tactic:
simp [eval, Seq.seq, pure, PFun.pure, Part.map_id']

Premises used: Pure.pure, Seq.seq, Part.map_id', PFun.pure, Nat.Partrec.Code.eval
-- Module: Mathlib.Computability.PartrecCode
Goal:
f : ℕ →. ℕ
h : Nat.Partrec f
refine_1 : ∃ (c : Code), c.eval = pure 0
refine_1₁ : ∃ (c : Code), c.eval = (↑Nat.succ : ℕ →. ℕ)
refine_1₂ : ∃ (c : Code), c.eval = (↑fun (n : ℕ) ↦ (unpair n).1 : ℕ →. ℕ)
refine_1₃ : ∃ (c : Code), c.eval = (↑fun (n : ℕ) ↦ (unpair n).2 : ℕ →. ℕ)
refine_1₄ :
  ∀ {f g : ℕ →. ℕ} (pf : Nat.Partrec f) (pg : Nat.Partrec g) (hf : ∃ (c : Code), c.eval = f)
    (hg : ∃ (c : Code), c.eval = g), ∃ (c : Code), c.eval = fun (n : ℕ) ↦ Nat.pair <$> f n <*> g n
refine_1₅ :
  ∀ {f g : ℕ →. ℕ} (pf : Nat.Partrec f) (pg : Nat.Partrec g) (hf : ∃ (c : Code), c.eval = f)
    (hg : ∃ (c : Code), c.eval = g), ∃ (c : Code), c.eval = fun (n : ℕ) ↦ g n >>= f
refine_1₆ :
  ∀ {f g : ℕ →. ℕ} (pf : Nat.Partrec f) (pg : Nat.Partrec g) (hf : ∃ (c : Code), c.eval = f)
    (hg : ∃ (c : Code), c.eval = g),
    ∃ (c : Code),
      c.eval =
        unpaired fun (a n : ℕ) ↦
          Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (f a)
            (fun (y : ℕ) (IH : Part ℕ) ↦ do
              let i ← IH
              g (Nat.pair a (Nat.pair y i)))
            n
refine_1₇ :
  ∀ {f : ℕ →. ℕ} (pf : Nat.Partrec f) (hf : ∃ (c : Code), c.eval = f),
    ∃ (c : Code), c.eval = fun (a : ℕ) ↦ Nat.rfind fun (n : ℕ) ↦ (fun (m : ℕ) ↦ decide (m = 0)) <$> f (Nat.pair a n)
⊢ ∃ (c : Code), c.eval = f

Tactic:
induction h with
    | zero => exact ⟨zero, rfl⟩
    | succ => exact ⟨succ, rfl⟩
    | left => exact ⟨left, rfl⟩
    | right => exact ⟨right, rfl⟩
    | pair pf pg hf hg =>
      rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
      exact ⟨pair cf cg, rfl⟩
    | comp pf pg hf hg =>
      rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
      exact ⟨comp cf cg, rfl⟩
    | prec pf pg hf hg =>
      rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
      exact ⟨prec cf cg, rfl⟩
    | rfind pf hf =>
      rcases hf with ⟨cf, rfl⟩
      refine ⟨comp (rfind' cf) (pair Code.id zero), ?_⟩
      simp [eval, Seq.seq, pure, PFun.pure, Part.map_id']

Premises used: Pure.pure, Nat.Partrec.Code.right, Nat.Partrec.rfind, Nat.Partrec.Code.prec, Nat.Partrec.Code.succ, Seq.seq, Nat.Partrec.Code.left, Nat.Partrec.Code.comp, Part.map_id', Nat.Partrec.Code.zero, PFun.pure, Nat.Partrec.Code.eval, Nat.Partrec.Code.pair, rfl
-- Module: Mathlib.Computability.PartrecCode
Goal:
⊢ Nat.Partrec zero.eval

Tactic:
Nat.Partrec.zero

Premises used: Nat.Partrec.zero, Nat.Partrec.Code.eval
-- Module: Mathlib.Computability.PartrecCode
Goal:
⊢ Nat.Partrec zero.eval

Tactic:
exact Nat.Partrec.zero

Premises used: Nat.Partrec.zero
-- Module: Mathlib.Computability.PartrecCode
Goal:
⊢ Nat.Partrec succ.eval

Tactic:
Nat.Partrec.succ

Premises used: Nat.Partrec.succ, Nat.Partrec.Code.eval
-- Module: Mathlib.Computability.PartrecCode
Goal:
⊢ Nat.Partrec succ.eval

Tactic:
exact Nat.Partrec.succ

Premises used: Nat.Partrec.succ
-- Module: Mathlib.Computability.PartrecCode
Goal:
⊢ Nat.Partrec left.eval

Tactic:
Nat.Partrec.left

Premises used: Nat.Partrec.left, Nat.Partrec.Code.eval
-- Module: Mathlib.Computability.PartrecCode
Goal:
⊢ Nat.Partrec left.eval

Tactic:
exact Nat.Partrec.left

Premises used: Nat.Partrec.left
-- Module: Mathlib.Computability.PartrecCode
Goal:
⊢ Nat.Partrec right.eval

Tactic:
Nat.Partrec.right

Premises used: Nat.Partrec.right, Nat.Partrec.Code.eval
-- Module: Mathlib.Computability.PartrecCode
Goal:
⊢ Nat.Partrec right.eval

Tactic:
exact Nat.Partrec.right

Premises used: Nat.Partrec.right
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
pf : Nat.Partrec cf.eval
pg : Nat.Partrec cg.eval
⊢ Nat.Partrec (cf.pair cg).eval

Tactic:
pf.pair pg

Premises used: Nat.Partrec.pair, Nat.Partrec.Code.eval
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
pf : Nat.Partrec cf.eval
pg : Nat.Partrec cg.eval
⊢ Nat.Partrec (cf.pair cg).eval

Tactic:
exact pf.pair pg

Premises used: Nat.Partrec.pair
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
pf : Nat.Partrec cf.eval
pg : Nat.Partrec cg.eval
⊢ Nat.Partrec (cf.comp cg).eval

Tactic:
pf.comp pg

Premises used: Nat.Partrec.comp, Nat.Partrec.Code.eval
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
pf : Nat.Partrec cf.eval
pg : Nat.Partrec cg.eval
⊢ Nat.Partrec (cf.comp cg).eval

Tactic:
exact pf.comp pg

Premises used: Nat.Partrec.comp
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
pf : Nat.Partrec cf.eval
pg : Nat.Partrec cg.eval
⊢ Nat.Partrec (cf.prec cg).eval

Tactic:
pf.prec pg

Premises used: Nat.Partrec.prec, Nat.Partrec.Code.eval
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
pf : Nat.Partrec cf.eval
pg : Nat.Partrec cg.eval
⊢ Nat.Partrec (cf.prec cg).eval

Tactic:
exact pf.prec pg

Premises used: Nat.Partrec.prec
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf : Code
pf : Nat.Partrec cf.eval
⊢ Nat.Partrec cf.rfind'.eval

Tactic:
pf.rfind'

Premises used: Nat.Partrec.rfind', Nat.Partrec.Code.eval
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf : Code
pf : Nat.Partrec cf.eval
⊢ Nat.Partrec cf.rfind'.eval

Tactic:
exact pf.rfind'

Premises used: Nat.Partrec.rfind'
-- Module: Mathlib.Computability.PartrecCode
Goal:
c : Code
refine_2 : Nat.Partrec zero.eval
refine_2₁ : Nat.Partrec succ.eval
refine_2₂ : Nat.Partrec left.eval
refine_2₃ : Nat.Partrec right.eval
refine_2₄ : ∀ (cf cg : Code) (pf : Nat.Partrec cf.eval) (pg : Nat.Partrec cg.eval), Nat.Partrec (cf.pair cg).eval
refine_2₅ : ∀ (cf cg : Code) (pf : Nat.Partrec cf.eval) (pg : Nat.Partrec cg.eval), Nat.Partrec (cf.comp cg).eval
refine_2₆ : ∀ (cf cg : Code) (pf : Nat.Partrec cf.eval) (pg : Nat.Partrec cg.eval), Nat.Partrec (cf.prec cg).eval
refine_2₇ : ∀ (cf : Code) (pf : Nat.Partrec cf.eval), Nat.Partrec cf.rfind'.eval
⊢ Nat.Partrec c.eval

Tactic:
induction c with
    | zero => exact Nat.Partrec.zero
    | succ => exact Nat.Partrec.succ
    | left => exact Nat.Partrec.left
    | right => exact Nat.Partrec.right
    | pair cf cg pf pg => exact pf.pair pg
    | comp cf cg pf pg => exact pf.comp pg
    | prec cf cg pf pg => exact pf.prec pg
    | rfind' cf pf => exact pf.rfind'

Premises used: Nat.Partrec.Code.rfind', Nat.Partrec.Code.right, Nat.Partrec.zero, Nat.Partrec.right, Nat.Partrec.Code.prec, Nat.Partrec.Code.succ, Nat.Partrec.Code.left, Nat.Partrec.Code.comp, Nat.Partrec.succ, Nat.Partrec.left, Nat.Partrec.Code.zero, Nat.Partrec.Code.pair
-- Module: Mathlib.Computability.PartrecCode
Goal:
c : Code
n x : ℕ
h : x ∈ evaln 0 c n
⊢ n < 0

Tactic:
simp [evaln] at h

Premises used: Nat.Partrec.Code.evaln
-- Module: Mathlib.Computability.PartrecCode
Goal:
k : ℕ
c : Code
n x : ℕ
h : x ∈ evaln (k + 1) c n
this :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
zero : ∀ (h : x ∈ evaln (k + 1) Code.zero n), n < k + 1
succ : ∀ (h : x ∈ evaln (k + 1) Code.succ n), n < k + 1
left : ∀ (h : x ∈ evaln (k + 1) Code.left n), n < k + 1
right : ∀ (h : x ∈ evaln (k + 1) Code.right n), n < k + 1
pair : ∀ (a a_1 : Code) (h : x ∈ evaln (k + 1) (a.pair a_1) n), n < k + 1
comp : ∀ (a a_1 : Code) (h : x ∈ evaln (k + 1) (a.comp a_1) n), n < k + 1
prec : ∀ (a a_1 : Code) (h : x ∈ evaln (k + 1) (a.prec a_1) n), n < k + 1
rfind' : ∀ (a : Code) (h : x ∈ evaln (k + 1) a.rfind' n), n < k + 1
⊢ n < k + 1

Tactic:
cases c
-- Module: Mathlib.Computability.PartrecCode
Goal:
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
h : x ∈ evaln (k + 1) zero n
⊢ Membership.mem (γ := Option ℕ)
    ((fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          pure 0 : Option ℕ))
      n)
    x

Tactic:
rw [evaln] at h

Premises used: Nat.Partrec.Code.evaln
-- Module: Mathlib.Computability.PartrecCode
Goal:
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
h : x ∈ evaln (k + 1) succ n
⊢ Membership.mem (γ := Option ℕ)
    ((fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          pure n.succ : Option ℕ))
      n)
    x

Tactic:
rw [evaln] at h

Premises used: Nat.Partrec.Code.evaln
-- Module: Mathlib.Computability.PartrecCode
Goal:
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
h : x ∈ evaln (k + 1) left n
⊢ Membership.mem (γ := Option ℕ)
    ((fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          pure (unpair n).1 : Option ℕ))
      n)
    x

Tactic:
rw [evaln] at h

Premises used: Nat.Partrec.Code.evaln
-- Module: Mathlib.Computability.PartrecCode
Goal:
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
h : x ∈ evaln (k + 1) right n
⊢ Membership.mem (γ := Option ℕ)
    ((fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          pure (unpair n).2 : Option ℕ))
      n)
    x

Tactic:
rw [evaln] at h

Premises used: Nat.Partrec.Code.evaln
-- Module: Mathlib.Computability.PartrecCode
Goal:
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
a a_1 : Code
h : x ∈ evaln (k + 1) (a.pair a_1) n
⊢ Membership.mem (γ := Option ℕ)
    ((fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          Nat.pair <$> evaln (k + 1) a n <*> evaln (k + 1) a_1 n : Option ℕ))
      n)
    x

Tactic:
rw [evaln] at h

Premises used: Nat.Partrec.Code.evaln
-- Module: Mathlib.Computability.PartrecCode
Goal:
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
a a_1 : Code
h : x ∈ evaln (k + 1) (a.comp a_1) n
⊢ Membership.mem (γ := Option ℕ)
    ((fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          let x ← evaln (k + 1) a_1 n
          evaln (k + 1) a x : Option ℕ))
      n)
    x

Tactic:
rw [evaln] at h

Premises used: Nat.Partrec.Code.evaln
-- Module: Mathlib.Computability.PartrecCode
Goal:
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
a a_1 : Code
h : x ∈ evaln (k + 1) (a.prec a_1) n
⊢ Membership.mem (γ := Option ℕ)
    ((fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          unpaired
              (fun (a_2 n : ℕ) ↦
                Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) n (evaln (k + 1) a a_2) fun (y : ℕ) ↦ do
                  let i ← evaln k (a.prec a_1) (Nat.pair a_2 y)
                  evaln (k + 1) a_1 (Nat.pair a_2 (Nat.pair y i)))
              n :
          Option ℕ))
      n)
    x

Tactic:
rw [evaln] at h

Premises used: Nat.Partrec.Code.evaln
-- Module: Mathlib.Computability.PartrecCode
Goal:
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
a : Code
h : x ∈ evaln (k + 1) a.rfind' n
⊢ Membership.mem (γ := Option ℕ)
    ((fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          unpaired
              (fun (a_1 m : ℕ) ↦ do
                let x ← evaln (k + 1) a (Nat.pair a_1 m)
                if x = 0 then pure m else evaln k a.rfind' (Nat.pair a_1 (m + 1)))
              n :
          Option ℕ))
      n)
    x

Tactic:
rw [evaln] at h

Premises used: Nat.Partrec.Code.evaln
-- Module: Mathlib.Computability.PartrecCode
Goal:
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
h :
  Membership.mem (γ := Option ℕ)
    ((fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          pure 0 : Option ℕ))
      n)
    x
⊢ n < k + 1

Tactic:
this h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
h :
  Membership.mem (γ := Option ℕ)
    ((fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          pure 0 : Option ℕ))
      n)
    x
⊢ n < k + 1

Tactic:
exact this h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
h :
  Membership.mem (γ := Option ℕ)
    ((fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          pure n.succ : Option ℕ))
      n)
    x
⊢ n < k + 1

Tactic:
this h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
h :
  Membership.mem (γ := Option ℕ)
    ((fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          pure n.succ : Option ℕ))
      n)
    x
⊢ n < k + 1

Tactic:
exact this h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
h :
  Membership.mem (γ := Option ℕ)
    ((fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          pure (unpair n).1 : Option ℕ))
      n)
    x
⊢ n < k + 1

Tactic:
this h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
h :
  Membership.mem (γ := Option ℕ)
    ((fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          pure (unpair n).1 : Option ℕ))
      n)
    x
⊢ n < k + 1

Tactic:
exact this h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
h :
  Membership.mem (γ := Option ℕ)
    ((fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          pure (unpair n).2 : Option ℕ))
      n)
    x
⊢ n < k + 1

Tactic:
this h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
h :
  Membership.mem (γ := Option ℕ)
    ((fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          pure (unpair n).2 : Option ℕ))
      n)
    x
⊢ n < k + 1

Tactic:
exact this h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
a a_1 : Code
h :
  Membership.mem (γ := Option ℕ)
    ((fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          Nat.pair <$> evaln (k + 1) a n <*> evaln (k + 1) a_1 n : Option ℕ))
      n)
    x
⊢ n < k + 1

Tactic:
this h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
a a_1 : Code
h :
  Membership.mem (γ := Option ℕ)
    ((fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          Nat.pair <$> evaln (k + 1) a n <*> evaln (k + 1) a_1 n : Option ℕ))
      n)
    x
⊢ n < k + 1

Tactic:
exact this h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
a a_1 : Code
h :
  Membership.mem (γ := Option ℕ)
    ((fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          let x ← evaln (k + 1) a_1 n
          evaln (k + 1) a x : Option ℕ))
      n)
    x
⊢ n < k + 1

Tactic:
this h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
a a_1 : Code
h :
  Membership.mem (γ := Option ℕ)
    ((fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          let x ← evaln (k + 1) a_1 n
          evaln (k + 1) a x : Option ℕ))
      n)
    x
⊢ n < k + 1

Tactic:
exact this h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
a a_1 : Code
h :
  Membership.mem (γ := Option ℕ)
    ((fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          unpaired
              (fun (a_2 n : ℕ) ↦
                Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) n (evaln (k + 1) a a_2) fun (y : ℕ) ↦ do
                  let i ← evaln k (a.prec a_1) (Nat.pair a_2 y)
                  evaln (k + 1) a_1 (Nat.pair a_2 (Nat.pair y i)))
              n :
          Option ℕ))
      n)
    x
⊢ n < k + 1

Tactic:
this h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
a a_1 : Code
h :
  Membership.mem (γ := Option ℕ)
    ((fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          unpaired
              (fun (a_2 n : ℕ) ↦
                Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) n (evaln (k + 1) a a_2) fun (y : ℕ) ↦ do
                  let i ← evaln k (a.prec a_1) (Nat.pair a_2 y)
                  evaln (k + 1) a_1 (Nat.pair a_2 (Nat.pair y i)))
              n :
          Option ℕ))
      n)
    x
⊢ n < k + 1

Tactic:
exact this h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
a : Code
h :
  Membership.mem (γ := Option ℕ)
    ((fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          unpaired
              (fun (a_1 m : ℕ) ↦ do
                let x ← evaln (k + 1) a (Nat.pair a_1 m)
                if x = 0 then pure m else evaln k a.rfind' (Nat.pair a_1 (m + 1)))
              n :
          Option ℕ))
      n)
    x
⊢ n < k + 1

Tactic:
this h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
a : Code
h :
  Membership.mem (γ := Option ℕ)
    ((fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          unpaired
              (fun (a_1 m : ℕ) ↦ do
                let x ← evaln (k + 1) a (Nat.pair a_1 m)
                if x = 0 then pure m else evaln k a.rfind' (Nat.pair a_1 (m + 1)))
              n :
          Option ℕ))
      n)
    x
⊢ n < k + 1

Tactic:
exact this h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k : ℕ
c : Code
n x : ℕ
h : x ∈ evaln (k + 1) c n
suffices :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
⊢ n < k + 1

Tactic:
suffices ∀ {o : Option ℕ}, x ∈ do { guard (n ≤ k); o } → n < k + 1 by
      cases c <;> rw [evaln] at h <;> exact this h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k : ℕ
c : Code
n x : ℕ
h : x ∈ evaln (k + 1) c n
⊢ ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1

Tactic:
simpa [Option.bind_eq_some_iff] using Nat.lt_succ_of_le

Premises used: Nat.lt_succ_of_le, Option.bind_eq_some_iff
-- Module: Mathlib.Computability.PartrecCode
Goal:
k₂ : ℕ
c : Code
n x : ℕ
h_1 : 0 ≤ k₂
h : x ∈ evaln 0 c n
⊢ x ∈ evaln k₂ c n

Tactic:
simp [evaln] at h

Premises used: Nat.Partrec.Code.evaln
-- Module: Mathlib.Computability.PartrecCode
Goal:
k k₂ : ℕ
c : Code
n x : ℕ
hl : k + 1 ≤ k₂ + 1
h : x ∈ evaln (k + 1) c n
⊢ k ≤ k₂

Tactic:
have hl' := Nat.le_of_succ_le_succ hl