awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.PartrecCode
Goal:
k k₂ : ℕ
c : Code
n x : ℕ
hl : k + 1 ≤ k₂ + 1
h : x ∈ evaln (k + 1) c n
hl' : k ≤ k₂
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
⊢ ∀ {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:
simp only [Option.mem_def, bind, Option.bind_eq_some_iff, Option.guard_eq_some',
        exists_and_left, exists_const, and_imp]

Premises used: and_imp, exists_and_left, Option.guard_eq_some', exists_const, Bind.bind, Option.bind_eq_some_iff, Option.mem_def
-- Module: Mathlib.Computability.PartrecCode
Goal:
k_1 k₂_1 : ℕ
c : Code
n_1 x_1 : ℕ
hl : k_1 + 1 ≤ k₂_1 + 1
h_1 : x_1 ∈ evaln (k_1 + 1) c n_1
hl' : k_1 ≤ k₂_1
k k₂ n x : ℕ
o₁ o₂ : Option ℕ
h : k ≤ k₂
h₁ : o₁ = some x → o₂ = some x
h₂ : n ≤ k
h₃ : o₁ = some x
⊢ n ≤ k₂ ∧ o₂ = some x

Tactic:
⟨le_trans h₂ h, h₁ h₃⟩

Premises used: And.intro, le_trans
-- Module: Mathlib.Computability.PartrecCode
Goal:
k_1 k₂_1 : ℕ
c : Code
n_1 x_1 : ℕ
hl : k_1 + 1 ≤ k₂_1 + 1
h_1 : x_1 ∈ evaln (k_1 + 1) c n_1
hl' : k_1 ≤ k₂_1
k k₂ n x : ℕ
o₁ o₂ : Option ℕ
h : k ≤ k₂
h₁ : o₁ = some x → o₂ = some x
h₂ : n ≤ k
h₃ : o₁ = some x
⊢ n ≤ k₂ ∧ o₂ = some x

Tactic:
exact ⟨le_trans h₂ h, h₁ h₃⟩
-- Module: Mathlib.Computability.PartrecCode
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

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₃⟩
-- Module: Mathlib.Computability.PartrecCode
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
⊢ evaln (k + 1) c n = some x

Tactic:
simp only [Option.mem_def] at h ⊢

Premises used: Option.mem_def
-- Module: Mathlib.Computability.PartrecCode
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
⊢ evaln (k + 1) c n = some x

Tactic:
simp? at h ⊢ says simp only [Option.mem_def] at h ⊢

Premises used: Option.mem_def
-- Module: Mathlib.Computability.PartrecCode
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
right : ∀ (n x : ℕ) (h : evaln (k + 1) Code.right n = some x), evaln (k₂ + 1) Code.right n = some x
pair :
  ∀ (a a_1 : Code),
    (∀ (n x : ℕ) (h : evaln (k + 1) a n = some x), evaln (k₂ + 1) a n = some x) →
      (∀ (n x : ℕ) (h : evaln (k + 1) a_1 n = some x), evaln (k₂ + 1) a_1 n = some x) →
        ∀ (n x : ℕ) (h : evaln (k + 1) (a.pair a_1) n = some x), evaln (k₂ + 1) (a.pair a_1) n = some x
comp :
  ∀ (a a_1 : Code),
    (∀ (n x : ℕ) (h : evaln (k + 1) a n = some x), evaln (k₂ + 1) a n = some x) →
      (∀ (n x : ℕ) (h : evaln (k + 1) a_1 n = some x), evaln (k₂ + 1) a_1 n = some x) →
        ∀ (n x : ℕ) (h : evaln (k + 1) (a.comp a_1) n = some x), evaln (k₂ + 1) (a.comp a_1) n = some x
prec :
  ∀ (a a_1 : Code),
    (∀ (n x : ℕ) (h : evaln (k + 1) a n = some x), evaln (k₂ + 1) a n = some x) →
      (∀ (n x : ℕ) (h : evaln (k + 1) a_1 n = some x), evaln (k₂ + 1) a_1 n = some x) →
        ∀ (n x : ℕ) (h : evaln (k + 1) (a.prec a_1) n = some x), evaln (k₂ + 1) (a.prec a_1) n = some x
rfind' :
  ∀ (a : Code),
    (∀ (n x : ℕ) (h : evaln (k + 1) a n = some x), evaln (k₂ + 1) a n = some x) →
      ∀ (n x : ℕ) (h : evaln (k + 1) a.rfind' n = some x), evaln (k₂ + 1) a.rfind' n = some x
⊢ evaln (k₂ + 1) c n = some x

Tactic:
induction c generalizing x n
-- Module: Mathlib.Computability.PartrecCode
Goal:
k k₂ : ℕ
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
n x : ℕ
h : evaln (k + 1) Code.zero n = some x
zero :
  ∀
    (h :
      (fun (n : ℕ) ↦
            (do
              guard (n ≤ k)
              pure 0 : Option ℕ))
          n =
        some x),
    (fun (n : ℕ) ↦
          (do
            guard (n ≤ k₂)
            pure 0 : Option ℕ))
        n =
      some x
⊢ evaln (k₂ + 1) Code.zero n = some x

Tactic:
rw [evaln] at h ⊢

Premises used: Nat.Partrec.Code.evaln
-- Module: Mathlib.Computability.PartrecCode
Goal:
k k₂ : ℕ
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
n x : ℕ
h : evaln (k + 1) Code.succ n = some x
succ :
  ∀
    (h :
      (fun (n : ℕ) ↦
            (do
              guard (n ≤ k)
              pure n.succ : Option ℕ))
          n =
        some x),
    (fun (n : ℕ) ↦
          (do
            guard (n ≤ k₂)
            pure n.succ : Option ℕ))
        n =
      some x
⊢ evaln (k₂ + 1) Code.succ n = some x

Tactic:
rw [evaln] at h ⊢

Premises used: Nat.Partrec.Code.evaln
-- Module: Mathlib.Computability.PartrecCode
Goal:
k k₂ : ℕ
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
n x : ℕ
h : evaln (k + 1) Code.left n = some x
left :
  ∀
    (h :
      (fun (n : ℕ) ↦
            (do
              guard (n ≤ k)
              pure (unpair n).1 : Option ℕ))
          n =
        some x),
    (fun (n : ℕ) ↦
          (do
            guard (n ≤ k₂)
            pure (unpair n).1 : Option ℕ))
        n =
      some x
⊢ evaln (k₂ + 1) Code.left n = some x

Tactic:
rw [evaln] at h ⊢

Premises used: Nat.Partrec.Code.evaln
-- Module: Mathlib.Computability.PartrecCode
Goal:
k k₂ : ℕ
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
n x : ℕ
h : evaln (k + 1) Code.right n = some x
right :
  ∀
    (h :
      (fun (n : ℕ) ↦
            (do
              guard (n ≤ k)
              pure (unpair n).2 : Option ℕ))
          n =
        some x),
    (fun (n : ℕ) ↦
          (do
            guard (n ≤ k₂)
            pure (unpair n).2 : Option ℕ))
        n =
      some x
⊢ evaln (k₂ + 1) Code.right n = some x

Tactic:
rw [evaln] at h ⊢

Premises used: Nat.Partrec.Code.evaln
-- Module: Mathlib.Computability.PartrecCode
Goal:
k k₂ : ℕ
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
a a_1 : Code
a_ih : ∀ (n x : ℕ) (h : evaln (k + 1) a n = some x), evaln (k₂ + 1) a n = some x
a_ih_1 : ∀ (n x : ℕ) (h : evaln (k + 1) a_1 n = some x), evaln (k₂ + 1) a_1 n = some x
n x : ℕ
h : evaln (k + 1) (a.pair a_1) n = some x
pair :
  ∀
    (h :
      (fun (n : ℕ) ↦
            (do
              guard (n ≤ k)
              Nat.pair <$> evaln (k + 1) a n <*> evaln (k + 1) a_1 n : Option ℕ))
          n =
        some x),
    (fun (n : ℕ) ↦
          (do
            guard (n ≤ k₂)
            Nat.pair <$> evaln (k₂ + 1) a n <*> evaln (k₂ + 1) a_1 n : Option ℕ))
        n =
      some x
⊢ evaln (k₂ + 1) (a.pair a_1) n = some x

Tactic:
rw [evaln] at h ⊢

Premises used: Nat.Partrec.Code.evaln
-- Module: Mathlib.Computability.PartrecCode
Goal:
k k₂ : ℕ
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
a a_1 : Code
a_ih : ∀ (n x : ℕ) (h : evaln (k + 1) a n = some x), evaln (k₂ + 1) a n = some x
a_ih_1 : ∀ (n x : ℕ) (h : evaln (k + 1) a_1 n = some x), evaln (k₂ + 1) a_1 n = some x
n x : ℕ
h : evaln (k + 1) (a.comp a_1) n = some x
comp :
  ∀
    (h :
      (fun (n : ℕ) ↦
            (do
              guard (n ≤ k)
              let x ← evaln (k + 1) a_1 n
              evaln (k + 1) a x : Option ℕ))
          n =
        some x),
    (fun (n : ℕ) ↦
          (do
            guard (n ≤ k₂)
            let x ← evaln (k₂ + 1) a_1 n
            evaln (k₂ + 1) a x : Option ℕ))
        n =
      some x
⊢ evaln (k₂ + 1) (a.comp a_1) n = some x

Tactic:
rw [evaln] at h ⊢

Premises used: Nat.Partrec.Code.evaln
-- Module: Mathlib.Computability.PartrecCode
Goal:
k k₂ : ℕ
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
a a_1 : Code
a_ih : ∀ (n x : ℕ) (h : evaln (k + 1) a n = some x), evaln (k₂ + 1) a n = some x
a_ih_1 : ∀ (n x : ℕ) (h : evaln (k + 1) a_1 n = some x), evaln (k₂ + 1) a_1 n = some x
n x : ℕ
h : evaln (k + 1) (a.prec a_1) n = some x
prec :
  ∀
    (h :
      (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 =
        some x),
    (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 =
      some x
⊢ evaln (k₂ + 1) (a.prec a_1) n = some x

Tactic:
rw [evaln] at h ⊢

Premises used: Nat.Partrec.Code.evaln
-- Module: Mathlib.Computability.PartrecCode
Goal:
k k₂ : ℕ
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
a : Code
a_ih : ∀ (n x : ℕ) (h : evaln (k + 1) a n = some x), evaln (k₂ + 1) a n = some x
n x : ℕ
h : evaln (k + 1) a.rfind' n = some x
rfind' :
  ∀
    (h :
      (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 =
        some x),
    (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 =
      some x
⊢ evaln (k₂ + 1) a.rfind' n = some x

Tactic:
rw [evaln] at h ⊢

Premises used: Nat.Partrec.Code.evaln
-- Module: Mathlib.Computability.PartrecCode
Goal:
k k₂ : ℕ
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
n x : ℕ
h :
  (fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          pure 0 : Option ℕ))
      n =
    some x
⊢ (fun (n : ℕ) ↦
        (do
          guard (n ≤ k₂)
          pure 0 : Option ℕ))
      n =
    some x

Tactic:
this hl' (fun h => ?_) h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k k₂ : ℕ
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
n x : ℕ
h :
  (fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          pure 0 : Option ℕ))
      n =
    some x
zero : ∀ (h : Membership.mem (γ := Option ℕ) (pure 0) x), Membership.mem (γ := Option ℕ) (pure 0) x
⊢ (fun (n : ℕ) ↦
        (do
          guard (n ≤ k₂)
          pure 0 : Option ℕ))
      n =
    some x

Tactic:
refine this hl' (fun h => ?_) h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k k₂ : ℕ
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
n x : ℕ
h :
  (fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          pure n.succ : Option ℕ))
      n =
    some x
⊢ (fun (n : ℕ) ↦
        (do
          guard (n ≤ k₂)
          pure n.succ : Option ℕ))
      n =
    some x

Tactic:
this hl' (fun h => ?_) h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k k₂ : ℕ
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
n x : ℕ
h :
  (fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          pure n.succ : Option ℕ))
      n =
    some x
succ : ∀ (h : Membership.mem (γ := Option ℕ) (pure n.succ) x), Membership.mem (γ := Option ℕ) (pure n.succ) x
⊢ (fun (n : ℕ) ↦
        (do
          guard (n ≤ k₂)
          pure n.succ : Option ℕ))
      n =
    some x

Tactic:
refine this hl' (fun h => ?_) h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k k₂ : ℕ
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
n x : ℕ
h :
  (fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          pure (unpair n).1 : Option ℕ))
      n =
    some x
⊢ (fun (n : ℕ) ↦
        (do
          guard (n ≤ k₂)
          pure (unpair n).1 : Option ℕ))
      n =
    some x

Tactic:
this hl' (fun h => ?_) h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k k₂ : ℕ
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
n x : ℕ
h :
  (fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          pure (unpair n).1 : Option ℕ))
      n =
    some x
