awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.PartrecCode
Goal:
k : ℕ
cf : Code
hf : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cf n), x ∈ cf.eval n
n : ℕ
left : n ≤ k
m : ℕ
h₁ : evaln (k + 1) cf n = some m
m0 : ¬m = 0
y : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + ((unpair n).2 + 1)))
hy₂ : ∀ {m : ℕ}, m < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m + ((unpair n).2 + 1))), ¬a = 0
h₂ : evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)) = some (y + ((unpair n).2 + 1))
i : ℕ
im : i + 1 < y + 1
z : ℕ
hz : z ∈ cf.eval (Nat.pair (unpair n).1 (i + ((unpair n).2 + 1)))
z0 : ¬z = 0
⊢ z ∈ cf.eval (Nat.pair (unpair n).1 (i + 1 + (unpair n).2))

Tactic:
simpa [add_comm, add_left_comm] using hz

Premises used: add_left_comm, add_comm
-- Module: Mathlib.Computability.PartrecCode
Goal:
k : ℕ
cf : Code
hf : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cf n), x ∈ cf.eval n
n : ℕ
left : n ≤ k
m : ℕ
h₁ : evaln (k + 1) cf n = some m
m0 : ¬m = 0
y : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + ((unpair n).2 + 1)))
hy₂ : ∀ {m : ℕ}, m < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m + ((unpair n).2 + 1))), ¬a = 0
h₂ : evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)) = some (y + ((unpair n).2 + 1))
i : ℕ
im : i + 1 < y + 1
z : ℕ
hz : z ∈ cf.eval (Nat.pair (unpair n).1 (i + ((unpair n).2 + 1)))
z0 : ¬z = 0
⊢ ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (i + 1 + (unpair n).2)), ¬a = 0

Tactic:
exact ⟨z, by simpa [add_comm, add_left_comm] using hz, z0⟩
-- Module: Mathlib.Computability.PartrecCode
Goal:
c : Code
n x : ℕ
⊢ x ∈ c.eval n ↔ ∃ (k : ℕ), x ∈ evaln k c n

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

Premises used: Membership.mem, _private.0.Nat.Partrec.Code.evaln_complete.match_1, Iff.intro, Nat.Partrec.Code.eval, Nat.Partrec.Code.evaln_sound
-- Module: Mathlib.Computability.PartrecCode
Goal:
c : Code
n x : ℕ
refine : ∀ (h : x ∈ c.eval n), ∃ (k : ℕ), x ∈ evaln k c n
⊢ x ∈ c.eval n ↔ ∃ (k : ℕ), x ∈ evaln k c n

Tactic:
refine ⟨fun h => ?_, fun ⟨k, h⟩ => evaln_sound h⟩
-- Module: Mathlib.Computability.PartrecCode
Goal:
c : Code
n x : ℕ
h : x ∈ c.eval n
rsuffices : ∀ (k : ℕ) (h : x ∈ evaln (k + 1) c n), ∃ (k : ℕ), x ∈ evaln k c n
rsuffices₁ : ∃ (k : ℕ), x ∈ evaln (k + 1) c n
⊢ ∃ (k : ℕ), x ∈ evaln k c n

Tactic:
rsuffices ⟨k, h⟩ : ∃ k, x ∈ evaln (k + 1) c n
-- Module: Mathlib.Computability.PartrecCode
Goal:
c : Code
n x : ℕ
h_1 : x ∈ c.eval n
k : ℕ
h : x ∈ evaln (k + 1) c n
⊢ ∃ (k : ℕ), x ∈ evaln k c n

Tactic:
⟨k + 1, h⟩

Premises used: HAdd.hAdd, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Computability.PartrecCode
Goal:
c : Code
n x : ℕ
h_1 : x ∈ c.eval n
k : ℕ
h : x ∈ evaln (k + 1) c n
⊢ ∃ (k : ℕ), x ∈ evaln k c n

