awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.PartrecCode
Goal:
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        Membership.mem (γ := Option ℕ)
            (do
              guard (n ≤ k)
              o₁)
            x →
          Membership.mem (γ := Option ℕ)
            (do
              guard (n ≤ k₂)
              o₂)
            x
cf : Code
hf : ∀ (n x : ℕ) (h : evaln (k + 1) cf n = some x), evaln (k₂ + 1) cf n = some x
n x_1 : ℕ
h_1 :
  (fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          unpaired
              (fun (a m : ℕ) ↦ do
                let x ← evaln (k + 1) cf (Nat.pair a m)
                if x = 0 then pure m else evaln k cf.rfind' (Nat.pair a (m + 1)))
              n :
          Option ℕ))
      n =
    some x_1
h :
  ∃ (a : ℕ),
    evaln (k + 1) cf n = some a ∧
      (if a = 0 then some (unpair n).2 else evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x_1
x : ℕ
x0 : ¬x = 0
neg :
  evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)) = some x_1 →
    evaln k₂ cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)) = some x_1
⊢ (if x = 0 then some (unpair n).2 else evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x_1 →
    (if x = 0 then some (unpair n).2 else evaln k₂ cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x_1

Tactic:
simp [x0]
-- Module: Mathlib.Computability.PartrecCode
Goal:
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        Membership.mem (γ := Option ℕ)
            (do
              guard (n ≤ k)
              o₁)
            x →
          Membership.mem (γ := Option ℕ)
            (do
              guard (n ≤ k₂)
              o₂)
            x
cf : Code
hf : ∀ (n x : ℕ) (h : evaln (k + 1) cf n = some x), evaln (k₂ + 1) cf n = some x
n x_1 : ℕ
h_1 :
  (fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          unpaired
              (fun (a m : ℕ) ↦ do
                let x ← evaln (k + 1) cf (Nat.pair a m)
                if x = 0 then pure m else evaln k cf.rfind' (Nat.pair a (m + 1)))
              n :
          Option ℕ))
      n =
    some x_1
h :
  ∃ (a : ℕ),
    evaln (k + 1) cf n = some a ∧
      (if a = 0 then some (unpair n).2 else evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x_1
x : ℕ
x0 : ¬x = 0
⊢ evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)) = some x_1 →
    evaln k₂ cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)) = some x_1

Tactic:
evaln_mono hl'
-- Module: Mathlib.Computability.PartrecCode
Goal:
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        Membership.mem (γ := Option ℕ)
            (do
              guard (n ≤ k)
              o₁)
            x →
          Membership.mem (γ := Option ℕ)
            (do
              guard (n ≤ k₂)
              o₂)
            x
cf : Code
hf : ∀ (n x : ℕ) (h : evaln (k + 1) cf n = some x), evaln (k₂ + 1) cf n = some x
n x_1 : ℕ
h_1 :
  (fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          unpaired
              (fun (a m : ℕ) ↦ do
                let x ← evaln (k + 1) cf (Nat.pair a m)
                if x = 0 then pure m else evaln k cf.rfind' (Nat.pair a (m + 1)))
              n :
          Option ℕ))
      n =
    some x_1
h :
  ∃ (a : ℕ),
    evaln (k + 1) cf n = some a ∧
      (if a = 0 then some (unpair n).2 else evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x_1
x : ℕ
x0 : ¬x = 0
⊢ evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)) = some x_1 →
    evaln k₂ cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)) = some x_1

Tactic:
exact evaln_mono hl'
-- Module: Mathlib.Computability.PartrecCode
Goal:
x_1 : Code
n x : ℕ
h : x ∈ evaln 0 x_1 n
⊢ x ∈ x_1.eval n

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
zero : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) Code.zero n), x ∈ Code.zero.eval n
succ : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) Code.succ n), x ∈ Code.succ.eval n
left : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) Code.left n), x ∈ Code.left.eval n
right : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) Code.right n), x ∈ Code.right.eval n
pair :
  ∀ (a a_1 : Code),
    (∀ (n x : ℕ) (h : x ∈ evaln (k + 1) a n), x ∈ a.eval n) →
      (∀ (n x : ℕ) (h : x ∈ evaln (k + 1) a_1 n), x ∈ a_1.eval n) →
        ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) (a.pair a_1) n), x ∈ (a.pair a_1).eval n
