awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
f : ℕ →. ℕ
h : Nat.Partrec f
refine_1 : ∃ (c : Code), c.eval = pure 0
refine_1₁ : ∃ (c : Code), c.eval = (↑Nat.succ : ℕ →. ℕ)
refine_1₂ : ∃ (c : Code), c.eval = (↑fun (n : ℕ) ↦ (unpair n).1 : ℕ →. ℕ)
refine_1₃ : ∃ (c : Code), c.eval = (↑fun (n : ℕ) ↦ (unpair n).2 : ℕ →. ℕ)
refine_1₄ :
  ∀ {f g : ℕ →. ℕ} (pf : Nat.Partrec f) (pg : Nat.Partrec g) (hf : ∃ (c : Code), c.eval = f)
    (hg : ∃ (c : Code), c.eval = g), ∃ (c : Code), c.eval = fun (n : ℕ) ↦ Nat.pair <$> f n <*> g n
refine_1₅ :
  ∀ {f g : ℕ →. ℕ} (pf : Nat.Partrec f) (pg : Nat.Partrec g) (hf : ∃ (c : Code), c.eval = f)
    (hg : ∃ (c : Code), c.eval = g), ∃ (c : Code), c.eval = fun (n : ℕ) ↦ g n >>= f
refine_1₆ :
  ∀ {f g : ℕ →. ℕ} (pf : Nat.Partrec f) (pg : Nat.Partrec g) (hf : ∃ (c : Code), c.eval = f)
    (hg : ∃ (c : Code), c.eval = g),
    ∃ (c : Code),
      c.eval =
        unpaired fun (a n : ℕ) ↦
          Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (f a)
            (fun (y : ℕ) (IH : Part ℕ) ↦ do
              let i ← IH
              g (Nat.pair a (Nat.pair y i)))
            n
⊢ ∃ (c : Code), c.eval = f
have refine_1₇ : ∀ {f : ℕ →. ℕ} (pf : Nat.Partrec f) (hf : ∃ (c : Code), c.eval = f),
  ∃ (c : Code), c.eval = fun (a : ℕ) ↦ Nat.rfind fun (n : ℕ) ↦ (fun (m : ℕ) ↦ decide (m = 0)) <$> f (Nat.pair a n)