Tactic:
exact ⟨k + 1, h⟩
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ} (h : x ∈ cg.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cg n
n x : ℕ
h : x ∈ (cf.pair cg).eval n
pair :
  ∀ (h : ∃ a ∈ cf.eval n, ∃ a_1 ∈ cg.eval n, Nat.pair a a_1 = x),
    ∃ (k : ℕ),
      n ≤ k ∧ ∃ (a : ℕ), evaln (k + 1) cf n = some a ∧ ∃ (a_1 : ℕ), evaln (k + 1) cg n = some a_1 ∧ Nat.pair a a_1 = x
⊢ ∃ (k : ℕ), x ∈ evaln (k + 1) (cf.pair cg) n

Tactic:
simp [eval, evaln, pure, PFun.pure, Seq.seq, Option.bind_eq_some_iff] at h ⊢

Premises used: Pure.pure, Nat.Partrec.Code.evaln, Seq.seq, PFun.pure, Nat.Partrec.Code.eval, Option.bind_eq_some_iff
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ} (h : x ∈ cg.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cg n
n x : ℕ
h : ∃ a ∈ cf.eval n, ∃ a_1 ∈ cg.eval n, Nat.pair a a_1 = x
pair :
  ∀ (x : ℕ) (hx : x ∈ cf.eval n) (y : ℕ) (hy : y ∈ cg.eval n),
    ∃ (k : ℕ),
      n ≤ k ∧
        ∃ (a : ℕ),
          evaln (k + 1) cf n = some a ∧ ∃ (a_1 : ℕ), evaln (k + 1) cg n = some a_1 ∧ Nat.pair a a_1 = Nat.pair x y
⊢ ∃ (k : ℕ),
    n ≤ k ∧ ∃ (a : ℕ), evaln (k + 1) cf n = some a ∧ ∃ (a_1 : ℕ), evaln (k + 1) cg n = some a_1 ∧ Nat.pair a a_1 = x

Tactic:
rcases h with ⟨x, hx, y, hy, rfl⟩

Premises used: rfl
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ} (h : x ∈ cg.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cg n
n x : ℕ
hx : x ∈ cf.eval n
y : ℕ
hy : y ∈ cg.eval n
pair :
  ∀ (k₁ : ℕ) (hk₁ : x ∈ evaln (k₁ + 1) cf n),
    ∃ (k : ℕ),
      n ≤ k ∧
        ∃ (a : ℕ),
          evaln (k + 1) cf n = some a ∧ ∃ (a_1 : ℕ), evaln (k + 1) cg n = some a_1 ∧ Nat.pair a a_1 = Nat.pair x y
⊢ ∃ (k : ℕ),
    n ≤ k ∧
      ∃ (a : ℕ),
        evaln (k + 1) cf n = some a ∧ ∃ (a_1 : ℕ), evaln (k + 1) cg n = some a_1 ∧ Nat.pair a a_1 = Nat.pair x y

Tactic:
rcases hf hx with ⟨k₁, hk₁⟩
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ} (h : x ∈ cg.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cg n
n x : ℕ
hx : x ∈ cf.eval n
y : ℕ
hy : y ∈ cg.eval n
k₁ : ℕ
hk₁ : x ∈ evaln (k₁ + 1) cf n
pair :
  ∀ (k₂ : ℕ) (hk₂ : y ∈ evaln (k₂ + 1) cg n),
    ∃ (k : ℕ),
      n ≤ k ∧
        ∃ (a : ℕ),
          evaln (k + 1) cf n = some a ∧ ∃ (a_1 : ℕ), evaln (k + 1) cg n = some a_1 ∧ Nat.pair a a_1 = Nat.pair x y
⊢ ∃ (k : ℕ),
    n ≤ k ∧
      ∃ (a : ℕ),
        evaln (k + 1) cf n = some a ∧ ∃ (a_1 : ℕ), evaln (k + 1) cg n = some a_1 ∧ Nat.pair a a_1 = Nat.pair x y

Tactic:
rcases hg hy with ⟨k₂, hk₂⟩
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ} (h : x ∈ cg.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cg n
n x : ℕ
hx : x ∈ cf.eval n
y : ℕ
hy : y ∈ cg.eval n
k₁ : ℕ
hk₁ : x ∈ evaln (k₁ + 1) cf n
k₂ : ℕ
hk₂ : y ∈ evaln (k₂ + 1) cg n
⊢ ∃ (k : ℕ),
    n ≤ k ∧
      ∃ (a : ℕ),
        evaln (k + 1) cf n = some a ∧ ∃ (a_1 : ℕ), evaln (k + 1) cg n = some a_1 ∧ Nat.pair a a_1 = Nat.pair x y

Tactic:
⟨max k₁ k₂, ?_⟩

Premises used: Max.max, Exists.intro
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ} (h : x ∈ cg.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cg n
n x : ℕ
hx : x ∈ cf.eval n
y : ℕ
hy : y ∈ cg.eval n
k₁ : ℕ
hk₁ : x ∈ evaln (k₁ + 1) cf n
k₂ : ℕ
hk₂ : y ∈ evaln (k₂ + 1) cg n
pair :
  n ≤ max k₁ k₂ ∧
    ∃ (a : ℕ),
      evaln (max k₁ k₂ + 1) cf n = some a ∧
        ∃ (a_1 : ℕ), evaln (max k₁ k₂ + 1) cg n = some a_1 ∧ Nat.pair a a_1 = Nat.pair x y
⊢ ∃ (k : ℕ),
    n ≤ k ∧
      ∃ (a : ℕ),
        evaln (k + 1) cf n = some a ∧ ∃ (a_1 : ℕ), evaln (k + 1) cg n = some a_1 ∧ Nat.pair a a_1 = Nat.pair x y

Tactic:
refine ⟨max k₁ k₂, ?_⟩
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ} (h : x ∈ cg.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cg n
n x : ℕ
hx : x ∈ cf.eval n
y : ℕ
hy : y ∈ cg.eval n
k₁ : ℕ
hk₁ : x ∈ evaln (k₁ + 1) cf n
k₂ : ℕ
hk₂ : y ∈ evaln (k₂ + 1) cg n
⊢ n ≤ max k₁ k₂ ∧
    ∃ (a : ℕ),
      evaln (max k₁ k₂ + 1) cf n = some a ∧
        ∃ (a_1 : ℕ), evaln (max k₁ k₂ + 1) cg n = some a_1 ∧ Nat.pair a a_1 = Nat.pair x y

Tactic:
⟨le_max_of_le_left <| Nat.le_of_lt_succ <| evaln_bound hk₁, _,
        evaln_mono (Nat.succ_le_succ <| le_max_left _ _) hk₁, _,
        evaln_mono (Nat.succ_le_succ <| le_max_right _ _) hk₂, rfl⟩

Premises used: le_max_right, Nat.Partrec.Code.evaln_bound, Nat.le_of_lt_succ, And.intro, le_max_of_le_left, Exists.intro, le_max_left, Nat.Partrec.Code.evaln_mono, rfl, Nat.succ_le_succ
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ} (h : x ∈ cg.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cg n
n x : ℕ
hx : x ∈ cf.eval n
y : ℕ
hy : y ∈ cg.eval n
k₁ : ℕ
hk₁ : x ∈ evaln (k₁ + 1) cf n
k₂ : ℕ
hk₂ : y ∈ evaln (k₂ + 1) cg n
⊢ n ≤ max k₁ k₂ ∧
    ∃ (a : ℕ),
      evaln (max k₁ k₂ + 1) cf n = some a ∧
        ∃ (a_1 : ℕ), evaln (max k₁ k₂ + 1) cg n = some a_1 ∧ Nat.pair a a_1 = Nat.pair x y

Tactic:
refine
      ⟨le_max_of_le_left <| Nat.le_of_lt_succ <| evaln_bound hk₁, _,
        evaln_mono (Nat.succ_le_succ <| le_max_left _ _) hk₁, _,
        evaln_mono (Nat.succ_le_succ <| le_max_right _ _) hk₂, rfl⟩
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ} (h : x ∈ cg.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cg n
n x : ℕ
h : x ∈ (cf.comp cg).eval n
comp :
  ∀ (h : ∃ a ∈ cg.eval n, x ∈ cf.eval a),
    ∃ (k : ℕ), n ≤ k ∧ ∃ (a : ℕ), evaln (k + 1) cg n = some a ∧ evaln (k + 1) cf a = some x
⊢ ∃ (k : ℕ), x ∈ evaln (k + 1) (cf.comp cg) n

Tactic:
simp [eval, evaln, pure, PFun.pure, Seq.seq, Option.bind_eq_some_iff] at h ⊢

Premises used: Pure.pure, Nat.Partrec.Code.evaln, Seq.seq, PFun.pure, Nat.Partrec.Code.eval, Option.bind_eq_some_iff
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ} (h : x ∈ cg.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cg n
n x : ℕ
h : ∃ a ∈ cg.eval n, x ∈ cf.eval a
comp :
  ∀ (y : ℕ) (hy : y ∈ cg.eval n) (hx : x ∈ cf.eval y),
    ∃ (k : ℕ), n ≤ k ∧ ∃ (a : ℕ), evaln (k + 1) cg n = some a ∧ evaln (k + 1) cf a = some x
⊢ ∃ (k : ℕ), n ≤ k ∧ ∃ (a : ℕ), evaln (k + 1) cg n = some a ∧ evaln (k + 1) cf a = some x

Tactic:
rcases h with ⟨y, hy, hx⟩
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ} (h : x ∈ cg.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cg n
n x y : ℕ
hy : y ∈ cg.eval n
hx : x ∈ cf.eval y
comp :
  ∀ (k₁ : ℕ) (hk₁ : y ∈ evaln (k₁ + 1) cg n),
    ∃ (k : ℕ), n ≤ k ∧ ∃ (a : ℕ), evaln (k + 1) cg n = some a ∧ evaln (k + 1) cf a = some x
⊢ ∃ (k : ℕ), n ≤ k ∧ ∃ (a : ℕ), evaln (k + 1) cg n = some a ∧ evaln (k + 1) cf a = some x

Tactic:
rcases hg hy with ⟨k₁, hk₁⟩
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ} (h : x ∈ cg.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cg n
n x y : ℕ
hy : y ∈ cg.eval n
hx : x ∈ cf.eval y
k₁ : ℕ
hk₁ : y ∈ evaln (k₁ + 1) cg n
comp :
  ∀ (k₂ : ℕ) (hk₂ : x ∈ evaln (k₂ + 1) cf y),
    ∃ (k : ℕ), n ≤ k ∧ ∃ (a : ℕ), evaln (k + 1) cg n = some a ∧ evaln (k + 1) cf a = some x
⊢ ∃ (k : ℕ), n ≤ k ∧ ∃ (a : ℕ), evaln (k + 1) cg n = some a ∧ evaln (k + 1) cf a = some x

Tactic:
rcases hf hx with ⟨k₂, hk₂⟩
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ} (h : x ∈ cg.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cg n
n x y : ℕ
hy : y ∈ cg.eval n
hx : x ∈ cf.eval y
k₁ : ℕ
hk₁ : y ∈ evaln (k₁ + 1) cg n
k₂ : ℕ
hk₂ : x ∈ evaln (k₂ + 1) cf y
⊢ ∃ (k : ℕ), n ≤ k ∧ ∃ (a : ℕ), evaln (k + 1) cg n = some a ∧ evaln (k + 1) cf a = some x

Tactic:
⟨max k₁ k₂, ?_⟩

Premises used: Max.max, Exists.intro
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ} (h : x ∈ cg.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cg n
n x y : ℕ
hy : y ∈ cg.eval n
hx : x ∈ cf.eval y
k₁ : ℕ
hk₁ : y ∈ evaln (k₁ + 1) cg n
k₂ : ℕ
hk₂ : x ∈ evaln (k₂ + 1) cf y
comp : n ≤ max k₁ k₂ ∧ ∃ (a : ℕ), evaln (max k₁ k₂ + 1) cg n = some a ∧ evaln (max k₁ k₂ + 1) cf a = some x
⊢ ∃ (k : ℕ), n ≤ k ∧ ∃ (a : ℕ), evaln (k + 1) cg n = some a ∧ evaln (k + 1) cf a = some x

Tactic:
refine ⟨max k₁ k₂, ?_⟩
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ} (h : x ∈ cg.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cg n
n x y : ℕ
hy : y ∈ cg.eval n
hx : x ∈ cf.eval y
k₁ : ℕ
hk₁ : y ∈ evaln (k₁ + 1) cg n
k₂ : ℕ
hk₂ : x ∈ evaln (k₂ + 1) cf y
⊢ n ≤ max k₁ k₂ ∧ ∃ (a : ℕ), evaln (max k₁ k₂ + 1) cg n = some a ∧ evaln (max k₁ k₂ + 1) cf a = some x

Tactic:
⟨le_max_of_le_left <| Nat.le_of_lt_succ <| evaln_bound hk₁, _,
        evaln_mono (Nat.succ_le_succ <| le_max_left _ _) hk₁,
        evaln_mono (Nat.succ_le_succ <| le_max_right _ _) hk₂⟩

Premises used: le_max_right, Nat.Partrec.Code.evaln_bound, Nat.le_of_lt_succ, And.intro, le_max_of_le_left, Exists.intro, le_max_left, Nat.Partrec.Code.evaln_mono, Nat.succ_le_succ
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ} (h : x ∈ cg.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cg n
n x y : ℕ
hy : y ∈ cg.eval n
hx : x ∈ cf.eval y
k₁ : ℕ
hk₁ : y ∈ evaln (k₁ + 1) cg n
k₂ : ℕ
hk₂ : x ∈ evaln (k₂ + 1) cf y
⊢ n ≤ max k₁ k₂ ∧ ∃ (a : ℕ), evaln (max k₁ k₂ + 1) cg n = some a ∧ evaln (max k₁ k₂ + 1) cf a = some x

Tactic:
exact
      ⟨le_max_of_le_left <| Nat.le_of_lt_succ <| evaln_bound hk₁, _,
        evaln_mono (Nat.succ_le_succ <| le_max_left _ _) hk₁,
        evaln_mono (Nat.succ_le_succ <| le_max_right _ _) hk₂⟩
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ} (h : x ∈ cg.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cg n
n x : ℕ
h : x ∈ (cf.prec cg).eval n
prec :
  ∃ (k : ℕ),
    n ≤ k ∧
      Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) cf (unpair n).1)
          (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
            (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun (i : ℕ) ↦
              evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
          (unpair n).2 =
        some x
⊢ ∃ (k : ℕ), x ∈ evaln (k + 1) (cf.prec cg) n

Tactic:
simp [eval, evaln, pure, PFun.pure, Seq.seq, Option.bind_eq_some_iff] at h ⊢

Premises used: Pure.pure, Nat.Partrec.Code.evaln, Seq.seq, PFun.pure, Nat.Partrec.Code.eval, Option.bind_eq_some_iff
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ} (h : x ∈ cg.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cg n
n x : ℕ
h :
  Membership.mem (γ := Part ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval (unpair n).1)
        (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ cg.eval (Nat.pair (unpair n).1 (Nat.pair y i)))
        (unpair n).2 :
      Part ℕ)
    x
prec :
  ∀
    (h :
      Membership.mem (γ := Part ℕ)
        (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval (unpair n).1)
            (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ cg.eval (Nat.pair (unpair n).1 (Nat.pair y i)))
            (unpair n).2 :
          Part ℕ)
        x),
    ∃ (k : ℕ),
      n ≤ k ∧
        Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) cf (unpair n).1)
            (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
              (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun (i : ℕ) ↦
                evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
            (unpair n).2 =
          some x
⊢ ∃ (k : ℕ),
    n ≤ k ∧
      Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) cf (unpair n).1)
          (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
            (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun (i : ℕ) ↦
              evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
          (unpair n).2 =
        some x

Tactic:
revert h
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ} (h : x ∈ cg.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cg n
n x : ℕ
prec :
  ∀ (n₁ : ℕ)
    (h :
      Membership.mem (γ := Part ℕ)
        (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval n₁)
            (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ cg.eval (Nat.pair n₁ (Nat.pair y i))) (unpair n).2 :
          Part ℕ)
        x),
    ∃ (k : ℕ),
      n ≤ k ∧
        Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) cf n₁)
            (fun (n : ℕ) (n_ih : Option ℕ) ↦
              (evaln k (cf.prec cg) (Nat.pair n₁ n)).bind fun (i : ℕ) ↦ evaln (k + 1) cg (Nat.pair n₁ (Nat.pair n i)))
            (unpair n).2 =
          some x
