awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
cf cg : Code
hf : ∀ (n x : ℕ) (h : evaln (k + 1) cf n = some x), evaln (k₂ + 1) cf n = some x
hg : ∀ (n x : ℕ) (h : evaln (k + 1) cg n = some x), evaln (k₂ + 1) cg n = some x
n x : ℕ
h_1 :
  (fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          unpaired
              (fun (a n : ℕ) ↦
                Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) n (evaln (k + 1) cf a) fun (y : ℕ) ↦ do
                  let i ← evaln k (cf.prec cg) (Nat.pair a y)
                  evaln (k + 1) cg (Nat.pair a (Nat.pair y i)))
              n :
          Option ℕ))
      n =
    some x
h :
  Membership.mem (γ := Option ℕ)
    (unpaired
      (fun (a n : ℕ) ↦
        Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) n (evaln (k + 1) cf a) fun (y : ℕ) ↦ do
          let i ← evaln k (cf.prec cg) (Nat.pair a y)
          evaln (k + 1) cg (Nat.pair a (Nat.pair y i)))
      n)
    x
revert :
  ∀
    (h :
      Membership.mem (γ := Option ℕ)
        (unpaired
          (fun (a n : ℕ) ↦
            Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) n (evaln (k + 1) cf a) fun (y : ℕ) ↦ do
              let i ← evaln k (cf.prec cg) (Nat.pair a y)
              evaln (k + 1) cg (Nat.pair a (Nat.pair y i)))
          n)
        x),
    Membership.mem (γ := Option ℕ)
      (unpaired
        (fun (a n : ℕ) ↦
          Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) n (evaln (k₂ + 1) cf a) fun (y : ℕ) ↦ do
            let i ← evaln k₂ (cf.prec cg) (Nat.pair a y)
            evaln (k₂ + 1) cg (Nat.pair a (Nat.pair y i)))
        n)
      x
⊢ Membership.mem (γ := Option ℕ)
    (unpaired
      (fun (a n : ℕ) ↦
        Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) n (evaln (k₂ + 1) cf a) fun (y : ℕ) ↦ do
          let i ← evaln k₂ (cf.prec cg) (Nat.pair a y)
          evaln (k₂ + 1) cg (Nat.pair a (Nat.pair y i)))
      n)
    x

Tactic:
revert 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
cf cg : Code
hf : ∀ (n x : ℕ) (h : evaln (k + 1) cf n = some x), evaln (k₂ + 1) cf n = some x
hg : ∀ (n x : ℕ) (h : evaln (k + 1) cg n = some x), evaln (k₂ + 1) cg n = some x
n x : ℕ
h :
  (fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          unpaired
              (fun (a n : ℕ) ↦
                Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) n (evaln (k + 1) cf a) fun (y : ℕ) ↦ do
                  let i ← evaln k (cf.prec cg) (Nat.pair a y)
                  evaln (k + 1) cg (Nat.pair a (Nat.pair y i)))
              n :
          Option ℕ))
      n =
    some x
simp :
  ∀
    (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),
    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
⊢ ∀
    (h :
      Membership.mem (γ := Option ℕ)
        (unpaired
          (fun (a n : ℕ) ↦
            Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) n (evaln (k + 1) cf a) fun (y : ℕ) ↦ do
              let i ← evaln k (cf.prec cg) (Nat.pair a y)
              evaln (k + 1) cg (Nat.pair a (Nat.pair y i)))
          n)
        x),
    Membership.mem (γ := Option ℕ)
      (unpaired
        (fun (a n : ℕ) ↦
          Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) n (evaln (k₂ + 1) cf a) fun (y : ℕ) ↦ do
            let i ← evaln k₂ (cf.prec cg) (Nat.pair a y)
            evaln (k₂ + 1) cg (Nat.pair a (Nat.pair y i)))
        n)
      x

Tactic:
simp only [unpaired, bind, Option.mem_def]

Premises used: Nat.unpaired, Bind.bind, Option.mem_def
-- 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
cf cg : Code
hf : ∀ (n x : ℕ) (h : evaln (k + 1) cf n = some x), evaln (k₂ + 1) cf n = some x
hg : ∀ (n x : ℕ) (h : evaln (k + 1) cg n = some x), evaln (k₂ + 1) cg n = some x
n x : ℕ
h :
  (fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          unpaired
              (fun (a n : ℕ) ↦
                Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) n (evaln (k + 1) cf a) fun (y : ℕ) ↦ do
                  let i ← evaln k (cf.prec cg) (Nat.pair a y)
                  evaln (k + 1) cg (Nat.pair a (Nat.pair y i)))
              n :
          Option ℕ))
      n =
    some x