Tactic: induction h with
    | zero => exact ⟨zero, rfl⟩
    | succ => exact ⟨succ, rfl⟩
    | left => exact ⟨left, rfl⟩
    | right => exact ⟨right, rfl⟩
    | pair pf pg hf hg =>
      rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
      exact ⟨pair cf cg, rfl⟩
    | comp pf pg hf hg =>
      rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
      exact ⟨comp cf cg, rfl⟩
    | prec pf pg hf hg =>
      rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
      exact ⟨prec cf cg, rfl⟩
    | rfind pf hf =>
      rcases hf with ⟨cf, rfl⟩
      refine ⟨comp (rfind' cf) (pair Code.id zero), ?_⟩
      simp [eval, Seq.seq, pure, PFun.pure, Part.map_id']
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
c : Code
⊢ Nat.Partrec c.eval
have refine_2 : Nat.Partrec zero.eval
Tactic: induction c with
    | zero => exact Nat.Partrec.zero
    | succ => exact Nat.Partrec.succ
    | left => exact Nat.Partrec.left
    | right => exact Nat.Partrec.right
    | pair cf cg pf pg => exact pf.pair pg
    | comp cf cg pf pg => exact pf.comp pg
    | prec cf cg pf pg => exact pf.prec pg
    | rfind' cf pf => exact pf.rfind'
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
c : Code
refine_2 : Nat.Partrec zero.eval
⊢ Nat.Partrec c.eval
have refine_2₁ : Nat.Partrec succ.eval
Tactic: induction c with
    | zero => exact Nat.Partrec.zero
    | succ => exact Nat.Partrec.succ
    | left => exact Nat.Partrec.left
    | right => exact Nat.Partrec.right
    | pair cf cg pf pg => exact pf.pair pg
    | comp cf cg pf pg => exact pf.comp pg
    | prec cf cg pf pg => exact pf.prec pg
    | rfind' cf pf => exact pf.rfind'
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
c : Code
refine_2 : Nat.Partrec zero.eval
refine_2₁ : Nat.Partrec succ.eval
⊢ Nat.Partrec c.eval
have refine_2₂ : Nat.Partrec left.eval
Tactic: induction c with
    | zero => exact Nat.Partrec.zero
    | succ => exact Nat.Partrec.succ
    | left => exact Nat.Partrec.left
    | right => exact Nat.Partrec.right
    | pair cf cg pf pg => exact pf.pair pg
    | comp cf cg pf pg => exact pf.comp pg
    | prec cf cg pf pg => exact pf.prec pg
    | rfind' cf pf => exact pf.rfind'
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
c : Code
refine_2 : Nat.Partrec zero.eval
refine_2₁ : Nat.Partrec succ.eval
refine_2₂ : Nat.Partrec left.eval
⊢ Nat.Partrec c.eval
have refine_2₃ : Nat.Partrec right.eval
Tactic: induction c with
    | zero => exact Nat.Partrec.zero
    | succ => exact Nat.Partrec.succ
    | left => exact Nat.Partrec.left
    | right => exact Nat.Partrec.right
    | pair cf cg pf pg => exact pf.pair pg
    | comp cf cg pf pg => exact pf.comp pg
    | prec cf cg pf pg => exact pf.prec pg
    | rfind' cf pf => exact pf.rfind'
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
c : Code
refine_2 : Nat.Partrec zero.eval
refine_2₁ : Nat.Partrec succ.eval
refine_2₂ : Nat.Partrec left.eval
refine_2₃ : Nat.Partrec right.eval
⊢ Nat.Partrec c.eval
have refine_2₄ : ∀ (cf cg : Code) (pf : Nat.Partrec cf.eval) (pg : Nat.Partrec cg.eval), Nat.Partrec (cf.pair cg).eval
Tactic: induction c with
    | zero => exact Nat.Partrec.zero
    | succ => exact Nat.Partrec.succ
    | left => exact Nat.Partrec.left
    | right => exact Nat.Partrec.right
    | pair cf cg pf pg => exact pf.pair pg
    | comp cf cg pf pg => exact pf.comp pg
    | prec cf cg pf pg => exact pf.prec pg
    | rfind' cf pf => exact pf.rfind'
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
c : Code
refine_2 : Nat.Partrec zero.eval
refine_2₁ : Nat.Partrec succ.eval
refine_2₂ : Nat.Partrec left.eval
refine_2₃ : Nat.Partrec right.eval
refine_2₄ : ∀ (cf cg : Code) (pf : Nat.Partrec cf.eval) (pg : Nat.Partrec cg.eval), Nat.Partrec (cf.pair cg).eval
⊢ Nat.Partrec c.eval
have refine_2₅ : ∀ (cf cg : Code) (pf : Nat.Partrec cf.eval) (pg : Nat.Partrec cg.eval), Nat.Partrec (cf.comp cg).eval
Tactic: induction c with
    | zero => exact Nat.Partrec.zero
    | succ => exact Nat.Partrec.succ
    | left => exact Nat.Partrec.left
    | right => exact Nat.Partrec.right
    | pair cf cg pf pg => exact pf.pair pg
    | comp cf cg pf pg => exact pf.comp pg
    | prec cf cg pf pg => exact pf.prec pg
    | rfind' cf pf => exact pf.rfind'
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
c : Code
refine_2 : Nat.Partrec zero.eval
refine_2₁ : Nat.Partrec succ.eval
refine_2₂ : Nat.Partrec left.eval
refine_2₃ : Nat.Partrec right.eval
refine_2₄ : ∀ (cf cg : Code) (pf : Nat.Partrec cf.eval) (pg : Nat.Partrec cg.eval), Nat.Partrec (cf.pair cg).eval
refine_2₅ : ∀ (cf cg : Code) (pf : Nat.Partrec cf.eval) (pg : Nat.Partrec cg.eval), Nat.Partrec (cf.comp cg).eval
⊢ Nat.Partrec c.eval
have refine_2₆ : ∀ (cf cg : Code) (pf : Nat.Partrec cf.eval) (pg : Nat.Partrec cg.eval), Nat.Partrec (cf.prec cg).eval
Tactic: induction c with
    | zero => exact Nat.Partrec.zero
    | succ => exact Nat.Partrec.succ
    | left => exact Nat.Partrec.left
    | right => exact Nat.Partrec.right
    | pair cf cg pf pg => exact pf.pair pg
    | comp cf cg pf pg => exact pf.comp pg
    | prec cf cg pf pg => exact pf.prec pg
    | rfind' cf pf => exact pf.rfind'
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
c : Code
refine_2 : Nat.Partrec zero.eval
refine_2₁ : Nat.Partrec succ.eval
refine_2₂ : Nat.Partrec left.eval
refine_2₃ : Nat.Partrec right.eval
refine_2₄ : ∀ (cf cg : Code) (pf : Nat.Partrec cf.eval) (pg : Nat.Partrec cg.eval), Nat.Partrec (cf.pair cg).eval
refine_2₅ : ∀ (cf cg : Code) (pf : Nat.Partrec cf.eval) (pg : Nat.Partrec cg.eval), Nat.Partrec (cf.comp cg).eval
refine_2₆ : ∀ (cf cg : Code) (pf : Nat.Partrec cf.eval) (pg : Nat.Partrec cg.eval), Nat.Partrec (cf.prec cg).eval
⊢ Nat.Partrec c.eval
have refine_2₇ : ∀ (cf : Code) (pf : Nat.Partrec cf.eval), Nat.Partrec cf.rfind'.eval
Tactic: induction c with
    | zero => exact Nat.Partrec.zero
    | succ => exact Nat.Partrec.succ
    | left => exact Nat.Partrec.left
    | right => exact Nat.Partrec.right
    | pair cf cg pf pg => exact pf.pair pg
    | comp cf cg pf pg => exact pf.comp pg
    | prec cf cg pf pg => exact pf.prec pg
    | rfind' cf pf => exact pf.rfind'
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
k : ℕ
c : Code
n x : ℕ
h : x ∈ evaln (k + 1) c n
this :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
⊢ n < k + 1
have zero : ∀ (h : x ∈ evaln (k + 1) zero n), n < k + 1
Tactic: cases c
Cleared hypotheses: c, h
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
k : ℕ
c : Code
n x : ℕ
h : x ∈ evaln (k + 1) c n
this :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
zero : ∀ (h : x ∈ evaln (k + 1) Code.zero n), n < k + 1
⊢ n < k + 1
have succ : ∀ (h : x ∈ evaln (k + 1) succ n), n < k + 1
Tactic: cases c
Cleared hypotheses: c, h
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
k : ℕ
c : Code
n x : ℕ
h : x ∈ evaln (k + 1) c n
this :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
zero : ∀ (h : x ∈ evaln (k + 1) Code.zero n), n < k + 1
succ : ∀ (h : x ∈ evaln (k + 1) Code.succ n), n < k + 1
⊢ n < k + 1
have left : ∀ (h : x ∈ evaln (k + 1) left n), n < k + 1
Tactic: cases c
Cleared hypotheses: c, h
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
k : ℕ
c : Code
n x : ℕ
h : x ∈ evaln (k + 1) c n
this :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
zero : ∀ (h : x ∈ evaln (k + 1) Code.zero n), n < k + 1
succ : ∀ (h : x ∈ evaln (k + 1) Code.succ n), n < k + 1
left : ∀ (h : x ∈ evaln (k + 1) Code.left n), n < k + 1
⊢ n < k + 1
have right : ∀ (h : x ∈ evaln (k + 1) right n), n < k + 1
Tactic: cases c
Cleared hypotheses: c, h
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
k : ℕ
c : Code
n x : ℕ
h : x ∈ evaln (k + 1) c n
this :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
zero : ∀ (h : x ∈ evaln (k + 1) Code.zero n), n < k + 1
succ : ∀ (h : x ∈ evaln (k + 1) Code.succ n), n < k + 1
left : ∀ (h : x ∈ evaln (k + 1) Code.left n), n < k + 1
right : ∀ (h : x ∈ evaln (k + 1) Code.right n), n < k + 1
⊢ n < k + 1
have pair : ∀ (a a_1 : Code) (h : x ∈ evaln (k + 1) (a.pair a_1) n), n < k + 1
Tactic: cases c
Cleared hypotheses: c, h
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
k : ℕ
c : Code
n x : ℕ
h : x ∈ evaln (k + 1) c n
this :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
zero : ∀ (h : x ∈ evaln (k + 1) Code.zero n), n < k + 1
succ : ∀ (h : x ∈ evaln (k + 1) Code.succ n), n < k + 1
left : ∀ (h : x ∈ evaln (k + 1) Code.left n), n < k + 1
right : ∀ (h : x ∈ evaln (k + 1) Code.right n), n < k + 1
pair : ∀ (a a_1 : Code) (h : x ∈ evaln (k + 1) (a.pair a_1) n), n < k + 1
⊢ n < k + 1
have comp : ∀ (a a_1 : Code) (h : x ∈ evaln (k + 1) (a.comp a_1) n), n < k + 1
Tactic: cases c
Cleared hypotheses: c, h
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
k : ℕ
c : Code
n x : ℕ
h : x ∈ evaln (k + 1) c n
this :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
zero : ∀ (h : x ∈ evaln (k + 1) Code.zero n), n < k + 1
succ : ∀ (h : x ∈ evaln (k + 1) Code.succ n), n < k + 1
left : ∀ (h : x ∈ evaln (k + 1) Code.left n), n < k + 1
right : ∀ (h : x ∈ evaln (k + 1) Code.right n), n < k + 1
pair : ∀ (a a_1 : Code) (h : x ∈ evaln (k + 1) (a.pair a_1) n), n < k + 1
comp : ∀ (a a_1 : Code) (h : x ∈ evaln (k + 1) (a.comp a_1) n), n < k + 1
⊢ n < k + 1
have prec : ∀ (a a_1 : Code) (h : x ∈ evaln (k + 1) (a.prec a_1) n), n < k + 1
Tactic: cases c
Cleared hypotheses: c, h
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
k : ℕ
c : Code
n x : ℕ
h : x ∈ evaln (k + 1) c n
this :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
zero : ∀ (h : x ∈ evaln (k + 1) Code.zero n), n < k + 1
succ : ∀ (h : x ∈ evaln (k + 1) Code.succ n), n < k + 1
left : ∀ (h : x ∈ evaln (k + 1) Code.left n), n < k + 1
right : ∀ (h : x ∈ evaln (k + 1) Code.right n), n < k + 1
pair : ∀ (a a_1 : Code) (h : x ∈ evaln (k + 1) (a.pair a_1) n), n < k + 1
comp : ∀ (a a_1 : Code) (h : x ∈ evaln (k + 1) (a.comp a_1) n), n < k + 1
prec : ∀ (a a_1 : Code) (h : x ∈ evaln (k + 1) (a.prec a_1) n), n < k + 1
⊢ n < k + 1
have rfind' : ∀ (a : Code) (h : x ∈ evaln (k + 1) a.rfind' n), n < k + 1
Tactic: cases c
Cleared hypotheses: c, h
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
Goal:
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
h : x ∈ evaln (k + 1) zero n
⊢ n < k + 1
have h₁ : Membership.mem (γ := Option ℕ)
  ((fun (n : ℕ) ↦
      (do
        guard (n ≤ k)
        pure 0 : Option ℕ))
    n)
  x
Tactic: rw [evaln] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
Goal:
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
h : x ∈ evaln (k + 1) succ n
⊢ n < k + 1
have h₁ : Membership.mem (γ := Option ℕ)
  ((fun (n : ℕ) ↦
      (do
        guard (n ≤ k)
        pure n.succ : Option ℕ))
    n)
  x
Tactic: rw [evaln] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
Goal:
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
h : x ∈ evaln (k + 1) left n
⊢ n < k + 1
have h₁ : Membership.mem (γ := Option ℕ)
  ((fun (n : ℕ) ↦
      (do
        guard (n ≤ k)
        pure (unpair n).1 : Option ℕ))
    n)
  x
Tactic: rw [evaln] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
Goal:
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
h : x ∈ evaln (k + 1) right n
⊢ n < k + 1
have h₁ : Membership.mem (γ := Option ℕ)
  ((fun (n : ℕ) ↦
      (do
        guard (n ≤ k)
        pure (unpair n).2 : Option ℕ))
    n)
  x
Tactic: rw [evaln] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
Goal:
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
a a_1 : Code
h : x ∈ evaln (k + 1) (a.pair a_1) n
⊢ n < k + 1
have h₁ : Membership.mem (γ := Option ℕ)
  ((fun (n : ℕ) ↦
      (do
        guard (n ≤ k)
        Nat.pair <$> evaln (k + 1) a n <*> evaln (k + 1) a_1 n : Option ℕ))
    n)
  x
Tactic: rw [evaln] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
Goal:
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
a a_1 : Code
h : x ∈ evaln (k + 1) (a.comp a_1) n
⊢ n < k + 1
have h₁ : Membership.mem (γ := Option ℕ)
  ((fun (n : ℕ) ↦
      (do
        guard (n ≤ k)
        let x ← evaln (k + 1) a_1 n
        evaln (k + 1) a x : Option ℕ))
    n)
  x
Tactic: rw [evaln] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
Goal:
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
a a_1 : Code
h : x ∈ evaln (k + 1) (a.prec a_1) n
⊢ n < k + 1
have h₁ : Membership.mem (γ := Option ℕ)
  ((fun (n : ℕ) ↦
      (do
        guard (n ≤ k)
        unpaired
            (fun (a_2 n : ℕ) ↦
              Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) n (evaln (k + 1) a a_2) fun (y : ℕ) ↦ do
                let i ← evaln k (a.prec a_1) (Nat.pair a_2 y)
                evaln (k + 1) a_1 (Nat.pair a_2 (Nat.pair y i)))
            n :
        Option ℕ))
    n)
  x
