awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.PartrecCode
Goal:
k : ℕ
cf cg : Code
hf : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cf n), x ∈ cf.eval n
hg : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cg n), x ∈ cg.eval n
n : ℕ
left : n ≤ k
m : ℕ
IH :
  ∀ (x : ℕ)
    (h :
      Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) cf (unpair n).1)
          (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
            (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun (i : ℕ) ↦
              evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
          m =
        some x),
    Membership.mem (γ := Part ℕ)
      (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval (unpair n).1)
          (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ cg.eval (Nat.pair (unpair n).1 (Nat.pair y i))) m :
        Part ℕ)
      x
x : ℕ
succ :
  ∀ (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
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))
⊢ ∀ (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:
refine fun y h₁ h₂ => ⟨y, IH _ ?_, ?_⟩
-- Module: Mathlib.Computability.PartrecCode
Goal:
k : ℕ
cf cg : Code
hf : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cf n), x ∈ cf.eval n
hg : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cg n), x ∈ cg.eval n
n : ℕ
left : n ≤ k
m : ℕ
IH :
  ∀ (x : ℕ)
    (h :
      Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) cf (unpair n).1)
          (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
            (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun (i : ℕ) ↦
              evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
          m =
        some x),
    Membership.mem (γ := Part ℕ)
      (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval (unpair n).1)
          (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ cg.eval (Nat.pair (unpair n).1 (Nat.pair y i))) m :
        Part ℕ)
      x
x 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
⊢ y ∈ evaln k.succ (cf.prec cg) (Nat.pair (unpair n).1 m)

Tactic:
have := evaln_mono k.le_succ h₁
-- Module: Mathlib.Computability.PartrecCode
Goal:
k : ℕ
cf cg : Code
hf : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cf n), x ∈ cf.eval n
hg : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cg n), x ∈ cg.eval n
n : ℕ
left : n ≤ k
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.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

Premises used: Nat.Partrec.Code.evaln, Option.bind_eq_some_iff
-- Module: Mathlib.Computability.PartrecCode
Goal:
k : ℕ
cf cg : Code
hf : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cf n), x ∈ cf.eval n
hg : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cg n), x ∈ cg.eval n
n : ℕ
left : n ≤ k
m : ℕ
IH :
  ∀ (x : ℕ)
    (h :
      Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) cf (unpair n).1)
          (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
            (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun (i : ℕ) ↦
              evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
          m =
        some x),
    Membership.mem (γ := Part ℕ)
      (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval (unpair n).1)
          (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ cg.eval (Nat.pair (unpair n).1 (Nat.pair y i))) m :
        Part ℕ)
      x
x 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 :
  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
⊢ 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:
this.2

Premises used: And.right
-- Module: Mathlib.Computability.PartrecCode
Goal:
k : ℕ
cf cg : Code
hf : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cf n), x ∈ cf.eval n
hg : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cg n), x ∈ cg.eval n
n : ℕ
left : n ≤ k
m : ℕ
IH :
  ∀ (x : ℕ)
    (h :
      Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) cf (unpair n).1)
          (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
            (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun (i : ℕ) ↦
              evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
          m =
        some x),
    Membership.mem (γ := Part ℕ)
      (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval (unpair n).1)
          (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ cg.eval (Nat.pair (unpair n).1 (Nat.pair y i))) m :
        Part ℕ)
      x
x 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 :
  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
⊢ 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:
exact this.2

Premises used: And.right
-- Module: Mathlib.Computability.PartrecCode
Goal:
k : ℕ
cf cg : Code
hf : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cf n), x ∈ cf.eval n
hg : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cg n), x ∈ cg.eval n
n : ℕ
left : n ≤ k
m : ℕ
IH :
  ∀ (x : ℕ)
    (h :
      Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) cf (unpair n).1)
          (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
            (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun (i : ℕ) ↦
              evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
          m =
        some x),
    Membership.mem (γ := Part ℕ)
      (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval (unpair n).1)
          (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ cg.eval (Nat.pair (unpair n).1 (Nat.pair y i))) m :
        Part ℕ)
      x
x 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:
hg _ _ h₂
-- Module: Mathlib.Computability.PartrecCode
Goal:
k : ℕ
cf cg : Code
hf : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cf n), x ∈ cf.eval n
hg : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cg n), x ∈ cg.eval n
n : ℕ
left : n ≤ k
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
⊢ x ∈ cg.eval (Nat.pair (unpair n).1 (Nat.pair m y))