comp :
  ∀ (a a_1 : Code),
    (∀ (n x : ℕ) (h : x ∈ evaln (k + 1) a n), x ∈ a.eval n) →
      (∀ (n x : ℕ) (h : x ∈ evaln (k + 1) a_1 n), x ∈ a_1.eval n) →
        ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) (a.comp a_1) n), x ∈ (a.comp a_1).eval n
prec :
  ∀ (a a_1 : Code),
    (∀ (n x : ℕ) (h : x ∈ evaln (k + 1) a n), x ∈ a.eval n) →
      (∀ (n x : ℕ) (h : x ∈ evaln (k + 1) a_1 n), x ∈ a_1.eval n) →
        ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) (a.prec a_1) n), x ∈ (a.prec a_1).eval n
rfind' :
  ∀ (a : Code),
    (∀ (n x : ℕ) (h : x ∈ evaln (k + 1) a n), x ∈ a.eval n) →
      ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) a.rfind' n), x ∈ a.rfind'.eval n
⊢ x ∈ c.eval n

Tactic:
induction c generalizing x n
-- Module: Mathlib.Computability.PartrecCode
Goal:
k n x : ℕ
h : x ∈ evaln (k + 1) zero n
⊢ n ≤ k ∧ 0 = x

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

Premises used: Nat.Partrec.Code.evaln, Seq.seq, Nat.Partrec.Code.eval, Option.bind_eq_some_iff
-- Module: Mathlib.Computability.PartrecCode
Goal:
k n x : ℕ
h : x ∈ evaln (k + 1) Code.succ n
succ : ∀ (h : n ≤ k ∧ n + 1 = x), x = n + 1
⊢ x ∈ Code.succ.eval n

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

Premises used: Nat.Partrec.Code.evaln, Seq.seq, Nat.Partrec.Code.eval, Option.bind_eq_some_iff
-- Module: Mathlib.Computability.PartrecCode
Goal:
k n x : ℕ
h : x ∈ evaln (k + 1) Code.left n
left : ∀ (h : n ≤ k ∧ (unpair n).1 = x), x = (unpair n).1
⊢ x ∈ Code.left.eval n

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

Premises used: Nat.Partrec.Code.evaln, Seq.seq, Nat.Partrec.Code.eval, Option.bind_eq_some_iff
-- Module: Mathlib.Computability.PartrecCode
Goal:
k n x : ℕ
h : x ∈ evaln (k + 1) Code.right n
right : ∀ (h : n ≤ k ∧ (unpair n).2 = x), x = (unpair n).2
⊢ x ∈ Code.right.eval n

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

Premises used: Nat.Partrec.Code.evaln, Seq.seq, Nat.Partrec.Code.eval, Option.bind_eq_some_iff
-- Module: Mathlib.Computability.PartrecCode
Goal:
k : ℕ
a a_1 : Code
a_ih : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) a n), x ∈ a.eval n
a_ih_1 : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) a_1 n), x ∈ a_1.eval n
n x : ℕ
h : x ∈ evaln (k + 1) (a.pair a_1) n
pair :
  ∀
    (h :
      n ≤ k ∧ ∃ (a_2 : ℕ), evaln (k + 1) a n = some a_2 ∧ ∃ (a : ℕ), evaln (k + 1) a_1 n = some a ∧ Nat.pair a_2 a = x),
    ∃ a_2 ∈ a.eval n, ∃ a ∈ a_1.eval n, Nat.pair a_2 a = x
⊢ x ∈ (a.pair a_1).eval n

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

Premises used: Nat.Partrec.Code.evaln, Seq.seq, Nat.Partrec.Code.eval, Option.bind_eq_some_iff
-- Module: Mathlib.Computability.PartrecCode
Goal:
k : ℕ
a a_1 : Code
a_ih : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) a n), x ∈ a.eval n
a_ih_1 : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) a_1 n), x ∈ a_1.eval n
n x : ℕ
h : x ∈ evaln (k + 1) (a.comp a_1) n
comp :
  ∀ (h : n ≤ k ∧ ∃ (a_2 : ℕ), evaln (k + 1) a_1 n = some a_2 ∧ evaln (k + 1) a a_2 = some x),
    ∃ a_2 ∈ a_1.eval n, x ∈ a.eval a_2
⊢ x ∈ (a.comp a_1).eval n

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