Tactic: rw [evaln] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
Goal:
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    Membership.mem (γ := Option ℕ)
        (do
          guard (n ≤ k)
          o)
        x →
      n < k + 1
a : Code
h : x ∈ evaln (k + 1) a.rfind' n
⊢ n < k + 1
have h₁ : Membership.mem (γ := Option ℕ)
  ((fun (n : ℕ) ↦
      (do
        guard (n ≤ k)
        unpaired
            (fun (a_1 m : ℕ) ↦ do
              let x ← evaln (k + 1) a (Nat.pair a_1 m)
              if x = 0 then pure m else evaln k a.rfind' (Nat.pair a_1 (m + 1)))
            n :
        Option ℕ))
    n)
  x
Tactic: rw [evaln] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
k : ℕ
c : Code
n x : ℕ
h : x ∈ evaln (k + 1) c n
⊢ n < k + 1
have suffices : ∀ {o : Option ℕ},
  Membership.mem (γ := Option ℕ)
      (do
        guard (n ≤ k)
        o)
      x →
    n < k + 1
Tactic: suffices ∀ {o : Option ℕ}, x ∈ do { guard (n ≤ k); o } → n < k + 1 by
      cases c <;> rw [evaln] at h <;> exact this h
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
Goal:
k k₂ : ℕ
c : Code
n x : ℕ
hl : k + 1 ≤ k₂ + 1
h : x ∈ evaln (k + 1) c n
⊢ x ∈ evaln (k₂ + 1) c n
have hl' : k ≤ k₂
Tactic: have hl' := Nat.le_of_succ_le_succ hl
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
k k₂ : ℕ
c : Code
n x : ℕ
hl : k + 1 ≤ k₂ + 1
h : x ∈ evaln (k + 1) c n
hl' : k ≤ k₂
⊢ ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        Membership.mem (γ := Option ℕ)
            (do
              guard (n ≤ k)
              o₁)
            x →
          Membership.mem (γ := Option ℕ)
            (do
              guard (n ≤ k₂)
              o₂)
            x
have simp : ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ}, k ≤ k₂ → (o₁ = some x → o₂ = some x) → n ≤ k → o₁ = some x → n ≤ k₂ ∧ o₂ = some x
Tactic: simp only [Option.mem_def, bind, Option.bind_eq_some_iff, Option.guard_eq_some',
        exists_and_left, exists_const, and_imp]
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
Goal:
k k₂ : ℕ
c : Code
n x : ℕ
hl : k + 1 ≤ k₂ + 1
h : x ∈ evaln (k + 1) c n
hl' : k ≤ k₂
⊢ x ∈ evaln (k₂ + 1) c n
have this : ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
  k ≤ k₂ →
    (x ∈ o₁ → x ∈ o₂) →
      Membership.mem (γ := Option ℕ)
          (do
            guard (n ≤ k)
            o₁)
          x →
        Membership.mem (γ := Option ℕ)
          (do
            guard (n ≤ k₂)
            o₂)
          x
