awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂ : ℕ
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
have pair : n ≤ max k₁ k₂ ∧
  ∃ (a : ℕ),
    evaln (max k₁ k₂ + 1) cf n = some a ∧
      ∃ (a_1 : ℕ), evaln (max k₁ k₂ + 1) cg n = some a_1 ∧ Nat.pair a a_1 = Nat.pair x y
Tactic: refine ⟨max k₁ k₂, ?_⟩
-- 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.comp cg).eval n
⊢ ∃ (k : ℕ), x ∈ evaln (k + 1) (cf.comp cg) n
have comp : ∀ (h : ∃ a ∈ cg.eval n, x ∈ cf.eval a),
  ∃ (k : ℕ), n ≤ k ∧ ∃ (a : ℕ), evaln (k + 1) cg n = some a ∧ evaln (k + 1) cf a = some x
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 ∈ cg.eval n, x ∈ cf.eval a
⊢ ∃ (k : ℕ), n ≤ k ∧ ∃ (a : ℕ), evaln (k + 1) cg n = some a ∧ evaln (k + 1) cf a = some x
have comp : ∀ (y : ℕ) (hy : y ∈ cg.eval n) (hx : x ∈ cf.eval y),
  ∃ (k : ℕ), n ≤ k ∧ ∃ (a : ℕ), evaln (k + 1) cg n = some a ∧ evaln (k + 1) cf a = some x
Tactic: rcases h with ⟨y, hy, hx⟩
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 y : ℕ
hy : y ∈ cg.eval n
hx : x ∈ cf.eval y
⊢ ∃ (k : ℕ), n ≤ k ∧ ∃ (a : ℕ), evaln (k + 1) cg n = some a ∧ evaln (k + 1) cf a = some x
have comp : ∀ (k₁ : ℕ) (hk₁ : y ∈ evaln (k₁ + 1) cg n),
  ∃ (k : ℕ), n ≤ k ∧ ∃ (a : ℕ), evaln (k + 1) cg n = some a ∧ evaln (k + 1) cf a = some x
Tactic: rcases hg hy 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 y : ℕ
hy : y ∈ cg.eval n
hx : x ∈ cf.eval y
k₁ : ℕ
hk₁ : y ∈ evaln (k₁ + 1) cg n
⊢ ∃ (k : ℕ), n ≤ k ∧ ∃ (a : ℕ), evaln (k + 1) cg n = some a ∧ evaln (k + 1) cf a = some x
have comp : ∀ (k₂ : ℕ) (hk₂ : x ∈ evaln (k₂ + 1) cf y),
  ∃ (k : ℕ), n ≤ k ∧ ∃ (a : ℕ), evaln (k + 1) cg n = some a ∧ evaln (k + 1) cf a = some x
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 y : ℕ
hy : y ∈ cg.eval n
hx : x ∈ cf.eval y
k₁ : ℕ
hk₁ : y ∈ evaln (k₁ + 1) cg n
k₂ : ℕ
hk₂ : x ∈ evaln (k₂ + 1) cf y
⊢ ∃ (k : ℕ), n ≤ k ∧ ∃ (a : ℕ), evaln (k + 1) cg n = some a ∧ evaln (k + 1) cf a = some x
have comp : n ≤ max k₁ k₂ ∧ ∃ (a : ℕ), evaln (max k₁ k₂ + 1) cg n = some a ∧ evaln (max k₁ k₂ + 1) cf a = some x
Tactic: refine ⟨max k₁ k₂, ?_⟩
-- 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.prec cg).eval n
⊢ ∃ (k : ℕ), x ∈ evaln (k + 1) (cf.prec cg) n
have prec : ∃ (k : ℕ),
  n ≤ k ∧
    Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) cf (unpair n).1)
        (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
          (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun (i : ℕ) ↦
            evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
        (unpair n).2 =
      some x
Tactic: simp [eval, evaln, pure, PFun.pure, Seq.seq, Option.bind_eq_some_iff] at 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 :
  Membership.mem (γ := Part ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval (unpair n).1)
        (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ cg.eval (Nat.pair (unpair n).1 (Nat.pair y i)))
        (unpair n).2 :
      Part ℕ)
    x
⊢ ∃ (k : ℕ),
    n ≤ k ∧
      Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) cf (unpair n).1)
          (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
            (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun (i : ℕ) ↦
              evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
          (unpair n).2 =
        some x
have prec : ∀
  (h :
    Membership.mem (γ := Part ℕ)
      (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval (unpair n).1)
          (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ cg.eval (Nat.pair (unpair n).1 (Nat.pair y i)))
          (unpair n).2 :
        Part ℕ)
      x),
  ∃ (k : ℕ),
    n ≤ k ∧
      Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) cf (unpair n).1)
          (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
            (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun (i : ℕ) ↦
              evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
          (unpair n).2 =
        some x
Tactic: revert 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 :
      Membership.mem (γ := Part ℕ)
        (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval (unpair n).1)
            (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ cg.eval (Nat.pair (unpair n).1 (Nat.pair y i)))
            (unpair n).2 :
          Part ℕ)
        x),
    ∃ (k : ℕ),
      n ≤ k ∧
        Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) cf (unpair n).1)
            (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
              (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun (i : ℕ) ↦
                evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
            (unpair n).2 =
          some x
have prec : ∀ (n₁ : ℕ)
  (h :
    Membership.mem (γ := Part ℕ)
      (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval n₁)
          (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ cg.eval (Nat.pair n₁ (Nat.pair y i))) (unpair n).2 :
        Part ℕ)
      x),
  ∃ (k : ℕ),
    n ≤ k ∧
      Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) cf n₁)
          (fun (n : ℕ) (n_ih : Option ℕ) ↦
            (evaln k (cf.prec cg) (Nat.pair n₁ n)).bind fun (i : ℕ) ↦ evaln (k + 1) cg (Nat.pair n₁ (Nat.pair n i)))
          (unpair n).2 =
        some x