Premises used: Nat.Partrec.Code.evaln, Seq.seq, Nat.Partrec.Code.eval, Option.bind_eq_some_iff
-- Module: Mathlib.Computability.PartrecCode
Goal:
k : ℕ
a a_1 : Code
a_ih : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) a n), x ∈ a.eval n
a_ih_1 : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) a_1 n), x ∈ a_1.eval n
n x : ℕ
h : x ∈ evaln (k + 1) (a.prec a_1) n
prec :
  ∀
    (h :
      n ≤ k ∧
        Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) a (unpair n).1)
            (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
              (evaln k (a.prec a_1) (Nat.pair (unpair n).1 n_1)).bind fun (i : ℕ) ↦
                evaln (k + 1) a_1 (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
            (unpair n).2 =
          some x),
    Membership.mem (γ := Part ℕ)
      (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (a.eval (unpair n).1)
          (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ a_1.eval (Nat.pair (unpair n).1 (Nat.pair y i)))
          (unpair n).2 :
        Part ℕ)
      x
⊢ x ∈ (a.prec a_1).eval n

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

Premises used: Nat.Partrec.Code.evaln, Seq.seq, Nat.Partrec.Code.eval, Option.bind_eq_some_iff
-- Module: Mathlib.Computability.PartrecCode
Goal:
k : ℕ
a : Code
a_ih : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) a n), x ∈ a.eval n
n x : ℕ
h : x ∈ evaln (k + 1) a.rfind' n
rfind' :
  ∀
    (h :
      n ≤ k ∧
        ∃ (a_1 : ℕ),
          evaln (k + 1) a n = some a_1 ∧
            (if a_1 = 0 then some (unpair n).2 else evaln k a.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) =
              some x),
    ∃ (a_1 : ℕ),
      (0 ∈ a.eval (Nat.pair (unpair n).1 (a_1 + (unpair n).2)) ∧
          ∀ {m : ℕ}, m < a_1 → ∃ a_3 ∈ a.eval (Nat.pair (unpair n).1 (m + (unpair n).2)), ¬a_3 = 0) ∧
        a_1 + (unpair n).2 = x
⊢ x ∈ a.rfind'.eval n

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

Premises used: Nat.Partrec.Code.evaln, Seq.seq, Nat.Partrec.Code.eval, Option.bind_eq_some_iff
-- Module: Mathlib.Computability.PartrecCode
Goal:
k n x : ℕ
h : n ≤ k ∧ 0 = x
⊢ n ≤ k

Tactic:
obtain ⟨_, h⟩ := h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k n x : ℕ
h : n ≤ k ∧ 0 = x
left : n ≤ k
⊢ 0 = x

Tactic:
obtain ⟨_, h⟩ := h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k n x : ℕ
h : n ≤ k ∧ n + 1 = x
⊢ n ≤ k

Tactic:
obtain ⟨_, h⟩ := h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k n x : ℕ
h : n ≤ k ∧ n + 1 = x
left : n ≤ k
⊢ n + 1 = x

Tactic:
obtain ⟨_, h⟩ := h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k n x : ℕ
h : n ≤ k ∧ (unpair n).1 = x
⊢ n ≤ k

Tactic:
obtain ⟨_, h⟩ := h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k n x : ℕ
h : n ≤ k ∧ (unpair n).1 = x
left : n ≤ k
⊢ (unpair n).1 = x

Tactic:
obtain ⟨_, h⟩ := h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k n x : ℕ
h : n ≤ k ∧ (unpair n).2 = x
⊢ n ≤ k

Tactic:
obtain ⟨_, h⟩ := h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k n x : ℕ
h : n ≤ k ∧ (unpair n).2 = x
left : n ≤ k
⊢ (unpair n).2 = x

Tactic:
obtain ⟨_, h⟩ := h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k : ℕ
a a_1 : Code
a_ih : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) a n), x ∈ a.eval n
a_ih_1 : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) a_1 n), x ∈ a_1.eval n
n x : ℕ
h : n ≤ k ∧ ∃ (a_2 : ℕ), evaln (k + 1) a n = some a_2 ∧ ∃ (a : ℕ), evaln (k + 1) a_1 n = some a ∧ Nat.pair a_2 a = x
⊢ n ≤ k

Tactic:
obtain ⟨_, h⟩ := h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k : ℕ
a a_1 : Code
a_ih : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) a n), x ∈ a.eval n
a_ih_1 : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) a_1 n), x ∈ a_1.eval n
n x : ℕ
h : n ≤ k ∧ ∃ (a_2 : ℕ), evaln (k + 1) a n = some a_2 ∧ ∃ (a : ℕ), evaln (k + 1) a_1 n = some a ∧ Nat.pair a_2 a = x
left : n ≤ k
⊢ ∃ (a_2 : ℕ), evaln (k + 1) a n = some a_2 ∧ ∃ (a : ℕ), evaln (k + 1) a_1 n = some a ∧ Nat.pair a_2 a = x