Tactic: have :
      ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
        k ≤ k₂ → (x ∈ o₁ → x ∈ o₂) →
          x ∈ do { guard (n ≤ k); o₁ } → x ∈ do { guard (n ≤ k₂); o₂ } := by
      simp only [Option.mem_def, bind, Option.bind_eq_some_iff, Option.guard_eq_some',
        exists_and_left, exists_const, and_imp]
      introv h h₁ h₂ h₃
      exact ⟨le_trans h₂ h, h₁ h₃⟩
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
Goal:
k k₂ : ℕ
c : Code
n x : ℕ
hl : k + 1 ≤ k₂ + 1
h : x ∈ evaln (k + 1) c n
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        Membership.mem (γ := Option ℕ)
            (do
              guard (n ≤ k)
              o₁)
            x →
          Membership.mem (γ := Option ℕ)
            (do
              guard (n ≤ k₂)
              o₂)
            x
⊢ x ∈ evaln (k₂ + 1) c n
have h₁ : evaln (k + 1) c n = some x
Tactic: simp only [Option.mem_def] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
Goal:
k k₂ : ℕ
c : Code
n x : ℕ
hl : k + 1 ≤ k₂ + 1
h : x ∈ evaln (k + 1) c n
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        Membership.mem (γ := Option ℕ)
            (do
              guard (n ≤ k)
              o₁)
            x →
          Membership.mem (γ := Option ℕ)
            (do
              guard (n ≤ k₂)
              o₂)
            x