Tactic: generalize n.unpair.1 = 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 n₁ : ℕ
⊢ ∀
    (h :
      Membership.mem (γ := Part ℕ)
        (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval n₁)
            (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ cg.eval (Nat.pair n₁ (Nat.pair y i))) (unpair n).2 :
          Part ℕ)
        x),
    ∃ (k : ℕ),
      n ≤ k ∧
        Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) cf n₁)
            (fun (n : ℕ) (n_ih : Option ℕ) ↦
              (evaln k (cf.prec cg) (Nat.pair n₁ n)).bind fun (i : ℕ) ↦ evaln (k + 1) cg (Nat.pair n₁ (Nat.pair n i)))
            (unpair n).2 =
          some x
have prec : ∀ (n₂ : ℕ)
  (h :
    Membership.mem (γ := Part ℕ)
      (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval n₁)
          (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ cg.eval (Nat.pair n₁ (Nat.pair y i))) n₂ :
        Part ℕ)
      x),
  ∃ (k : ℕ),
    n ≤ k ∧
      Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) cf n₁)
          (fun (n : ℕ) (n_ih : Option ℕ) ↦
            (evaln k (cf.prec cg) (Nat.pair n₁ n)).bind fun (i : ℕ) ↦ evaln (k + 1) cg (Nat.pair n₁ (Nat.pair n i)))
          n₂ =
        some x
Tactic: generalize n.unpair.2 = 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₁ n x : ℕ
h : x ∈ cf.eval n₁
⊢ ∃ (k : ℕ), n ≤ k ∧ evaln (k + 1) cf n₁ = some x
have prec : ∀ (k : ℕ) (hk : x ∈ evaln (k + 1) cf n₁), ∃ (k : ℕ), n ≤ k ∧ evaln (k + 1) cf n₁ = some x
Tactic: rcases hf h 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₁ 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 : ℕ
⊢ ∀
    (h :
      Membership.mem (γ := Part ℕ)
        (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval n₁)
            (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ cg.eval (Nat.pair n₁ (Nat.pair y i))) (m + 1) :
          Part ℕ)
        x),
    ∃ (k : ℕ),
      n ≤ k ∧
        Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) cf n₁)
            (fun (n : ℕ) (n_ih : Option ℕ) ↦
              (evaln k (cf.prec cg) (Nat.pair n₁ n)).bind fun (i : ℕ) ↦ evaln (k + 1) cg (Nat.pair n₁ (Nat.pair n i)))
            (m + 1) =
          some x
have prec : ∀ (x_1 : ℕ),
  Membership.mem (γ := Part ℕ)
      (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval n₁)
          (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ cg.eval (Nat.pair n₁ (Nat.pair y i))) m :
        Part ℕ)
      x_1 →
    x ∈ cg.eval (Nat.pair n₁ (Nat.pair m x_1)) →
      ∃ (k : ℕ),
        n ≤ k ∧
          ∃ (a : ℕ),
            evaln k (cf.prec cg) (Nat.pair n₁ m) = some a ∧ evaln (k + 1) cg (Nat.pair n₁ (Nat.pair m a)) = some x
Tactic: simp [Option.bind_eq_some_iff]
-- 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₁ 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 : ℕ),
    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