n_1 : ℕ
h_1 :
  ∀
    (h :
      Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) cf (unpair n).1)
          (fun (n_2 : ℕ) (n_ih : Option ℕ) ↦
            (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_2)).bind fun (i : ℕ) ↦
              evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_2 i)))
          n_1 =
        some x),
    Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k₂ + 1) cf (unpair n).1)
        (fun (n_2 : ℕ) (n_ih : Option ℕ) ↦
          (evaln k₂ (cf.prec cg) (Nat.pair (unpair n).1 n_2)).bind fun (i : ℕ) ↦
            evaln (k₂ + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_2 i)))
        n_1 =
      some x
succ :
  ∀ (x_1 : ℕ),
    evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_1) = some x_1 →
      evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 x_1)) = some x →
        ∃ (a : ℕ),
          evaln k₂ (cf.prec cg) (Nat.pair (unpair n).1 n_1) = some a ∧
            evaln (k₂ + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 a)) = some x
⊢ ∀
    (h :
      Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) cf (unpair n).1)
          (fun (n_2 : ℕ) (n_ih : Option ℕ) ↦
            (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_2)).bind fun (i : ℕ) ↦
              evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_2 i)))
          (n_1 + 1) =
        some x),
    Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k₂ + 1) cf (unpair n).1)
        (fun (n_2 : ℕ) (n_ih : Option ℕ) ↦
          (evaln k₂ (cf.prec cg) (Nat.pair (unpair n).1 n_2)).bind fun (i : ℕ) ↦
            evaln (k₂ + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_2 i)))
        (n_1 + 1) =
      some x

Tactic:
simp [Option.bind_eq_some_iff]

Premises used: Option.bind_eq_some_iff
-- 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
cf cg : Code
hf : ∀ (n x : ℕ) (h : evaln (k + 1) cf n = some x), evaln (k₂ + 1) cf n = some x
hg : ∀ (n x : ℕ) (h : evaln (k + 1) cg n = some x), evaln (k₂ + 1) cg n = some x
n x : ℕ
h :
  (fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          unpaired
              (fun (a n : ℕ) ↦
                Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) n (evaln (k + 1) cf a) fun (y : ℕ) ↦ do
                  let i ← evaln k (cf.prec cg) (Nat.pair a y)
                  evaln (k + 1) cg (Nat.pair a (Nat.pair y i)))
              n :
          Option ℕ))
      n =
    some x
⊢ ∀ (h : evaln (k + 1) cf (unpair n).1 = some x), evaln (k₂ + 1) cf (unpair n).1 = some x

Tactic:
apply hf
-- 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
cf cg : Code
hf : ∀ (n x : ℕ) (h : evaln (k + 1) cf n = some x), evaln (k₂ + 1) cf n = some x
hg : ∀ (n x : ℕ) (h : evaln (k + 1) cg n = some x), evaln (k₂ + 1) cg n = some x
n x : ℕ
h :
  (fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          unpaired
              (fun (a n : ℕ) ↦
                Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) n (evaln (k + 1) cf a) fun (y : ℕ) ↦ do
                  let i ← evaln k (cf.prec cg) (Nat.pair a y)
                  evaln (k + 1) cg (Nat.pair a (Nat.pair y i)))
              n :
          Option ℕ))
      n =
    some x
n_1 : ℕ
h_1 :
  ∀
    (h :
      Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) cf (unpair n).1)
          (fun (n_2 : ℕ) (n_ih : Option ℕ) ↦
            (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_2)).bind fun (i : ℕ) ↦
              evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_2 i)))
          n_1 =
        some x),
    Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k₂ + 1) cf (unpair n).1)
        (fun (n_2 : ℕ) (n_ih : Option ℕ) ↦
          (evaln k₂ (cf.prec cg) (Nat.pair (unpair n).1 n_2)).bind fun (i : ℕ) ↦
            evaln (k₂ + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_2 i)))
        n_1 =
      some x
⊢ ∀ (x_1 : ℕ),
    evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_1) = some x_1 →
      evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 x_1)) = some x →
        ∃ (a : ℕ),
          evaln k₂ (cf.prec cg) (Nat.pair (unpair n).1 n_1) = some a ∧
            evaln (k₂ + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 a)) = some x

Tactic:
fun y h₁ h₂ => ⟨y, evaln_mono hl' h₁, hg _ _ h₂⟩