⊢ x ∈ evaln (k₂ + 1) c n
have h₁ : evaln (k + 1) c n = some x
Tactic: simp? at h ⊢ says simp only [Option.mem_def] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
k k₂ : ℕ
c : Code
n x : ℕ
hl : k + 1 ≤ k₂ + 1
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        Membership.mem (γ := Option ℕ)
            (do
              guard (n ≤ k)
              o₁)
            x →
          Membership.mem (γ := Option ℕ)
            (do
              guard (n ≤ k₂)
              o₂)
            x
h : evaln (k + 1) c n = some x
⊢ evaln (k₂ + 1) c n = some x
have zero : ∀ (n x : ℕ) (h : evaln (k + 1) zero n = some x), evaln (k₂ + 1) zero n = some x
Tactic: induction c generalizing x n
Cleared hypotheses: c, n, x, h
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
k k₂ : ℕ
c : Code
n x : ℕ
hl : k + 1 ≤ k₂ + 1
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        Membership.mem (γ := Option ℕ)
            (do
              guard (n ≤ k)
              o₁)
            x →
          Membership.mem (γ := Option ℕ)
            (do
              guard (n ≤ k₂)
              o₂)
            x
h : evaln (k + 1) c n = some x
zero : ∀ (n x : ℕ) (h : evaln (k + 1) Code.zero n = some x), evaln (k₂ + 1) Code.zero n = some x
⊢ evaln (k₂ + 1) c n = some x
have succ : ∀ (n x : ℕ) (h : evaln (k + 1) succ n = some x), evaln (k₂ + 1) succ n = some x
Tactic: induction c generalizing x n
Cleared hypotheses: c, n, x, h
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
k k₂ : ℕ
c : Code
n x : ℕ
hl : k + 1 ≤ k₂ + 1
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        Membership.mem (γ := Option ℕ)
            (do
              guard (n ≤ k)
              o₁)
            x →
          Membership.mem (γ := Option ℕ)
            (do
              guard (n ≤ k₂)
              o₂)
            x