Tactic:
obtain ⟨_, h⟩ := h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k : ℕ
a a_1 : Code
a_ih : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) a n), x ∈ a.eval n
a_ih_1 : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) a_1 n), x ∈ a_1.eval n
n x : ℕ
h : n ≤ k ∧ ∃ (a_2 : ℕ), evaln (k + 1) a_1 n = some a_2 ∧ evaln (k + 1) a a_2 = some x
⊢ n ≤ k

Tactic:
obtain ⟨_, h⟩ := h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k : ℕ
a a_1 : Code
a_ih : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) a n), x ∈ a.eval n
a_ih_1 : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) a_1 n), x ∈ a_1.eval n
n x : ℕ
h : n ≤ k ∧ ∃ (a_2 : ℕ), evaln (k + 1) a_1 n = some a_2 ∧ evaln (k + 1) a a_2 = some x
left : n ≤ k
⊢ ∃ (a_2 : ℕ), evaln (k + 1) a_1 n = some a_2 ∧ evaln (k + 1) a a_2 = some x

Tactic:
obtain ⟨_, h⟩ := h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k : ℕ
a a_1 : Code
a_ih : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) a n), x ∈ a.eval n
a_ih_1 : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) a_1 n), x ∈ a_1.eval n
n x : ℕ
h :
  n ≤ k ∧
    Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) a (unpair n).1)
        (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
          (evaln k (a.prec a_1) (Nat.pair (unpair n).1 n_1)).bind fun (i : ℕ) ↦
            evaln (k + 1) a_1 (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
        (unpair n).2 =
      some x
⊢ n ≤ k

Tactic:
obtain ⟨_, h⟩ := h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k : ℕ
a a_1 : Code
a_ih : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) a n), x ∈ a.eval n
a_ih_1 : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) a_1 n), x ∈ a_1.eval n
n x : ℕ
h :
  n ≤ k ∧
    Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) a (unpair n).1)
        (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
          (evaln k (a.prec a_1) (Nat.pair (unpair n).1 n_1)).bind fun (i : ℕ) ↦
            evaln (k + 1) a_1 (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
        (unpair n).2 =
      some x
left : n ≤ k
⊢ Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) a (unpair n).1)
      (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
        (evaln k (a.prec a_1) (Nat.pair (unpair n).1 n_1)).bind fun (i : ℕ) ↦
          evaln (k + 1) a_1 (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
      (unpair n).2 =
    some x

Tactic:
obtain ⟨_, h⟩ := h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k : ℕ
a : Code
a_ih : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) a n), x ∈ a.eval n
n x : ℕ
h :
  n ≤ k ∧
    ∃ (a_1 : ℕ),
      evaln (k + 1) a n = some a_1 ∧
        (if a_1 = 0 then some (unpair n).2 else evaln k a.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x
⊢ n ≤ k

Tactic:
obtain ⟨_, h⟩ := h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k : ℕ
a : Code
a_ih : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) a n), x ∈ a.eval n
n x : ℕ
h :
  n ≤ k ∧
    ∃ (a_1 : ℕ),
      evaln (k + 1) a n = some a_1 ∧
        (if a_1 = 0 then some (unpair n).2 else evaln k a.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x
left : n ≤ k
⊢ ∃ (a_1 : ℕ),
    evaln (k + 1) a n = some a_1 ∧
      (if a_1 = 0 then some (unpair n).2 else evaln k a.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x

Tactic:
obtain ⟨_, h⟩ := h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k n x : ℕ
left : n ≤ k
h : 0 = x
⊢ Membership.mem (γ := Part ℕ) (pure 0 n) x

Tactic:
simpa [pure, PFun.pure, eq_comm] using h

Premises used: Pure.pure, eq_comm, PFun.pure
-- Module: Mathlib.Computability.PartrecCode
Goal:
k n x : ℕ
left : n ≤ k
h : n + 1 = x
⊢ x = n + 1

Tactic:
simpa [pure, PFun.pure, eq_comm] using h

Premises used: Pure.pure, eq_comm, PFun.pure
-- Module: Mathlib.Computability.PartrecCode
Goal:
k n x : ℕ
left : n ≤ k
h : (unpair n).1 = x
⊢ x = (unpair n).1

Tactic:
simpa [pure, PFun.pure, eq_comm] using h

Premises used: Pure.pure, eq_comm, PFun.pure
-- Module: Mathlib.Computability.PartrecCode
Goal:
k n x : ℕ
left : n ≤ k
h : (unpair n).2 = x
⊢ x = (unpair n).2

Tactic:
simpa [pure, PFun.pure, eq_comm] using h

Premises used: Pure.pure, eq_comm, PFun.pure
-- Module: Mathlib.Computability.PartrecCode
Goal:
k : ℕ
cf cg : Code
hf : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cf n), x ∈ cf.eval n
hg : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cg n), x ∈ cg.eval n
n x : ℕ
left : n ≤ k
h : ∃ (a : ℕ), evaln (k + 1) cf n = some a ∧ ∃ (a_1 : ℕ), evaln (k + 1) cg n = some a_1 ∧ Nat.pair a a_1 = x
rcases :
  ∀ (y : ℕ) (ef : evaln (k + 1) cf n = some y) (z : ℕ) (eg : evaln (k + 1) cg n = some z),
    ∃ a ∈ cf.eval n, ∃ a_1 ∈ cg.eval n, Nat.pair a a_1 = Nat.pair y z
