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
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)
          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

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)
          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
prec :
  ∀
    (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
⊢ (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

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 : Code
a_ih : ∀ (n x : ℕ) (h : evaln (k + 1) a n = some x), evaln (k₂ + 1) a n = some x
n x : ℕ
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

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 : Code
a_ih : ∀ (n x : ℕ) (h : evaln (k + 1) a n = some x), evaln (k₂ + 1) a n = some x
n x : ℕ
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
rfind' :
  ∀
    (h :
      Membership.mem (γ := Option ℕ)
        (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)
        x),
    Membership.mem (γ := Option ℕ)
      (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)
      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

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_1 :
  (fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          pure 0 : Option ℕ))
      n =
    some x
h : Membership.mem (γ := Option ℕ) (pure 0) x
⊢ Membership.mem (γ := Option ℕ) (pure 0) x

Tactic:
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_1 :
  (fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          pure 0 : Option ℕ))
      n =
    some x
h : Membership.mem (γ := Option ℕ) (pure 0) x
⊢ Membership.mem (γ := Option ℕ) (pure 0) x

Tactic:
exact 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_1 :
  (fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          pure n.succ : Option ℕ))
      n =
    some x
h : Membership.mem (γ := Option ℕ) (pure n.succ) x
⊢ Membership.mem (γ := Option ℕ) (pure n.succ) x

Tactic:
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_1 :
  (fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          pure n.succ : Option ℕ))
      n =
    some x
h : Membership.mem (γ := Option ℕ) (pure n.succ) x
⊢ Membership.mem (γ := Option ℕ) (pure n.succ) x

Tactic:
exact 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_1 :
  (fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          pure (unpair n).1 : Option ℕ))
      n =
    some x
h : Membership.mem (γ := Option ℕ) (pure (unpair n).1) x
⊢ Membership.mem (γ := Option ℕ) (pure (unpair n).1) x

Tactic:
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_1 :
  (fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          pure (unpair n).1 : Option ℕ))
      n =
    some x
h : Membership.mem (γ := Option ℕ) (pure (unpair n).1) x
⊢ Membership.mem (γ := Option ℕ) (pure (unpair n).1) x

Tactic:
exact 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_1 :
  (fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          pure (unpair n).2 : Option ℕ))
      n =
    some x
h : Membership.mem (γ := Option ℕ) (pure (unpair n).2) x
⊢ Membership.mem (γ := Option ℕ) (pure (unpair n).2) x

Tactic:
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_1 :
  (fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          pure (unpair n).2 : Option ℕ))
      n =
    some x
h : Membership.mem (γ := Option ℕ) (pure (unpair n).2) x
⊢ Membership.mem (γ := Option ℕ) (pure (unpair n).2) x

Tactic:
exact 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_1 :
  (fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          Nat.pair <$> evaln (k + 1) cf n <*> evaln (k + 1) cg n : Option ℕ))
      n =
    some x
h : x ∈ Nat.pair <$> evaln (k + 1) cf n <*> evaln (k + 1) cg n
simp :
  ∀ (h : ∃ (a : ℕ), evaln (k + 1) cf n = some a ∧ ∃ (a_1 : ℕ), evaln (k + 1) cg n = some a_1 ∧ Nat.pair a a_1 = x),
    ∃ (a : ℕ), evaln (k₂ + 1) cf n = some a ∧ ∃ (a_1 : ℕ), evaln (k₂ + 1) cg n = some a_1 ∧ Nat.pair a a_1 = x
⊢ x ∈ Nat.pair <$> evaln (k₂ + 1) cf n <*> evaln (k₂ + 1) cg n

Tactic:
simp only [Seq.seq, Option.map_eq_map, Option.mem_def, Option.bind_eq_some_iff,
          Option.map_eq_some_iff, exists_exists_and_eq_and] at h ⊢

Premises used: Seq.seq, exists_exists_and_eq_and, Option.bind_eq_some_iff, Option.map_eq_map, Option.map_eq_some_iff, 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_1 :
  (fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          Nat.pair <$> evaln (k + 1) cf n <*> evaln (k + 1) cg n : Option ℕ))
      n =
    some x
h : x ∈ Nat.pair <$> evaln (k + 1) cf n <*> evaln (k + 1) cg n
simp? :
  ∀ (h : ∃ (a : ℕ), evaln (k + 1) cf n = some a ∧ ∃ (a_1 : ℕ), evaln (k + 1) cg n = some a_1 ∧ Nat.pair a a_1 = x),
    ∃ (a : ℕ), evaln (k₂ + 1) cf n = some a ∧ ∃ (a_1 : ℕ), evaln (k₂ + 1) cg n = some a_1 ∧ Nat.pair a a_1 = x
⊢ x ∈ Nat.pair <$> evaln (k₂ + 1) cf n <*> evaln (k₂ + 1) cg n

Tactic:
simp? [Seq.seq, Option.bind_eq_some_iff] at h ⊢ says
        simp only [Seq.seq, Option.map_eq_map, Option.mem_def, Option.bind_eq_some_iff,
          Option.map_eq_some_iff, exists_exists_and_eq_and] at h ⊢

Premises used: Seq.seq, exists_exists_and_eq_and, Option.bind_eq_some_iff, Option.map_eq_map, Option.map_eq_some_iff, 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_1 :
  (fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          Nat.pair <$> evaln (k + 1) cf n <*> evaln (k + 1) cg n : Option ℕ))
      n =
    some x