have prec : ∀ (k₁ : ℕ) (nk₁ : max n (Nat.pair n₁ m) ≤ k₁)
  (hk₁ :
    Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k₁ + 1) cf n₁)
        (fun (n : ℕ) (n_ih : Option ℕ) ↦
          (evaln k₁ (cf.prec cg) (Nat.pair n₁ n)).bind fun (i : ℕ) ↦ evaln (k₁ + 1) cg (Nat.pair n₁ (Nat.pair n i)))
        m =
      some y),
  ∃ (k : ℕ),
    n ≤ k ∧
      ∃ (a : ℕ), evaln k (cf.prec cg) (Nat.pair n₁ m) = some a ∧ evaln (k + 1) cg (Nat.pair n₁ (Nat.pair m a)) = some x
Tactic: rcases IH hy with ⟨k₁, nk₁, 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₁ 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 : ℕ),
    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
have 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
Tactic: rcases hg 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₁ 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
have prec : y ∈ evaln k₁.succ (cf.prec cg) (Nat.pair n₁ m)
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₂⟩
-- 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₁ 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))
⊢ y ∈ evaln k₁.succ (cf.prec cg) (Nat.pair n₁ m)
have 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
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]
-- 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 n₁ n₂ : ℕ
⊢ ∀
    (h :
      Membership.mem (γ := Part ℕ)
        (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval n₁)
            (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ cg.eval (Nat.pair n₁ (Nat.pair y i))) n₂ :
          Part ℕ)
        x),
    ∃ (k : ℕ),
      n ≤ k ∧
        Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) cf n₁)
            (fun (n : ℕ) (n_ih : Option ℕ) ↦
              (evaln k (cf.prec cg) (Nat.pair n₁ n)).bind fun (i : ℕ) ↦ evaln (k + 1) cg (Nat.pair n₁ (Nat.pair n i)))
            n₂ =
          some x
have prec : ∀ {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))) 0 :
        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)))
          0 =
        some x
Tactic: induction n₂ generalizing x n with simp [Option.bind_eq_some_iff]
    | zero =>
      intro h
      rcases hf h with ⟨k, hk⟩
      exact ⟨_, le_max_left _ _, evaln_mono (Nat.succ_le_succ <| le_max_right _ _) hk⟩
    | succ m IH =>
      intro y hy hx
      rcases IH hy with ⟨k₁, nk₁, hk₁⟩
      rcases hg hx with ⟨k₂, hk₂⟩
      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₂⟩
      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]
      exact ⟨le_trans (le_max_right _ _) nk₁, hk₁⟩
Cleared hypotheses: n, x, 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 n₁ n₂ : ℕ
prec :
  ∀ {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))) 0 :
          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)))
            0 =
          some x
⊢ ∀
    (h :
      Membership.mem (γ := Part ℕ)
        (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval n₁)
            (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ cg.eval (Nat.pair n₁ (Nat.pair y i))) n₂ :
          Part ℕ)
        x),
    ∃ (k : ℕ),
      n ≤ k ∧
        Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) cf n₁)
            (fun (n : ℕ) (n_ih : Option ℕ) ↦
              (evaln k (cf.prec cg) (Nat.pair n₁ n)).bind fun (i : ℕ) ↦ evaln (k + 1) cg (Nat.pair n₁ (Nat.pair n i)))
            n₂ =
          some x
have prec₁ : ∀ {n x : ℕ} (h : x ∈ cf.eval n₁), ∃ (k : ℕ), n ≤ k ∧ evaln (k + 1) cf n₁ = some x
Tactic: induction n₂ generalizing x n with simp [Option.bind_eq_some_iff]
    | zero =>
      intro h
      rcases hf h with ⟨k, hk⟩
      exact ⟨_, le_max_left _ _, evaln_mono (Nat.succ_le_succ <| le_max_right _ _) hk⟩
    | succ m IH =>
      intro y hy hx
      rcases IH hy with ⟨k₁, nk₁, hk₁⟩
      rcases hg hx with ⟨k₂, hk₂⟩
      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₂⟩
      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]
      exact ⟨le_trans (le_max_right _ _) nk₁, hk₁⟩
Cleared hypotheses: n, x, n₂
-- 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 : x ∈ cf.rfind'.eval n
⊢ ∃ (k : ℕ), x ∈ evaln (k + 1) cf.rfind' n
have 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
Tactic: simp [eval, evaln, pure, PFun.pure, Seq.seq, Option.bind_eq_some_iff] at h ⊢
Cleared hypotheses: h