left :
  ∀ (h : Membership.mem (γ := Option ℕ) (pure (unpair n).1) x), Membership.mem (γ := Option ℕ) (pure (unpair n).1) x
⊢ (fun (n : ℕ) ↦
        (do
          guard (n ≤ k₂)
          pure (unpair n).1 : Option ℕ))
      n =
    some x

Tactic:
refine this hl' (fun h => ?_) h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k k₂ : ℕ
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
n x : ℕ
h :
  (fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          pure (unpair n).2 : Option ℕ))
      n =
    some x
⊢ (fun (n : ℕ) ↦
        (do
          guard (n ≤ k₂)
          pure (unpair n).2 : Option ℕ))
      n =
    some x

Tactic:
this hl' (fun h => ?_) h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k k₂ : ℕ
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
n x : ℕ
h :
  (fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          pure (unpair n).2 : Option ℕ))
      n =
    some x
right :
  ∀ (h : Membership.mem (γ := Option ℕ) (pure (unpair n).2) x), Membership.mem (γ := Option ℕ) (pure (unpair n).2) x
⊢ (fun (n : ℕ) ↦
        (do
          guard (n ≤ k₂)
          pure (unpair n).2 : Option ℕ))
      n =
    some x

Tactic:
refine this hl' (fun h => ?_) h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k k₂ : ℕ
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
a a_1 : Code
a_ih : ∀ (n x : ℕ) (h : evaln (k + 1) a n = some x), evaln (k₂ + 1) a n = some x
a_ih_1 : ∀ (n x : ℕ) (h : evaln (k + 1) a_1 n = some x), evaln (k₂ + 1) a_1 n = some x
n x : ℕ
h :
  (fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          Nat.pair <$> evaln (k + 1) a n <*> evaln (k + 1) a_1 n : Option ℕ))
      n =
    some x