Tactic:
exact hg _ _ h₂
-- Module: Mathlib.Computability.PartrecCode
Goal:
k : ℕ
cf cg : Code
hf : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cf n), x ∈ cf.eval n
hg : ∀ (n x : ℕ) (h : x ∈ evaln (k + 1) cg n), x ∈ cg.eval n
n x : ℕ
left : n ≤ k
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
⊢ ∀
    (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

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₂

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

Tactic:
case prec cf cg hf hg _ =>
      revert h
      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₂

Premises used: Nat.Partrec.Code.evaln, Nat.unpair, Nat.Partrec.Code.prec, Nat.Partrec.Code.succ, Nat.Partrec.Code.zero, Option.bind_eq_some_iff, Prod.snd
-- Module: Mathlib.Computability.PartrecCode
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
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
⊢ ∃ (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₂⟩
-- Module: Mathlib.Computability.PartrecCode
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
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
⊢ ∃ (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
-- Module: Mathlib.Computability.PartrecCode
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
⊢ (unpair n).2 = x

Tactic:
simp [m0] at h₂
-- Module: Mathlib.Computability.PartrecCode
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
⊢ evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)) = some x

Tactic:
simp [m0] at h₂
-- Module: Mathlib.Computability.PartrecCode
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₂ : (unpair n).2 = x
⊢ 0 ∈ cf.eval (Nat.pair (unpair n).1 (0 + (unpair n).2))

Tactic:
simpa [m0] using hf _ _ h₁
-- Module: Mathlib.Computability.PartrecCode
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₂ : (unpair n).2 = x
⊢ 0 + (unpair n).2 = x

Tactic:
simp [h₂]
-- Module: Mathlib.Computability.PartrecCode
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₂ : (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

Tactic:
exact
          ⟨0, ⟨by simpa [m0] using hf _ _ h₁, fun {m} => (Nat.not_lt_zero _).elim⟩, by simp [h₂]⟩
-- Module: Mathlib.Computability.PartrecCode
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
⊢ x ∈ cf.rfind'.eval (Nat.pair (unpair n).1 ((unpair n).2 + 1))

Tactic:
have := evaln_sound h₂
-- Module: Mathlib.Computability.PartrecCode
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 + 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

Premises used: Nat.Partrec.Code.eval
-- Module: Mathlib.Computability.PartrecCode
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
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)
⊢ ∃ (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 this with ⟨y, ⟨hy₁, hy₂⟩, rfl⟩

Premises used: rfl
-- Module: Mathlib.Computability.PartrecCode
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))
⊢ 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + 1 + (unpair n).2))

Tactic:
simpa [add_comm, add_left_comm] using hy₁

Premises used: add_left_comm, add_comm
-- Module: Mathlib.Computability.PartrecCode
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))
⊢ y + 1 + (unpair n).2 = y + ((unpair n).2 + 1)

Tactic:
simp [add_comm, add_left_comm]

Premises used: add_left_comm, add_comm
-- Module: Mathlib.Computability.PartrecCode
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))
neg : ∀ {i : ℕ} (im : i < y + 1), ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (i + (unpair n).2)), ¬a = 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 = y + ((unpair n).2 + 1)

Tactic:
refine
          ⟨y + 1, ⟨by simpa [add_comm, add_left_comm] using hy₁, fun {i} im => ?_⟩, by
            simp [add_comm, add_left_comm]⟩
-- Module: Mathlib.Computability.PartrecCode
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
neg₁ : ∀ (i : ℕ) (im : i + 1 < y + 1), ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (i + 1 + (unpair n).2)), ¬a = 0
⊢ ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (i + (unpair n).2)), ¬a = 0

Tactic:
rcases i with - | i
-- Module: Mathlib.Computability.PartrecCode
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))
im : 0 < y + 1
⊢ m ∈ cf.eval (Nat.pair (unpair n).1 (0 + (unpair n).2))

Tactic:
simpa using hf _ _ h₁
-- Module: Mathlib.Computability.PartrecCode
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))
im : 0 < y + 1
⊢ ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (0 + (unpair n).2)), ¬a = 0

Tactic:
exact ⟨m, by simpa using hf _ _ h₁, m0⟩
-- Module: Mathlib.Computability.PartrecCode
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
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
⊢ ∃ 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⟩

Premises used: Nat.lt_of_succ_lt_succ