awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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 : ℕ
⊢ ∀
    (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
have 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))
Tactic: simp [Option.bind_eq_some_iff]
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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))
have succ : ∀ (y : ℕ) (h₁ : evaln k (cf.prec cg) (Nat.pair (unpair n).1 m) = some y)
  (h₂ : evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair m y)) = some x),
  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 y
Tactic: refine fun y h₁ h₂ => ⟨y, IH _ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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 :
  ∀ (y : ℕ) (h₁ : evaln k (cf.prec cg) (Nat.pair (unpair n).1 m) = some y)
    (h₂ : evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair m y)) = some x),
    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 y
⊢ ∀ (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))
have succ₁ : ∀ (y : ℕ) (h₁ : evaln k (cf.prec cg) (Nat.pair (unpair n).1 m) = some y)
  (h₂ : evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair m y)) = some x),
  x ∈ cg.eval (Nat.pair (unpair n).1 (Nat.pair m y))
Tactic: refine fun y h₁ h₂ => ⟨y, IH _ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
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 y : ℕ
h₁ : evaln k (cf.prec cg) (Nat.pair (unpair n).1 m) = some y
h₂ : evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair m y)) = some x
⊢ 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 y
have this : y ∈ evaln k.succ (cf.prec cg) (Nat.pair (unpair n).1 m)
Tactic: have := evaln_mono k.le_succ h₁
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
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 y : ℕ
h₁ : evaln k (cf.prec cg) (Nat.pair (unpair n).1 m) = some y
h₂ : evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair m y)) = some x
this : y ∈ evaln k.succ (cf.prec cg) (Nat.pair (unpair n).1 m)
⊢ 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 y
have this₁ : Nat.pair (unpair n).1 m ≤ 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)))
      m =
    some y
Tactic: simp [evaln, Option.bind_eq_some_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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),
    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
have induction : ∀ (x_1 : ℕ)
  (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)))
        x_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))) x_1 :
      Part ℕ)
    x
Tactic: induction n.unpair.2 generalizing x with simp [Option.bind_eq_some_iff]
      | zero => apply hf
      | succ m IH =>
        refine fun y h₁ h₂ => ⟨y, IH _ ?_, ?_⟩
        · have := evaln_mono k.le_succ h₁
          simp [evaln, Option.bind_eq_some_iff] at this
          exact this.2
        · exact hg _ _ h₂
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
k : ℕ
cf : Code
hf : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cf n), x ∈ cf.eval n
n x : ℕ
left : n ≤ k
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
⊢ ∃ (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
have rcases : ∀ (m : ℕ) (h₁ : evaln (k + 1) cf n = some m)
  (h₂ : (if m = 0 then some (unpair n).2 else evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x),
  ∃ (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
Tactic: rcases h with ⟨m, h₁, h₂⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
k : ℕ
cf : Code
hf : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cf n), x ∈ cf.eval n
n x : ℕ
left : n ≤ k
m : ℕ
h₁ : evaln (k + 1) cf n = some m
h₂ : (if m = 0 then some (unpair n).2 else evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x
⊢ ∃ (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
have pos : ∀ (m0 : m = 0),
  ∃ (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
Tactic: by_cases m0 : m = 0
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
k : ℕ
cf : Code
hf : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cf n), x ∈ cf.eval n
n x : ℕ
left : n ≤ k
m : ℕ
h₁ : evaln (k + 1) cf n = some m
h₂ : (if m = 0 then some (unpair n).2 else evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x
pos :
  ∀ (m0 : m = 0),
    ∃ (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
⊢ ∃ (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
have neg : ∀ (m0 : ¬m = 0),
  ∃ (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
Tactic: by_cases m0 : m = 0
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
Goal:
k : ℕ
cf : Code
hf : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cf n), x ∈ cf.eval n
n x : ℕ
left : n ≤ k
m : ℕ
h₁ : evaln (k + 1) cf n = some m
h₂ : (if m = 0 then some (unpair n).2 else evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x
m0 : m = 0
⊢ ∃ (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
have h₃ : (unpair n).2 = x
Tactic: simp [m0] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
Goal:
k : ℕ
cf : Code
hf : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cf n), x ∈ cf.eval n
n x : ℕ
left : n ≤ k
m : ℕ
h₁ : evaln (k + 1) cf n = some m
h₂ : (if m = 0 then some (unpair n).2 else evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x
m0 : ¬m = 0
⊢ ∃ (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
have h₃ : evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)) = some x
Tactic: simp [m0] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
Goal:
k : ℕ
cf : Code
hf : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cf n), x ∈ cf.eval n
n x : ℕ
left : n ≤ k
m : ℕ
h₁ : evaln (k + 1) cf n = some m
m0 : ¬m = 0
h₂ : evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)) = some x
⊢ ∃ (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
have this : x ∈ cf.rfind'.eval (Nat.pair (unpair n).1 ((unpair n).2 + 1))
Tactic: have := evaln_sound h₂
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
Goal:
k : ℕ
cf : Code
hf : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cf n), x ∈ cf.eval n
n x : ℕ
left : n ≤ k
m : ℕ
h₁ : evaln (k + 1) cf n = some m
m0 : ¬m = 0
h₂ : evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)) = some x
this : x ∈ cf.rfind'.eval (Nat.pair (unpair n).1 ((unpair n).2 + 1))
⊢ ∃ (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
have this₁ : ∃ (a : ℕ),
  (0 ∈ cf.eval (Nat.pair (unpair n).1 (a + ((unpair n).2 + 1))) ∧
      ∀ {m : ℕ}, m < a → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m + ((unpair n).2 + 1))), ¬a = 0) ∧
    a + ((unpair n).2 + 1) = x
Tactic: simp [eval] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
k : ℕ
cf : Code
hf : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cf n), x ∈ cf.eval n
n x : ℕ
left : n ≤ k
m : ℕ
h₁ : evaln (k + 1) cf n = some m
m0 : ¬m = 0
h₂ : evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)) = some x
this :
  ∃ (a : ℕ),
    (0 ∈ cf.eval (Nat.pair (unpair n).1 (a + ((unpair n).2 + 1))) ∧
        ∀ {m : ℕ}, m < a → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m + ((unpair n).2 + 1))), ¬a = 0) ∧
      a + ((unpair n).2 + 1) = x