⊢ (fun (n : ℕ) ↦
        (do
          guard (n ≤ k₂)
          Nat.pair <$> evaln (k₂ + 1) a n <*> evaln (k₂ + 1) a_1 n : Option ℕ))
      n =
    some x

Tactic:
this hl' (fun h => ?_) h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k k₂ : ℕ
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
a a_1 : Code
a_ih : ∀ (n x : ℕ) (h : evaln (k + 1) a n = some x), evaln (k₂ + 1) a n = some x
a_ih_1 : ∀ (n x : ℕ) (h : evaln (k + 1) a_1 n = some x), evaln (k₂ + 1) a_1 n = some x
n x : ℕ
h :
  (fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          Nat.pair <$> evaln (k + 1) a n <*> evaln (k + 1) a_1 n : Option ℕ))
      n =
    some x
pair :
  ∀ (h : x ∈ Nat.pair <$> evaln (k + 1) a n <*> evaln (k + 1) a_1 n),
    x ∈ Nat.pair <$> evaln (k₂ + 1) a n <*> evaln (k₂ + 1) a_1 n
⊢ (fun (n : ℕ) ↦
        (do
          guard (n ≤ k₂)
          Nat.pair <$> evaln (k₂ + 1) a n <*> evaln (k₂ + 1) a_1 n : Option ℕ))
      n =
    some x