⊢ ∀
    (h :
      Membership.mem (γ := Part ℕ)
        (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval (unpair n).1)
            (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ cg.eval (Nat.pair (unpair n).1 (Nat.pair y i)))
            (unpair n).2 :
          Part ℕ)
        x),
    ∃ (k : ℕ),
      n ≤ k ∧
        Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) cf (unpair n).1)
            (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
              (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun (i : ℕ) ↦
                evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
            (unpair n).2 =
          some x

Tactic:
generalize n.unpair.1 = n₁

Premises used: Nat.unpair, Prod.fst
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ} (h : x ∈ cg.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cg n
n x n₁ : ℕ
prec :
  ∀ (n₂ : ℕ)
    (h :
      Membership.mem (γ := Part ℕ)
        (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval n₁)
            (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ cg.eval (Nat.pair n₁ (Nat.pair y i))) n₂ :
          Part ℕ)
        x),
    ∃ (k : ℕ),
      n ≤ k ∧
        Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) cf n₁)
            (fun (n : ℕ) (n_ih : Option ℕ) ↦
              (evaln k (cf.prec cg) (Nat.pair n₁ n)).bind fun (i : ℕ) ↦ evaln (k + 1) cg (Nat.pair n₁ (Nat.pair n i)))
            n₂ =
          some x
