awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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
⊢ ∃ (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
have 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)
Tactic: rcases h with ⟨y, ⟨hy₁, hy₂⟩, rfl⟩
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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
⊢ ∃ (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)
have rfind' : ∃ (k : ℕ), y + (unpair n).2 ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 (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]
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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
⊢ ∃ (k : ℕ), y + (unpair n).2 ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 (unpair n).2)
have 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)
Tactic: revert hy₁ hy₂
Cleared hypotheses: hy₁, hy₂
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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),
    ∃ (k : ℕ), y + (unpair n).2 ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 (unpair n).2)
have 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)
Tactic: generalize n.unpair.2 = m
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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
⊢ ∃ (k : ℕ), 0 + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)
have 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)
Tactic: simp [evaln, Option.bind_eq_some_iff]
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
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
⊢ ∃ (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)
have hy₃ : 0 ∈ cf.eval (Nat.pair (unpair n).1 m)
Tactic: simp at hy₁
Cleared hypotheses: hy₁
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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 : ℕ),
    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)
have 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)
Tactic: rcases hf hy₁ with ⟨k, hk⟩
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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
⊢ ∃ (k : ℕ), y + 1 + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)
have 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)
Tactic: simp [evaln, Option.bind_eq_some_iff]
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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
⊢ ∃ (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)
have 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)
Tactic: rcases hy₂ (Nat.succ_pos _) with ⟨a, ha, a0⟩
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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 : ℕ),
    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)