⊢ ∃ a ∈ cf.eval n, ∃ a_1 ∈ cg.eval n, Nat.pair a a_1 = x

Tactic:
rcases h with ⟨y, ef, z, eg, rfl⟩

Premises used: rfl
-- Module: Mathlib.Computability.PartrecCode
Goal:
k : ℕ
cf cg : Code
hf : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cf n), x ∈ cf.eval n
hg : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cg n), x ∈ cg.eval n
n : ℕ
left : n ≤ k
y : ℕ
ef : evaln (k + 1) cf n = some y
z : ℕ
eg : evaln (k + 1) cg n = some z
⊢ ∃ a ∈ cf.eval n, ∃ a_1 ∈ cg.eval n, Nat.pair a a_1 = Nat.pair y z

Tactic:
⟨_, hf _ _ ef, _, hg _ _ eg, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Computability.PartrecCode
Goal:
k : ℕ
cf cg : Code
hf : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cf n), x ∈ cf.eval n
hg : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cg n), x ∈ cg.eval n
n : ℕ
left : n ≤ k
y : ℕ
ef : evaln (k + 1) cf n = some y
z : ℕ
eg : evaln (k + 1) cg n = some z
⊢ ∃ a ∈ cf.eval n, ∃ a_1 ∈ cg.eval n, Nat.pair a a_1 = Nat.pair y z

Tactic:
exact ⟨_, hf _ _ ef, _, hg _ _ eg, rfl⟩
-- Module: Mathlib.Computability.PartrecCode
Goal:
k : ℕ
a a_1 : Code
a_ih : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) a n), x ∈ a.eval n
a_ih_1 : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) a_1 n), x ∈ a_1.eval n
n x : ℕ
left : n ≤ k
h : ∃ (a_2 : ℕ), evaln (k + 1) a n = some a_2 ∧ ∃ (a : ℕ), evaln (k + 1) a_1 n = some a ∧ Nat.pair a_2 a = x
⊢ ∃ a_2 ∈ a.eval n, ∃ a ∈ a_1.eval n, Nat.pair a_2 a = x

Tactic:
case pair cf cg hf hg _ =>
      rcases h with ⟨y, ef, z, eg, rfl⟩
      exact ⟨_, hf _ _ ef, _, hg _ _ eg, rfl⟩

Premises used: Nat.Partrec.Code.pair, rfl
-- Module: Mathlib.Computability.PartrecCode
Goal:
k : ℕ
cf cg : Code
hf : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cf n), x ∈ cf.eval n
hg : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cg n), x ∈ cg.eval n
n x : ℕ
left : n ≤ k
h : ∃ (a : ℕ), evaln (k + 1) cg n = some a ∧ evaln (k + 1) cf a = some x
rcases : ∀ (y : ℕ) (eg : evaln (k + 1) cg n = some y) (ef : evaln (k + 1) cf y = some x), ∃ a ∈ cg.eval n, x ∈ cf.eval a
⊢ ∃ a ∈ cg.eval n, x ∈ cf.eval a