h : ∃ (a : ℕ), evaln (k + 1) cf n = some a ∧ ∃ (a_1 : ℕ), evaln (k + 1) cg n = some a_1 ∧ Nat.pair a a_1 = x
⊢ ∃ (a : ℕ), evaln (k₂ + 1) cf n = some a ∧ ∃ (a_1 : ℕ), evaln (k₂ + 1) cg n = some a_1 ∧ Nat.pair a a_1 = x

Tactic:
h.imp fun a => And.imp (hf _ _) <| Exists.imp fun b => And.imp_left (hg _ _)

Premises used: And.imp, And.imp_left, 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 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)
          Nat.pair <$> evaln (k + 1) cf n <*> evaln (k + 1) cg n : Option ℕ))
      n =
    some x
h : ∃ (a : ℕ), evaln (k + 1) cf n = some a ∧ ∃ (a_1 : ℕ), evaln (k + 1) cg n = some a_1 ∧ Nat.pair a a_1 = x
⊢ ∃ (a : ℕ), evaln (k₂ + 1) cf n = some a ∧ ∃ (a_1 : ℕ), evaln (k₂ + 1) cg n = some a_1 ∧ Nat.pair a a_1 = x

Tactic:
exact h.imp fun a => And.imp (hf _ _) <| Exists.imp fun b => And.imp_left (hg _ _)

Premises used: And.imp, And.imp_left, 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
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)
          Nat.pair <$> evaln (k + 1) a n <*> evaln (k + 1) a_1 n : Option ℕ))
      n =
    some x
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

Tactic:
case pair cf cg hf hg _ =>
      simp? [Seq.seq, Option.bind_eq_some_iff] at h ⊢ says
        simp only [Seq.seq, Option.map_eq_map, Option.mem_def, Option.bind_eq_some_iff,
          Option.map_eq_some_iff, exists_exists_and_eq_and] at h ⊢
      exact h.imp fun a => And.imp (hf _ _) <| Exists.imp fun b => And.imp_left (hg _ _)

Premises used: Seq.seq, exists_exists_and_eq_and, Option.bind_eq_some_iff, Nat.Partrec.Code.pair, Option.map_eq_map, Option.map_eq_some_iff, 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_1 :
  (fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          let x ← evaln (k + 1) cg n
          evaln (k + 1) cf x : Option ℕ))
      n =
    some x
h :
  Membership.mem (γ := Option ℕ)
    (do
      let x ← evaln (k + 1) cg n
      evaln (k + 1) cf x)
    x
simp :
  ∀ (h : ∃ (a : ℕ), evaln (k + 1) cg n = some a ∧ evaln (k + 1) cf a = some x),
    ∃ (a : ℕ), evaln (k₂ + 1) cg n = some a ∧ evaln (k₂ + 1) cf a = some x
⊢ Membership.mem (γ := Option ℕ)
    (do
      let x ← evaln (k₂ + 1) cg n
      evaln (k₂ + 1) cf x)
    x

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

Premises used: Bind.bind, Option.bind_eq_some_iff, 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_1 :
  (fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          let x ← evaln (k + 1) cg n
          evaln (k + 1) cf x : Option ℕ))
      n =
    some x
h :
  Membership.mem (γ := Option ℕ)
    (do
      let x ← evaln (k + 1) cg n
      evaln (k + 1) cf x)
    x
simp? :
  ∀ (h : ∃ (a : ℕ), evaln (k + 1) cg n = some a ∧ evaln (k + 1) cf a = some x),
    ∃ (a : ℕ), evaln (k₂ + 1) cg n = some a ∧ evaln (k₂ + 1) cf a = some x
⊢ Membership.mem (γ := Option ℕ)
    (do
      let x ← evaln (k₂ + 1) cg n
      evaln (k₂ + 1) cf x)
    x

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

Premises used: Bind.bind, Option.bind_eq_some_iff, 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_1 :
  (fun (n : ℕ) ↦
        (do
          guard (n ≤ k)
          let x ← evaln (k + 1) cg n
          evaln (k + 1) cf x : Option ℕ))
      n =
    some x
h : ∃ (a : ℕ), evaln (k + 1) cg n = some a ∧ evaln (k + 1) cf a = some x
⊢ ∃ (a : ℕ), evaln (k₂ + 1) cg n = some a ∧ evaln (k₂ + 1) cf a = some x

Tactic:
h.imp fun a => And.imp (hg _ _) (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 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)
          let x ← evaln (k + 1) cg n
          evaln (k + 1) cf x : Option ℕ))
      n =
    some x
h : ∃ (a : ℕ), evaln (k + 1) cg n = some a ∧ evaln (k + 1) cf a = some x
⊢ ∃ (a : ℕ), evaln (k₂ + 1) cg n = some a ∧ evaln (k₂ + 1) cf a = some x

Tactic:
exact h.imp fun a => And.imp (hg _ _) (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
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)
          let x ← evaln (k + 1) a_1 n
          evaln (k + 1) a x : Option ℕ))
      n =
    some x
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

Tactic:
case comp cf cg hf hg _ =>
      simp? [Bind.bind, Option.bind_eq_some_iff] at h ⊢ says
        simp only [bind, Option.mem_def, Option.bind_eq_some_iff] at h ⊢
      exact h.imp fun a => And.imp (hg _ _) (hf _ _)

Premises used: Nat.Partrec.Code.comp, Bind.bind, Option.bind_eq_some_iff, Option.mem_def