awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
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
prec :
  ∀ (k₂ : ℕ) (hk₂ : x ∈ evaln (k₂ + 1) cg (Nat.pair n₁ (Nat.pair m 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 hg 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₁ 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))
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₂ : ℕ
hk₂ : x ∈ evaln (k₂ + 1) cg (Nat.pair n₁ (Nat.pair m 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

Tactic:
⟨(max k₁ k₂).succ,
          Nat.le_succ_of_le <| le_max_of_le_left <|
            le_trans (le_max_left _ (Nat.pair n₁ m)) nk₁, y,
          evaln_mono (Nat.succ_le_succ <| le_max_left _ _) ?_,
          evaln_mono (Nat.succ_le_succ <| Nat.le_succ_of_le <| le_max_right _ _) hk₂⟩

Premises used: le_max_right, Nat.pair, Max.max, And.intro, le_max_of_le_left, Exists.intro, Nat.le_succ_of_le, le_max_left, Nat.succ, Nat.Partrec.Code.evaln_mono, Nat.succ_le_succ, le_trans
-- 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))
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₂ : ℕ
hk₂ : x ∈ evaln (k₂ + 1) cg (Nat.pair n₁ (Nat.pair m y))
prec : y ∈ evaln k₁.succ (cf.prec cg) (Nat.pair n₁ m)
⊢ ∃ (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:
refine
        ⟨(max k₁ k₂).succ,
          Nat.le_succ_of_le <| le_max_of_le_left <|
            le_trans (le_max_left _ (Nat.pair n₁ m)) nk₁, y,
          evaln_mono (Nat.succ_le_succ <| le_max_left _ _) ?_,
          evaln_mono (Nat.succ_le_succ <| Nat.le_succ_of_le <| 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 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))
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₂ : ℕ
hk₂ : x ∈ evaln (k₂ + 1) cg (Nat.pair n₁ (Nat.pair m y))
prec :
  Nat.pair n₁ m ≤ 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 (a : ℕ) ↦ evaln (k₁ + 1) cg (Nat.pair n₁ (Nat.pair n a)))
        m =
      some y
⊢ y ∈ evaln k₁.succ (cf.prec cg) (Nat.pair n₁ m)

Tactic:
simp only [evaln.eq_8, bind, unpaired, unpair_pair, Option.mem_def, Option.bind_eq_some_iff,
        Option.guard_eq_some', exists_and_left, exists_const]

Premises used: Nat.Partrec.Code.evaln.eq_8, exists_and_left, Option.guard_eq_some', Nat.unpaired, exists_const, Bind.bind, Option.bind_eq_some_iff, Nat.unpair_pair, Option.mem_def
-- 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))
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₂ : ℕ
hk₂ : x ∈ evaln (k₂ + 1) cg (Nat.pair n₁ (Nat.pair m y))
⊢ Nat.pair n₁ m ≤ 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 (a : ℕ) ↦ evaln (k₁ + 1) cg (Nat.pair n₁ (Nat.pair n a)))
        m =
      some y

Tactic:
⟨le_trans (le_max_right _ _) nk₁, hk₁⟩

Premises used: le_max_right, And.intro, le_trans
-- 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))
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₂ : ℕ
hk₂ : x ∈ evaln (k₂ + 1) cg (Nat.pair n₁ (Nat.pair m y))
⊢ Nat.pair n₁ m ≤ 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 (a : ℕ) ↦ evaln (k₁ + 1) cg (Nat.pair n₁ (Nat.pair n a)))
        m =
      some y

Tactic:
exact ⟨le_trans (le_max_right _ _) nk₁, hk₁⟩
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
n x : ℕ
h : x ∈ cf.rfind'.eval n
rfind' :
  ∀
    (h :
      ∃ (a : ℕ),
        (0 ∈ cf.eval (Nat.pair (unpair n).1 (a + (unpair n).2)) ∧
            ∀ {m : ℕ}, m < a → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m + (unpair n).2)), ¬a = 0) ∧
          a + (unpair n).2 = x),
    ∃ (k : ℕ),
      n ≤ k ∧
        ∃ (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
⊢ ∃ (k : ℕ), x ∈ evaln (k + 1) cf.rfind' 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 : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
n x : ℕ
h :
  ∃ (a : ℕ),
    (0 ∈ cf.eval (Nat.pair (unpair n).1 (a + (unpair n).2)) ∧
        ∀ {m : ℕ}, m < a → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m + (unpair n).2)), ¬a = 0) ∧
      a + (unpair n).2 = x