Tactic:
rcases h with ⟨y, eg, ef⟩
-- Module: Mathlib.Computability.PartrecCode
Goal:
k : ℕ
cf cg : Code
hf : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cf n), x ∈ cf.eval n
hg : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cg n), x ∈ cg.eval n
n x : ℕ
left : n ≤ k
y : ℕ
eg : evaln (k + 1) cg n = some y
ef : evaln (k + 1) cf y = some x
⊢ ∃ a ∈ cg.eval n, x ∈ cf.eval a

Tactic:
⟨_, hg _ _ eg, hf _ _ ef⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Computability.PartrecCode
Goal:
k : ℕ
cf cg : Code
hf : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cf n), x ∈ cf.eval n
hg : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cg n), x ∈ cg.eval n
n x : ℕ
left : n ≤ k
y : ℕ
eg : evaln (k + 1) cg n = some y
ef : evaln (k + 1) cf y = some x
⊢ ∃ a ∈ cg.eval n, x ∈ cf.eval a

Tactic:
exact ⟨_, hg _ _ eg, hf _ _ ef⟩
-- Module: Mathlib.Computability.PartrecCode
Goal:
k : ℕ
a a_1 : Code
a_ih : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) a n), x ∈ a.eval n
a_ih_1 : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) a_1 n), x ∈ a_1.eval n
n x : ℕ
left : n ≤ k
h : ∃ (a_2 : ℕ), evaln (k + 1) a_1 n = some a_2 ∧ evaln (k + 1) a a_2 = some x
⊢ ∃ a_2 ∈ a_1.eval n, x ∈ a.eval a_2

Tactic:
case comp cf cg hf hg _ =>
      rcases h with ⟨y, eg, ef⟩
      exact ⟨_, hg _ _ eg, hf _ _ ef⟩

Premises used: Nat.Partrec.Code.comp
-- Module: Mathlib.Computability.PartrecCode
Goal:
k : ℕ
cf cg : Code
hf : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cf n), x ∈ cf.eval n
hg : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cg n), x ∈ cg.eval n
n x : ℕ
left : n ≤ k
h :
  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
revert :
  ∀
    (h :
      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),
    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
⊢ 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

Tactic:
revert h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k : ℕ
cf cg : Code
hf : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cf n), x ∈ cf.eval n
hg : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cg n), x ∈ cg.eval n
n : ℕ
left : n ≤ k
x : ℕ
⊢ ∀ (h : evaln (k + 1) cf (unpair n).1 = some x), x ∈ cf.eval (unpair n).1

Tactic:
apply hf
-- Module: Mathlib.Computability.PartrecCode
Goal:
k : ℕ
cf cg : Code
hf : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cf n), x ∈ cf.eval n
hg : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cg n), x ∈ cg.eval n
n : ℕ
left : n ≤ k
m : ℕ
IH :
  ∀ (x : ℕ)
    (h :
      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)))
          m =
        some x),
    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))) m :
        Part ℕ)
      x
x : ℕ
succ :
  ∀ (x_1 : ℕ),
    evaln k (cf.prec cg) (Nat.pair (unpair n).1 m) = some x_1 →
      evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair m x_1)) = some x →
        ∃ (a : ℕ),
          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))) m :
                Part ℕ)
              a ∧
            x ∈ cg.eval (Nat.pair (unpair n).1 (Nat.pair m a))
⊢ ∀
    (h :
      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)))
          (m + 1) =
        some x),
    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))) (m + 1) :
        Part ℕ)
      x

Tactic:
simp [Option.bind_eq_some_iff]

Premises used: Option.bind_eq_some_iff
-- Module: Mathlib.Computability.PartrecCode
Goal:
k : ℕ
cf cg : Code
hf : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cf n), x ∈ cf.eval n
hg : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cg n), x ∈ cg.eval n
n : ℕ
left : n ≤ k
m : ℕ
IH :
  ∀ (x : ℕ)
    (h :
      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)))
          m =
        some x),
    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))) m :
        Part ℕ)
      x
x : ℕ
⊢ ∀ (x_1 : ℕ),
    evaln k (cf.prec cg) (Nat.pair (unpair n).1 m) = some x_1 →
      evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair m x_1)) = some x →
        ∃ (a : ℕ),
          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))) m :
                Part ℕ)
              a ∧
            x ∈ cg.eval (Nat.pair (unpair n).1 (Nat.pair m a))

Tactic:
fun y h₁ h₂ => ⟨y, IH _ ?_, ?_⟩

Premises used: And.intro, Exists.intro