⊢ ∃ (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
have neg : ∀ (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))),
  ∃ (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 = y + ((unpair n).2 + 1)
Tactic: rcases this with ⟨y, ⟨hy₁, hy₂⟩, rfl⟩
Cleared hypotheses: x, h₂, this
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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))
⊢ ∃ (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 = y + ((unpair n).2 + 1)
have neg : ∀ {i : ℕ} (im : i < y + 1), ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (i + (unpair n).2)), ¬a = 0
Tactic: refine
          ⟨y + 1, ⟨by simpa [add_comm, add_left_comm] using hy₁, fun {i} im => ?_⟩, by
            simp [add_comm, add_left_comm]⟩
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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 < y + 1
⊢ ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (i + (unpair n).2)), ¬a = 0
have neg : ∀ (im : 0 < y + 1), ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (0 + (unpair n).2)), ¬a = 0
Tactic: rcases i with - | i
Cleared hypotheses: i, im
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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 < y + 1
neg : ∀ (im : 0 < y + 1), ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (0 + (unpair n).2)), ¬a = 0
⊢ ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (i + (unpair n).2)), ¬a = 0
have neg₁ : ∀ (i : ℕ) (im : i + 1 < y + 1), ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (i + 1 + (unpair n).2)), ¬a = 0
Tactic: rcases i with - | i
Cleared hypotheses: i, im
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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
⊢ ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (i + 1 + (unpair n).2)), ¬a = 0
have neg : ∀ (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: rcases hy₂ (Nat.lt_of_succ_lt_succ im) with ⟨z, hz, z0⟩
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
c : Code
n x : ℕ
⊢ x ∈ c.eval n ↔ ∃ (k : ℕ), x ∈ evaln k c n
have refine : ∀ (h : x ∈ c.eval n), ∃ (k : ℕ), x ∈ evaln k c n
Tactic: refine ⟨fun h => ?_, fun ⟨k, h⟩ => evaln_sound h⟩
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
c : Code
n x : ℕ
h : x ∈ c.eval n
⊢ ∃ (k : ℕ), x ∈ evaln k c n
have rsuffices : ∀ (k : ℕ) (h : x ∈ evaln (k + 1) c n), ∃ (k : ℕ), x ∈ evaln k c n
Tactic: rsuffices ⟨k, h⟩ : ∃ k, x ∈ evaln (k + 1) c n
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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
⊢ ∃ (k : ℕ), x ∈ evaln k c n
have rsuffices₁ : ∃ (k : ℕ), x ∈ evaln (k + 1) c n
Tactic: rsuffices ⟨k, h⟩ : ∃ k, x ∈ evaln (k + 1) c n
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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
⊢ ∃ (k : ℕ), x ∈ evaln (k + 1) (cf.pair cg) n
have 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
Tactic: simp [eval, evaln, pure, PFun.pure, Seq.seq, Option.bind_eq_some_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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
⊢ ∃ (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
have 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
Tactic: rcases h with ⟨x, hx, y, hy, rfl⟩
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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 : ℕ),
    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
have 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
Tactic: rcases hf hx with ⟨k₁, hk₁⟩
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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 : ℕ),
    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
have 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
Tactic: rcases hg hy with ⟨k₂, hk₂⟩