Premises used: Nat.unpair, Prod.fst, Nat.pair, And.intro, Exists.intro
-- 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
cf cg : Code
hf : ∀ (n x : ℕ) (h : evaln (k + 1) cf n = some x), evaln (k₂ + 1) cf n = some x
hg : ∀ (n x : ℕ) (h : evaln (k + 1) cg n = some x), evaln (k₂ + 1) cg n = some x
n x : ℕ
h :
  (fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          unpaired
              (fun (a n : ℕ) ↦
                Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) n (evaln (k + 1) cf a) fun (y : ℕ) ↦ do
                  let i ← evaln k (cf.prec cg) (Nat.pair a y)
                  evaln (k + 1) cg (Nat.pair a (Nat.pair y i)))
              n :
          Option ℕ))
      n =
    some x
n_1 : ℕ
h_1 :
  ∀
    (h :
      Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) cf (unpair n).1)
          (fun (n_2 : ℕ) (n_ih : Option ℕ) ↦
            (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_2)).bind fun (i : ℕ) ↦
              evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_2 i)))
          n_1 =
        some x),
    Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k₂ + 1) cf (unpair n).1)
        (fun (n_2 : ℕ) (n_ih : Option ℕ) ↦
          (evaln k₂ (cf.prec cg) (Nat.pair (unpair n).1 n_2)).bind fun (i : ℕ) ↦
            evaln (k₂ + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_2 i)))
        n_1 =
      some x
⊢ ∀ (x_1 : ℕ),
    evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_1) = some x_1 →
      evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 x_1)) = some x →
        ∃ (a : ℕ),
          evaln k₂ (cf.prec cg) (Nat.pair (unpair n).1 n_1) = some a ∧
            evaln (k₂ + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 a)) = some x