h : evaln (k + 1) c n = some x
zero : ∀ (n x : ℕ) (h : evaln (k + 1) Code.zero n = some x), evaln (k₂ + 1) Code.zero n = some x
succ : ∀ (n x : ℕ) (h : evaln (k + 1) Code.succ n = some x), evaln (k₂ + 1) Code.succ n = some x
⊢ evaln (k₂ + 1) c n = some x
have left : ∀ (n x : ℕ) (h : evaln (k + 1) left n = some x), evaln (k₂ + 1) left n = some x
Tactic: induction c generalizing x n
Cleared hypotheses: c, n, x, h
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
k k₂ : ℕ
c : Code
n x : ℕ
hl : k + 1 ≤ k₂ + 1
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        Membership.mem (γ := Option ℕ)
            (do
              guard (n ≤ k)
              o₁)
            x →
          Membership.mem (γ := Option ℕ)
            (do
              guard (n ≤ k₂)
              o₂)
            x
h : evaln (k + 1) c n = some x
zero : ∀ (n x : ℕ) (h : evaln (k + 1) Code.zero n = some x), evaln (k₂ + 1) Code.zero n = some x
succ : ∀ (n x : ℕ) (h : evaln (k + 1) Code.succ n = some x), evaln (k₂ + 1) Code.succ n = some x
left : ∀ (n x : ℕ) (h : evaln (k + 1) Code.left n = some x), evaln (k₂ + 1) Code.left n = some x
⊢ evaln (k₂ + 1) c n = some x
have right : ∀ (n x : ℕ) (h : evaln (k + 1) right n = some x), evaln (k₂ + 1) right n = some x
Tactic: induction c generalizing x n
Cleared hypotheses: c, n, x, h