have 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)
Tactic: rcases hf ha with ⟨k₁, hk₁⟩
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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))
⊢ ∃ (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)
have rfind' : ∀ (k₂ : ℕ) (hk₂ : y + m.succ ∈ evaln (k₂ + 1) cf.rfind' (Nat.pair (unpair n).1 m.succ)),
  ∃ (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 IH m.succ (by simpa [Nat.succ_eq_add_one, add_comm, add_left_comm] using hy₁)
          fun {i} hi => by
          simpa [Nat.succ_eq_add_one, add_comm, add_left_comm] using
            hy₂ (Nat.succ_lt_succ hi) with
        ⟨k₂, hk₂⟩
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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))
k₂ : ℕ
hk₂ : y + m.succ ∈ evaln (k₂ + 1) cf.rfind' (Nat.pair (unpair n).1 m.succ)
⊢ ∃ (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)
have h : Nat.pair (unpair n).1 m ≤ (max k₁ k₂).succ ∧
  ∃ (a : ℕ),
    evaln ((max k₁ k₂).succ + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
      (if a = 0 then some m else evaln (max k₁ k₂).succ cf.rfind' (Nat.pair (unpair n).1 (m + 1))) = some (y + 1 + m)
Tactic: use (max k₁ k₂).succ
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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))
k₂ : ℕ
hk₂ : y + m.succ ∈ evaln (k₂ + 1) cf.rfind' (Nat.pair (unpair n).1 m.succ)
⊢ Nat.pair (unpair n).1 m ≤ (max k₁ k₂).succ ∧
    ∃ (a : ℕ),
      evaln ((max k₁ k₂).succ + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
        (if a = 0 then some m else evaln (max k₁ k₂).succ cf.rfind' (Nat.pair (unpair n).1 (m + 1))) = some (y + 1 + m)
have h : ∀ (hk₁ : a ∈ evaln (k₁ + 1) cf (Nat.pair (unpair n).1 m)) (k₂ : ℕ)
  (hk₂ : y + m.succ ∈ evaln (k₂ + 1) cf.rfind' (Nat.pair (unpair n).1 m.succ)),
  Nat.pair (unpair n).1 m ≤ (max k₁ k₂).succ ∧
    ∃ (a : ℕ),
      evaln ((max k₁ k₂).succ + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
        (if a = 0 then some m else evaln (max k₁ k₂).succ cf.rfind' (Nat.pair (unpair n).1 (m + 1))) = some (y + 1 + m)
Tactic: rw [zero_add] at hk₁
Cleared hypotheses: hk₁, k₂, hk₂
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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 m)
k₂ : ℕ
hk₂ : y + m.succ ∈ evaln (k₂ + 1) cf.rfind' (Nat.pair (unpair n).1 m.succ)
⊢ Nat.pair (unpair n).1 m ≤ (max k₁ k₂).succ ∧
    ∃ (a : ℕ),
      evaln ((max k₁ k₂).succ + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
        (if a = 0 then some m else evaln (max k₁ k₂).succ cf.rfind' (Nat.pair (unpair n).1 (m + 1))) = some (y + 1 + m)
have right : ∃ (a : ℕ),
  evaln ((max k₁ k₂).succ + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
    (if a = 0 then some m else evaln (max k₁ k₂).succ cf.rfind' (Nat.pair (unpair n).1 (m + 1))) = some (y + 1 + m)
Tactic: use Nat.le_succ_of_le <| le_max_of_le_left <| Nat.le_of_lt_succ <| evaln_bound hk₁
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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 m)
k₂ : ℕ
hk₂ : y + m.succ ∈ evaln (k₂ + 1) cf.rfind' (Nat.pair (unpair n).1 m.succ)
⊢ ∃ (a : ℕ),
    evaln ((max k₁ k₂).succ + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
      (if a = 0 then some m else evaln (max k₁ k₂).succ cf.rfind' (Nat.pair (unpair n).1 (m + 1))) = some (y + 1 + m)
have h : evaln ((max k₁ k₂).succ + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
  (if a = 0 then some m else evaln (max k₁ k₂).succ cf.rfind' (Nat.pair (unpair n).1 (m + 1))) = some (y + 1 + m)
Tactic: use a
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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 m)
k₂ : ℕ
hk₂ : y + m.succ ∈ evaln (k₂ + 1) cf.rfind' (Nat.pair (unpair n).1 m.succ)
⊢ evaln ((max k₁ k₂).succ + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
    (if a = 0 then some m else evaln (max k₁ k₂).succ cf.rfind' (Nat.pair (unpair n).1 (m + 1))) = some (y + 1 + m)
have right : (if a = 0 then some m else evaln (max k₁ k₂).succ cf.rfind' (Nat.pair (unpair n).1 (m + 1))) = some (y + 1 + m)
Tactic: use evaln_mono (Nat.succ_le_succ <| Nat.le_succ_of_le <| le_max_left _ _) hk₁
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
cf : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
n y 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)
have rfind' : ∀ (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),
  ∃ (k : ℕ), 0 + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)
Tactic: induction y generalizing m with simp [evaln, Option.bind_eq_some_iff]
    | zero =>
      simp at hy₁
      rcases hf hy₁ with ⟨k, hk⟩
      exact ⟨_, Nat.le_of_lt_succ <| evaln_bound hk, _, hk, by simp⟩
    | succ y IH =>
      rcases hy₂ (Nat.succ_pos _) with ⟨a, ha, a0⟩
      rcases hf ha with ⟨k₁, hk₁⟩
      rcases IH m.succ (by simpa [Nat.succ_eq_add_one, add_comm, add_left_comm] using hy₁)
          fun {i} hi => by
          simpa [Nat.succ_eq_add_one, add_comm, add_left_comm] using
            hy₂ (Nat.succ_lt_succ hi) with
        ⟨k₂, hk₂⟩
      use (max k₁ k₂).succ
      rw [zero_add] at hk₁
      use Nat.le_succ_of_le <| le_max_of_le_left <| Nat.le_of_lt_succ <| evaln_bound hk₁
      use a
      use evaln_mono (Nat.succ_le_succ <| Nat.le_succ_of_le <| le_max_left _ _) hk₁
      simpa [a0, add_comm, add_left_comm] using
        evaln_mono (Nat.succ_le_succ <| le_max_right _ _) hk₂
Cleared hypotheses: y, m, hy₁, hy₂
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
cf : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
n y 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
rfind' :
  ∀ (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),
    ∃ (k : ℕ), 0 + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)
⊢ ∃ (k : ℕ), y + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)
have rfind'₁ : ∀ (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),
  ∃ (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: induction y generalizing m with simp [evaln, Option.bind_eq_some_iff]
    | zero =>
      simp at hy₁
      rcases hf hy₁ with ⟨k, hk⟩
      exact ⟨_, Nat.le_of_lt_succ <| evaln_bound hk, _, hk, by simp⟩
    | succ y IH =>
      rcases hy₂ (Nat.succ_pos _) with ⟨a, ha, a0⟩
      rcases hf ha with ⟨k₁, hk₁⟩
      rcases IH m.succ (by simpa [Nat.succ_eq_add_one, add_comm, add_left_comm] using hy₁)
          fun {i} hi => by
          simpa [Nat.succ_eq_add_one, add_comm, add_left_comm] using
            hy₂ (Nat.succ_lt_succ hi) with
        ⟨k₂, hk₂⟩
      use (max k₁ k₂).succ
      rw [zero_add] at hk₁
      use Nat.le_succ_of_le <| le_max_of_le_left <| Nat.le_of_lt_succ <| evaln_bound hk₁
      use a
      use evaln_mono (Nat.succ_le_succ <| Nat.le_succ_of_le <| le_max_left _ _) hk₁
      simpa [a0, add_comm, add_left_comm] using
        evaln_mono (Nat.succ_le_succ <| le_max_right _ _) hk₂
Cleared hypotheses: y, m, hy₁, hy₂
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
cf : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
n y 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
rfind' :
  ∀ (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),
    ∃ (k : ℕ), 0 + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)
rfind'₁ :
  ∀ (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),
    ∃ (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 : ℕ), y + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)
have rfind'₂ : ∀ (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),
  ∃ (k : ℕ), y + 1 + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)
Tactic: induction y generalizing m with simp [evaln, Option.bind_eq_some_iff]
    | zero =>
      simp at hy₁
      rcases hf hy₁ with ⟨k, hk⟩
      exact ⟨_, Nat.le_of_lt_succ <| evaln_bound hk, _, hk, by simp⟩
    | succ y IH =>
      rcases hy₂ (Nat.succ_pos _) with ⟨a, ha, a0⟩
      rcases hf ha with ⟨k₁, hk₁⟩
      rcases IH m.succ (by simpa [Nat.succ_eq_add_one, add_comm, add_left_comm] using hy₁)
          fun {i} hi => by
          simpa [Nat.succ_eq_add_one, add_comm, add_left_comm] using
            hy₂ (Nat.succ_lt_succ hi) with
        ⟨k₂, hk₂⟩
      use (max k₁ k₂).succ
      rw [zero_add] at hk₁
      use Nat.le_succ_of_le <| le_max_of_le_left <| Nat.le_of_lt_succ <| evaln_bound hk₁
      use a
      use evaln_mono (Nat.succ_le_succ <| Nat.le_succ_of_le <| le_max_left _ _) hk₁
      simpa [a0, add_comm, add_left_comm] using
        evaln_mono (Nat.succ_le_succ <| le_max_right _ _) hk₂
Cleared hypotheses: y, m, hy₁, hy₂