Tactic:
exact fun y h₁ h₂ => ⟨y, evaln_mono hl' h₁, hg _ _ 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_1 :
  (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
h :
  Membership.mem (γ := Option ℕ)
    (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)
    x
⊢ Membership.mem (γ := Option ℕ)
    (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)
    x

Tactic:
case prec cf cg hf hg _ =>
      revert h
      simp only [unpaired, bind, Option.mem_def]
      induction n.unpair.2 <;> simp [Option.bind_eq_some_iff]
      · apply hf
      · exact fun y h₁ h₂ => ⟨y, evaln_mono hl' h₁, hg _ _ h₂⟩

Premises used: Nat.unpair, Nat.Partrec.Code.prec, Nat.unpaired, Bind.bind, Option.bind_eq_some_iff, Prod.snd, Option.mem_def
-- 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
cf : Code
hf : ∀ (n x : ℕ) (h : evaln (k + 1) cf n = some x), evaln (k₂ + 1) cf n = some x
n x : ℕ
h_1 :
  (fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          unpaired
              (fun (a m : ℕ) ↦ do
                let x ← evaln (k + 1) cf (Nat.pair a m)
                if x = 0 then pure m else evaln k cf.rfind' (Nat.pair a (m + 1)))
              n :
          Option ℕ))
      n =
    some x
h :
  Membership.mem (γ := Option ℕ)
    (unpaired
      (fun (a m : ℕ) ↦ do
        let x ← evaln (k + 1) cf (Nat.pair a m)
        if x = 0 then pure m else evaln k cf.rfind' (Nat.pair a (m + 1)))
      n)
    x
simp :
  ∀
    (h :
      ∃ (a : ℕ),
        evaln (k + 1) cf n = some a ∧
          (if a = 0 then some (unpair n).2 else evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x),
    ∃ (a : ℕ),
      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
⊢ Membership.mem (γ := Option ℕ)
    (unpaired
      (fun (a m : ℕ) ↦ do
        let x ← evaln (k₂ + 1) cf (Nat.pair a m)
        if x = 0 then pure m else evaln k₂ cf.rfind' (Nat.pair a (m + 1)))
      n)
    x

Tactic:
simp only [unpaired, bind, pair_unpair, Option.pure_def, Option.mem_def,
          Option.bind_eq_some_iff] at h ⊢

Premises used: Nat.unpaired, Nat.pair_unpair, Bind.bind, Option.bind_eq_some_iff, Option.pure_def, Option.mem_def
-- 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
cf : Code
hf : ∀ (n x : ℕ) (h : evaln (k + 1) cf n = some x), evaln (k₂ + 1) cf n = some x
n x : ℕ
h_1 :
  (fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          unpaired
              (fun (a m : ℕ) ↦ do
                let x ← evaln (k + 1) cf (Nat.pair a m)
                if x = 0 then pure m else evaln k cf.rfind' (Nat.pair a (m + 1)))
              n :
          Option ℕ))
      n =
    some x
h :
  Membership.mem (γ := Option ℕ)
    (unpaired
      (fun (a m : ℕ) ↦ do
        let x ← evaln (k + 1) cf (Nat.pair a m)
        if x = 0 then pure m else evaln k cf.rfind' (Nat.pair a (m + 1)))
      n)
    x
simp? :
  ∀
    (h :
      ∃ (a : ℕ),
        evaln (k + 1) cf n = some a ∧
          (if a = 0 then some (unpair n).2 else evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x),
    ∃ (a : ℕ),
      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
⊢ Membership.mem (γ := Option ℕ)
    (unpaired
      (fun (a m : ℕ) ↦ do
        let x ← evaln (k₂ + 1) cf (Nat.pair a m)
        if x = 0 then pure m else evaln k₂ cf.rfind' (Nat.pair a (m + 1)))
      n)
    x

Tactic:
simp? [Bind.bind, Option.bind_eq_some_iff] at h ⊢ says
        simp only [unpaired, bind, pair_unpair, Option.pure_def, Option.mem_def,
          Option.bind_eq_some_iff] at h ⊢

Premises used: Nat.unpaired, Nat.pair_unpair, Bind.bind, Option.bind_eq_some_iff, Option.pure_def, Option.mem_def
-- 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
cf : Code
hf : ∀ (n x : ℕ) (h : evaln (k + 1) cf n = some x), evaln (k₂ + 1) cf n = some x
n x : ℕ
h_1 :
  (fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          unpaired
              (fun (a m : ℕ) ↦ do
                let x ← evaln (k + 1) cf (Nat.pair a m)
                if x = 0 then pure m else evaln k cf.rfind' (Nat.pair a (m + 1)))
              n :
          Option ℕ))
      n =
    some x
h :
  ∃ (a : ℕ),
    evaln (k + 1) cf n = some a ∧
      (if a = 0 then some (unpair n).2 else evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x
⊢ ∃ (a : ℕ),
    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:
h.imp fun x => And.imp (hf _ _) ?_

Premises used: And.imp, Exists.imp
-- 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
cf : Code
hf : ∀ (n x : ℕ) (h : evaln (k + 1) cf n = some x), evaln (k₂ + 1) cf n = some x
n x : ℕ
h_1 :
  (fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          unpaired
              (fun (a m : ℕ) ↦ do
                let x ← evaln (k + 1) cf (Nat.pair a m)
                if x = 0 then pure m else evaln k cf.rfind' (Nat.pair a (m + 1)))
              n :
          Option ℕ))
      n =
    some x
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
refine :
  ∀ (x_1 : ℕ),
    (if x_1 = 0 then some (unpair n).2 else evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x →
      (if x_1 = 0 then some (unpair n).2 else evaln k₂ cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x
⊢ ∃ (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:
refine h.imp fun x => And.imp (hf _ _) ?_

Premises used: And.imp, Exists.imp
-- 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
cf : Code
hf : ∀ (n x : ℕ) (h : evaln (k + 1) cf n = some x), evaln (k₂ + 1) cf n = some x
n x_1 : ℕ
h_1 :
  (fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          unpaired
              (fun (a m : ℕ) ↦ do
                let x ← evaln (k + 1) cf (Nat.pair a m)
                if x = 0 then pure m else evaln k cf.rfind' (Nat.pair a (m + 1)))
              n :
          Option ℕ))
      n =
    some x_1
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_1
x : ℕ
pos :
  ∀ (x0 : x = 0),
    (if x = 0 then some (unpair n).2 else evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x_1 →
      (if x = 0 then some (unpair n).2 else evaln k₂ cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x_1
neg :
  ∀ (x0 : ¬x = 0),
    (if x = 0 then some (unpair n).2 else evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x_1 →
      (if x = 0 then some (unpair n).2 else evaln k₂ cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x_1
⊢ (if x = 0 then some (unpair n).2 else evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x_1 →
    (if x = 0 then some (unpair n).2 else evaln k₂ cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x_1

Tactic:
by_cases x0 : x = 0
-- 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
cf : Code
hf : ∀ (n x : ℕ) (h : evaln (k + 1) cf n = some x), evaln (k₂ + 1) cf n = some x
n x_1 : ℕ
h_1 :
  (fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          unpaired
              (fun (a m : ℕ) ↦ do
                let x ← evaln (k + 1) cf (Nat.pair a m)
                if x = 0 then pure m else evaln k cf.rfind' (Nat.pair a (m + 1)))
              n :
          Option ℕ))
      n =
    some x_1
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_1
x : ℕ
x0 : x = 0
⊢ (if x = 0 then some (unpair n).2 else evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x_1 →
    (if x = 0 then some (unpair n).2 else evaln k₂ cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x_1

Tactic:
simp [x0]