rfind' :
  ∀ (y : ℕ) (hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + (unpair n).2)))
    (hy₂ : ∀ {m : ℕ}, m < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m + (unpair n).2)), ¬a = 0),
    ∃ (k : ℕ),
      n ≤ k ∧
        ∃ (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 (y + (unpair n).2)
⊢ ∃ (k : ℕ),
    n ≤ k ∧
      ∃ (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

Tactic:
rcases h with ⟨y, ⟨hy₁, hy₂⟩, rfl⟩

Premises used: rfl
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
n y : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + (unpair n).2))
hy₂ : ∀ {m : ℕ}, m < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m + (unpair n).2)), ¬a = 0
this : ∃ (k : ℕ), y + (unpair n).2 ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 (unpair n).2)
⊢ ∃ (k : ℕ),
    n ≤ k ∧
      ∃ (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 (y + (unpair n).2)

Tactic:
simpa [evaln, Option.bind_eq_some_iff]

Premises used: Nat.Partrec.Code.evaln, Option.bind_eq_some_iff
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
n y : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + (unpair n).2))
hy₂ : ∀ {m : ℕ}, m < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m + (unpair n).2)), ¬a = 0
rfind' : ∃ (k : ℕ), y + (unpair n).2 ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 (unpair n).2)
⊢ ∃ (k : ℕ),
    n ≤ k ∧
      ∃ (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 (y + (unpair n).2)

Tactic:
suffices ∃ k, y + n.unpair.2 ∈ evaln (k + 1) (rfind' cf) (Nat.pair n.unpair.1 n.unpair.2) by
      simpa [evaln, Option.bind_eq_some_iff]
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
n y : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + (unpair n).2))
hy₂ : ∀ {m : ℕ}, m < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m + (unpair n).2)), ¬a = 0
rfind' :
  ∀ (hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + (unpair n).2)))
    (hy₂ : ∀ {m : ℕ}, m < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m + (unpair n).2)), ¬a = 0),
    ∃ (k : ℕ), y + (unpair n).2 ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 (unpair n).2)
⊢ ∃ (k : ℕ), y + (unpair n).2 ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 (unpair n).2)

Tactic:
revert hy₁ hy₂
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
n y : ℕ
rfind' :
  ∀ (m : ℕ) (hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + m)))
    (hy₂ : ∀ {m_1 : ℕ}, m_1 < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0),
    ∃ (k : ℕ), y + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)
⊢ ∀ (hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + (unpair n).2)))
    (hy₂ : ∀ {m : ℕ}, m < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m + (unpair n).2)), ¬a = 0),
    ∃ (k : ℕ), y + (unpair n).2 ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 (unpair n).2)

Tactic:
generalize n.unpair.2 = m

Premises used: Nat.unpair, Prod.snd
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
n m : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (0 + m))
hy₂ : ∀ {m_1 : ℕ}, m_1 < 0 → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0
rfind' :
  ∃ (k : ℕ),
    Nat.pair (unpair n).1 m ≤ k ∧
      ∃ (a : ℕ),
        evaln (k + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
          (¬a = 0 → evaln k cf.rfind' (Nat.pair (unpair n).1 (m + 1)) = some m)
⊢ ∃ (k : ℕ), 0 + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)

Tactic:
simp [evaln, Option.bind_eq_some_iff]

Premises used: Nat.Partrec.Code.evaln, Option.bind_eq_some_iff
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
n m : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (0 + m))
hy₂ : ∀ {m_1 : ℕ}, m_1 < 0 → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0
⊢ 0 ∈ cf.eval (Nat.pair (unpair n).1 m)

Tactic:
simp at hy₁
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
n m : ℕ
hy₂ : ∀ {m_1 : ℕ}, m_1 < 0 → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 m)
rfind' :
  ∀ (k : ℕ) (hk : 0 ∈ evaln (k + 1) cf (Nat.pair (unpair n).1 m)),
    ∃ (k : ℕ),
      Nat.pair (unpair n).1 m ≤ k ∧
        ∃ (a : ℕ),
          evaln (k + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
            (¬a = 0 → evaln k cf.rfind' (Nat.pair (unpair n).1 (m + 1)) = some m)
⊢ ∃ (k : ℕ),
    Nat.pair (unpair n).1 m ≤ k ∧
      ∃ (a : ℕ),
        evaln (k + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
          (¬a = 0 → evaln k cf.rfind' (Nat.pair (unpair n).1 (m + 1)) = some m)

Tactic:
rcases hf hy₁ with ⟨k, hk⟩
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
n m : ℕ
hy₂ : ∀ {m_1 : ℕ}, m_1 < 0 → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 m)
k : ℕ
hk : 0 ∈ evaln (k + 1) cf (Nat.pair (unpair n).1 m)
⊢ ¬Eq (α := ℕ) 0 0 → evaln k cf.rfind' (Nat.pair (unpair n).1 (m + 1)) = some m

Tactic:
simp
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
n m : ℕ
hy₂ : ∀ {m_1 : ℕ}, m_1 < 0 → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 m)
k : ℕ
hk : 0 ∈ evaln (k + 1) cf (Nat.pair (unpair n).1 m)
⊢ ∃ (k : ℕ),
    Nat.pair (unpair n).1 m ≤ k ∧
      ∃ (a : ℕ),
        evaln (k + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
          (¬a = 0 → evaln k cf.rfind' (Nat.pair (unpair n).1 (m + 1)) = some m)

Tactic:
exact ⟨_, Nat.le_of_lt_succ <| evaln_bound hk, _, hk, by simp⟩
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
n y : ℕ
IH :
  ∀ (m : ℕ) (hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + m)))
    (hy₂ : ∀ {m_1 : ℕ}, m_1 < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0),
    ∃ (k : ℕ), y + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)
m : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + 1 + m))
hy₂ : ∀ {m_1 : ℕ}, m_1 < y + 1 → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0
rfind' :
  ∃ (k : ℕ),
    Nat.pair (unpair n).1 m ≤ k ∧
      ∃ (a : ℕ),
        evaln (k + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
          (if a = 0 then some m else evaln k cf.rfind' (Nat.pair (unpair n).1 (m + 1))) = some (y + 1 + m)
⊢ ∃ (k : ℕ), y + 1 + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)

Tactic:
simp [evaln, Option.bind_eq_some_iff]

Premises used: Nat.Partrec.Code.evaln, Option.bind_eq_some_iff
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
n y : ℕ
IH :
  ∀ (m : ℕ) (hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + m)))
    (hy₂ : ∀ {m_1 : ℕ}, m_1 < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0),
    ∃ (k : ℕ), y + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)
m : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + 1 + m))
hy₂ : ∀ {m_1 : ℕ}, m_1 < y + 1 → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0
rfind' :
  ∀ (a : ℕ) (ha : a ∈ cf.eval (Nat.pair (unpair n).1 (0 + m))) (a0 : ¬a = 0),
    ∃ (k : ℕ),
      Nat.pair (unpair n).1 m ≤ k ∧
        ∃ (a : ℕ),
          evaln (k + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
            (if a = 0 then some m else evaln k cf.rfind' (Nat.pair (unpair n).1 (m + 1))) = some (y + 1 + m)
⊢ ∃ (k : ℕ),
    Nat.pair (unpair n).1 m ≤ k ∧
      ∃ (a : ℕ),
        evaln (k + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
          (if a = 0 then some m else evaln k cf.rfind' (Nat.pair (unpair n).1 (m + 1))) = some (y + 1 + m)

Tactic:
rcases hy₂ (Nat.succ_pos _) with ⟨a, ha, a0⟩

Premises used: Nat.succ_pos
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
n y : ℕ
IH :
  ∀ (m : ℕ) (hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + m)))
    (hy₂ : ∀ {m_1 : ℕ}, m_1 < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0),
    ∃ (k : ℕ), y + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)
m : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + 1 + m))
hy₂ : ∀ {m_1 : ℕ}, m_1 < y + 1 → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0
a : ℕ
ha : a ∈ cf.eval (Nat.pair (unpair n).1 (0 + m))
a0 : ¬a = 0
rfind' :
  ∀ (k₁ : ℕ) (hk₁ : a ∈ evaln (k₁ + 1) cf (Nat.pair (unpair n).1 (0 + m))),
    ∃ (k : ℕ),
      Nat.pair (unpair n).1 m ≤ k ∧
        ∃ (a : ℕ),
          evaln (k + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
            (if a = 0 then some m else evaln k cf.rfind' (Nat.pair (unpair n).1 (m + 1))) = some (y + 1 + m)
⊢ ∃ (k : ℕ),
    Nat.pair (unpair n).1 m ≤ k ∧
      ∃ (a : ℕ),
        evaln (k + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
          (if a = 0 then some m else evaln k cf.rfind' (Nat.pair (unpair n).1 (m + 1))) = some (y + 1 + m)

Tactic:
rcases hf ha with ⟨k₁, hk₁⟩
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
n y : ℕ
IH :
  ∀ (m : ℕ) (hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + m)))
    (hy₂ : ∀ {m_1 : ℕ}, m_1 < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0),
    ∃ (k : ℕ), y + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)
m : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + 1 + m))
hy₂ : ∀ {m_1 : ℕ}, m_1 < y + 1 → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0
a : ℕ
ha : a ∈ cf.eval (Nat.pair (unpair n).1 (0 + m))
a0 : ¬a = 0
k₁ : ℕ
hk₁ : a ∈ evaln (k₁ + 1) cf (Nat.pair (unpair n).1 (0 + m))
⊢ 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + m.succ))

Tactic:
simpa [Nat.succ_eq_add_one, add_comm, add_left_comm] using hy₁

Premises used: Nat.succ_eq_add_one, add_left_comm, add_comm
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
n y : ℕ
IH :
  ∀ (m : ℕ) (hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + m)))
    (hy₂ : ∀ {m_1 : ℕ}, m_1 < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0),
    ∃ (k : ℕ), y + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)
m : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + 1 + m))
hy₂ : ∀ {m_1 : ℕ}, m_1 < y + 1 → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0
a : ℕ
ha : a ∈ cf.eval (Nat.pair (unpair n).1 (0 + m))
a0 : ¬a = 0
k₁ : ℕ
hk₁ : a ∈ evaln (k₁ + 1) cf (Nat.pair (unpair n).1 (0 + m))
i : ℕ
hi : i < y
⊢ ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (i + m.succ)), ¬a = 0

Tactic:
simpa [Nat.succ_eq_add_one, add_comm, add_left_comm] using
            hy₂ (Nat.succ_lt_succ hi)

Premises used: Nat.succ_eq_add_one, add_left_comm, Nat.succ_lt_succ, add_comm