Tactic:
refine this hl' (fun h => ?_) h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k k₂ : ℕ
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
a a_1 : Code
a_ih : ∀ (n x : ℕ) (h : evaln (k + 1) a n = some x), evaln (k₂ + 1) a n = some x
a_ih_1 : ∀ (n x : ℕ) (h : evaln (k + 1) a_1 n = some x), evaln (k₂ + 1) a_1 n = some x
n x : ℕ
h :
  (fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          let x ← evaln (k + 1) a_1 n
          evaln (k + 1) a x : Option ℕ))
      n =
    some x
⊢ (fun (n : ℕ) ↦
        (do
          guard (n ≤ k₂)
          let x ← evaln (k₂ + 1) a_1 n
          evaln (k₂ + 1) a x : Option ℕ))
      n =
    some x

Tactic:
this hl' (fun h => ?_) h
-- Module: Mathlib.Computability.PartrecCode
Goal:
k k₂ : ℕ
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
a a_1 : Code
a_ih : ∀ (n x : ℕ) (h : evaln (k + 1) a n = some x), evaln (k₂ + 1) a n = some x
a_ih_1 : ∀ (n x : ℕ) (h : evaln (k + 1) a_1 n = some x), evaln (k₂ + 1) a_1 n = some x
n x : ℕ
h :
  (fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          let x ← evaln (k + 1) a_1 n
          evaln (k + 1) a x : Option ℕ))
      n =
    some x
comp :
  ∀
    (h :
      Membership.mem (γ := Option ℕ)
        (do
          let x ← evaln (k + 1) a_1 n
          evaln (k + 1) a x)
        x),
    Membership.mem (γ := Option ℕ)
      (do
        let x ← evaln (k₂ + 1) a_1 n
        evaln (k₂ + 1) a x)
      x
⊢ (fun (n : ℕ) ↦
        (do
          guard (n ≤ k₂)
          let x ← evaln (k₂ + 1) a_1 n
          evaln (k₂ + 1) a x : Option ℕ))
      n =
    some x

Tactic:
refine this hl' (fun h => ?_) h