⊢ ∀
    (h :
      Membership.mem (γ := Part ℕ)
        (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval n₁)
            (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ cg.eval (Nat.pair n₁ (Nat.pair y i))) (unpair n).2 :
          Part ℕ)
        x),
    ∃ (k : ℕ),
      n ≤ k ∧
        Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) cf n₁)
            (fun (n : ℕ) (n_ih : Option ℕ) ↦
              (evaln k (cf.prec cg) (Nat.pair n₁ n)).bind fun (i : ℕ) ↦ evaln (k + 1) cg (Nat.pair n₁ (Nat.pair n i)))
            (unpair n).2 =
          some x

Tactic:
generalize n.unpair.2 = n₂

Premises used: Nat.unpair, Prod.snd
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ} (h : x ∈ cg.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cg n
n₁ n x : ℕ
h : x ∈ cf.eval n₁
prec : ∀ (k : ℕ) (hk : x ∈ evaln (k + 1) cf n₁), ∃ (k : ℕ), n ≤ k ∧ evaln (k + 1) cf n₁ = some x
⊢ ∃ (k : ℕ), n ≤ k ∧ evaln (k + 1) cf n₁ = some x

Tactic:
rcases hf h with ⟨k, hk⟩
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ} (h : x ∈ cg.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cg n
n₁ n x : ℕ
h : x ∈ cf.eval n₁
k : ℕ
hk : x ∈ evaln (k + 1) cf n₁
⊢ ∃ (k : ℕ), n ≤ k ∧ evaln (k + 1) cf n₁ = some x

Tactic:
⟨_, le_max_left _ _, evaln_mono (Nat.succ_le_succ <| le_max_right _ _) hk⟩

Premises used: le_max_right, And.intro, Exists.intro, le_max_left, Nat.Partrec.Code.evaln_mono, Nat.succ_le_succ
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ} (h : x ∈ cg.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cg n
n₁ n x : ℕ
h : x ∈ cf.eval n₁
k : ℕ
hk : x ∈ evaln (k + 1) cf n₁
⊢ ∃ (k : ℕ), n ≤ k ∧ evaln (k + 1) cf n₁ = some x

Tactic:
exact ⟨_, le_max_left _ _, evaln_mono (Nat.succ_le_succ <| le_max_right _ _) hk⟩
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ} (h : x ∈ cg.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cg n
n₁ m : ℕ
IH :
  ∀ {n x : ℕ}
    (h :
      Membership.mem (γ := Part ℕ)
        (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval n₁)
            (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ cg.eval (Nat.pair n₁ (Nat.pair y i))) m :
          Part ℕ)
        x),
    ∃ (k : ℕ),
      n ≤ k ∧
        Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) cf n₁)
            (fun (n : ℕ) (n_ih : Option ℕ) ↦
              (evaln k (cf.prec cg) (Nat.pair n₁ n)).bind fun (i : ℕ) ↦ evaln (k + 1) cg (Nat.pair n₁ (Nat.pair n i)))
            m =
          some x
n x : ℕ
prec :
  ∀ (x_1 : ℕ),
    Membership.mem (γ := Part ℕ)
        (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval n₁)
            (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ cg.eval (Nat.pair n₁ (Nat.pair y i))) m :
          Part ℕ)
        x_1 →
      x ∈ cg.eval (Nat.pair n₁ (Nat.pair m x_1)) →
        ∃ (k : ℕ),
          n ≤ k ∧
            ∃ (a : ℕ),
              evaln k (cf.prec cg) (Nat.pair n₁ m) = some a ∧ evaln (k + 1) cg (Nat.pair n₁ (Nat.pair m a)) = some x
⊢ ∀
    (h :
      Membership.mem (γ := Part ℕ)
        (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval n₁)
            (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ cg.eval (Nat.pair n₁ (Nat.pair y i))) (m + 1) :
          Part ℕ)
        x),
    ∃ (k : ℕ),
      n ≤ k ∧
        Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) cf n₁)
            (fun (n : ℕ) (n_ih : Option ℕ) ↦
              (evaln k (cf.prec cg) (Nat.pair n₁ n)).bind fun (i : ℕ) ↦ evaln (k + 1) cg (Nat.pair n₁ (Nat.pair n i)))
            (m + 1) =
          some x

Tactic:
simp [Option.bind_eq_some_iff]

Premises used: Option.bind_eq_some_iff
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ} (h : x ∈ cg.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cg n
n₁ m : ℕ
IH :
  ∀ {n x : ℕ}
    (h :
      Membership.mem (γ := Part ℕ)
        (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval n₁)
            (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ cg.eval (Nat.pair n₁ (Nat.pair y i))) m :
          Part ℕ)
        x),
    ∃ (k : ℕ),
      n ≤ k ∧
        Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) cf n₁)
            (fun (n : ℕ) (n_ih : Option ℕ) ↦
              (evaln k (cf.prec cg) (Nat.pair n₁ n)).bind fun (i : ℕ) ↦ evaln (k + 1) cg (Nat.pair n₁ (Nat.pair n i)))
            m =
          some x
n x y : ℕ
hy :
  Membership.mem (γ := Part ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval n₁)
        (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ cg.eval (Nat.pair n₁ (Nat.pair y i))) m :
      Part ℕ)
    y
hx : x ∈ cg.eval (Nat.pair n₁ (Nat.pair m y))
prec :
  ∀ (k₁ : ℕ) (nk₁ : max n (Nat.pair n₁ m) ≤ k₁)
    (hk₁ :
      Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k₁ + 1) cf n₁)
          (fun (n : ℕ) (n_ih : Option ℕ) ↦
            (evaln k₁ (cf.prec cg) (Nat.pair n₁ n)).bind fun (i : ℕ) ↦ evaln (k₁ + 1) cg (Nat.pair n₁ (Nat.pair n i)))
          m =
        some y),
    ∃ (k : ℕ),
      n ≤ k ∧
        ∃ (a : ℕ),
          evaln k (cf.prec cg) (Nat.pair n₁ m) = some a ∧ evaln (k + 1) cg (Nat.pair n₁ (Nat.pair m a)) = some x
⊢ ∃ (k : ℕ),
    n ≤ k ∧
      ∃ (a : ℕ), evaln k (cf.prec cg) (Nat.pair n₁ m) = some a ∧ evaln (k + 1) cg (Nat.pair n₁ (Nat.pair m a)) = some x

Tactic:
rcases IH hy with ⟨k₁, nk₁, hk₁⟩