awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
inst : Primcodable α
P : α → ℕ → Prop
inst_1 : DecidableRel P
hP_comp : ComputablePred fun (p : α × ℕ) ↦ P p.1 p.2
hP_ex : ∀ (x : α), ∃ (n : ℕ), P x n
h : Partrec.{u_1, 0} (α := α) (σ := ℕ) fun (x : α) ↦ Nat.rfind fun (n : ℕ) ↦ Part.some (decide (P x n))
x : α
⊢ Nat.find (p := P x) ⋯ ∈ Nat.rfind fun (n : ℕ) ↦ Part.some (decide (P x n))

Tactic:
simp +contextual [Nat.find_spec]

Premises used: Nat.find_spec
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
inst : Primcodable α
f : α → Bool
h : Computable f
⊢ DecidablePred fun (a : α) ↦ f a = true

Tactic:
infer_instance
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
inst : Primcodable α
f : α → Bool
h : Computable f
⊢ Computable (σ := Bool) fun (a : α) ↦ decide ((fun (a : α) ↦ f a = true) a)

Tactic:
simpa using h
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
inst : Primcodable α
f : α → Bool
h : Computable f
⊢ ComputablePred fun (a : α) ↦ f a = true

Tactic:
exact ⟨by infer_instance, by simpa using h⟩
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
w : DecidablePred p
hp : Computable (σ := Bool) fun (a : α) ↦ decide (p a)
⊢ ∀ (n : α), (!decide (p n)) = decide ¬p n

Tactic:
simp
-- Module: Mathlib.Computability.RE
Goal:
f₁ f₂ : ℕ → ℕ
hf₁ : Computable f₁
hf₂ : Computable f₂
c : ℕ → Prop
inst : DecidablePred c
hc : ComputablePred c
⊢ Computable (σ := ℕ) fun (k : ℕ) ↦ if c k then f₁ k else f₂ k

Tactic:
simpa [Bool.cond_decide] using hc.decide.cond hf₁ hf₂

Premises used: ComputablePred.decide, Computable.cond, Bool.cond_decide
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
hp : ComputablePred p
obtain :
  ∀ (f : α → Bool) (hf : Computable f) (hp : ComputablePred fun (a : α) ↦ f a = true), REPred fun (a : α) ↦ f a = true
⊢ REPred p

Tactic:
obtain ⟨f, hf, rfl⟩ := computable_iff.1 hp

Premises used: Iff.mp, ComputablePred.computable_iff, rfl
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
inst : Primcodable α
f : α → Bool
hf : Computable f
hp : ComputablePred fun (a : α) ↦ f a = true
⊢ Partrec.{u_1, 0} (α := α) (σ := Unit) fun (a : α) ↦ Part.assert (f a = true) fun (x : f a = true) ↦ Part.some ()

Tactic:
(Partrec.cond hf (Decidable.Partrec.const' (Part.some ())) Partrec.none).of_eq fun n =>
      Part.ext fun a => ?_

Premises used: Unit.unit, Part.some, Part.ext, Partrec.cond, Partrec.none, Partrec.of_eq, Decidable.Partrec.const'
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
inst : Primcodable α
f : α → Bool
hf : Computable f
hp : ComputablePred fun (a : α) ↦ f a = true
hf₁ :
  ∀ (n : α) (a : Unit),
    (a ∈ bif f n then Part.some () else Part.none) ↔
      Membership.mem (γ := Part Unit) (Part.assert (f n = true) fun (x : f n = true) ↦ Part.some ()) a
⊢ Partrec.{u_1, 0} (α := α) (σ := Unit) fun (a : α) ↦ Part.assert (f a = true) fun (x : f a = true) ↦ Part.some ()

Tactic:
refine
    (Partrec.cond hf (Decidable.Partrec.const' (Part.some ())) Partrec.none).of_eq fun n =>
      Part.ext fun a => ?_

Premises used: Unit.unit, Part.some, Part.ext, Partrec.cond, Partrec.none, Partrec.of_eq, Decidable.Partrec.const'
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
inst : Primcodable α
f : α → Bool
hf : Computable f
hp : ComputablePred fun (a : α) ↦ f a = true
n : α
a : Unit
unit :
  (PUnit.unit ∈ bif f n then Part.some () else Part.none) ↔
    Membership.mem (γ := Part Unit) (Part.assert (f n = true) fun (x : f n = true) ↦ Part.some ()) PUnit.unit
⊢ (a ∈ bif f n then Part.some () else Part.none) ↔
    Membership.mem (γ := Part Unit) (Part.assert (f n = true) fun (x : f n = true) ↦ Part.some ()) a

Tactic:
cases a
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
inst : Primcodable α
f : α → Bool
hf : Computable f
hp : ComputablePred fun (a : α) ↦ f a = true
n : α
unit :
  (PUnit.unit ∈ bif false then Part.some () else Part.none) ↔
    Membership.mem (γ := Part Unit) (Part.assert (false = true) fun (x : false = true) ↦ Part.some ()) PUnit.unit
unit₁ :
  (PUnit.unit ∈ bif true then Part.some () else Part.none) ↔
    Membership.mem (γ := Part Unit) (Part.assert (true = true) fun (x : true = true) ↦ Part.some ()) PUnit.unit
⊢ (PUnit.unit ∈ bif f n then Part.some () else Part.none) ↔
    Membership.mem (γ := Part Unit) (Part.assert (f n = true) fun (x : f n = true) ↦ Part.some ()) PUnit.unit

Tactic:
cases f n
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
inst : Primcodable α
f : α → Bool
hf : Computable f
hp : ComputablePred fun (a : α) ↦ f a = true
n : α
⊢ (PUnit.unit ∈ bif false then Part.some () else Part.none) ↔
    Membership.mem (γ := Part Unit) (Part.assert (false = true) fun (x : false = true) ↦ Part.some ()) PUnit.unit

Tactic:
simp
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
inst : Primcodable α
f : α → Bool
hf : Computable f
hp : ComputablePred fun (a : α) ↦ f a = true
n : α
⊢ (PUnit.unit ∈ bif true then Part.some () else Part.none) ↔
    Membership.mem (γ := Part Unit) (Part.assert (true = true) fun (x : true = true) ↦ Part.some ()) PUnit.unit

Tactic:
simp
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
inst_1 : DecidablePred p
h : REPred p ∧ REPred fun (a : α) ↦ ¬p a
h₁ : REPred p
h₂ : REPred fun (a : α) ↦ ¬p a
a : α
x : Bool
hx :
  Membership.mem (γ := Part Bool) (Part.map (fun (b : Unit) ↦ true) (Part.assert (p a) fun (x : p a) ↦ Part.some ())) x
y : Bool
hy :
  Membership.mem (γ := Part Bool)
    (Part.map (fun (b : Unit) ↦ false)
      (Part.assert ((fun (a : α) ↦ ¬p a) a) fun (x : (fun (a : α) ↦ ¬p a) a) ↦ Part.some ()))
    y
⊢ p a ∧ true = x

Tactic:
simp only [Part.mem_map_iff, Part.mem_assert_iff, Part.mem_some_iff, exists_prop,
            and_true, exists_const] at hx hy

Premises used: and_true, Part.mem_some_iff, exists_prop, exists_const, Part.mem_map_iff, Part.mem_assert_iff
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
inst_1 : DecidablePred p
h : REPred p ∧ REPred fun (a : α) ↦ ¬p a
h₁ : REPred p
h₂ : REPred fun (a : α) ↦ ¬p a
a : α
x : Bool
hx :
  Membership.mem (γ := Part Bool) (Part.map (fun (b : Unit) ↦ true) (Part.assert (p a) fun (x : p a) ↦ Part.some ())) x
y : Bool
hy :
  Membership.mem (γ := Part Bool)
    (Part.map (fun (b : Unit) ↦ false)
      (Part.assert ((fun (a : α) ↦ ¬p a) a) fun (x : (fun (a : α) ↦ ¬p a) a) ↦ Part.some ()))
    y
hx₁ : p a ∧ true = x
⊢ ¬p a ∧ false = y

Tactic:
simp only [Part.mem_map_iff, Part.mem_assert_iff, Part.mem_some_iff, exists_prop,
            and_true, exists_const] at hx hy

Premises used: and_true, Part.mem_some_iff, exists_prop, exists_const, Part.mem_map_iff, Part.mem_assert_iff
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
inst_1 : DecidablePred p
h : REPred p ∧ REPred fun (a : α) ↦ ¬p a
h₁ : REPred p
h₂ : REPred fun (a : α) ↦ ¬p a
a : α
x y : Bool
hx : p a ∧ true = x
hy : ¬p a ∧ false = y
⊢ x = y

Tactic:
cases hy.1 hx.1

Premises used: And.left
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
inst_1 : DecidablePred p
h : REPred p ∧ REPred fun (a : α) ↦ ¬p a
h₁ : REPred p
h₂ : REPred fun (a : α) ↦ ¬p a
obtain :
  ∀ (k : α →. Bool) (pk : Partrec k)
    (hk :
      ∀ (a : α) (x : Bool),
        x ∈ k a ↔
          Membership.mem (γ := Part Bool)
              (Part.map (fun (b : Unit) ↦ true) (Part.assert (p a) fun (x : p a) ↦ Part.some ())) x ∨
            Membership.mem (γ := Part Bool)
              (Part.map (fun (b : Unit) ↦ false)
                (Part.assert ((fun (a : α) ↦ ¬p a) a) fun (x : (fun (a : α) ↦ ¬p a) a) ↦ Part.some ()))
              x),
    Computable (σ := Bool) fun (a : α) ↦ decide (p a)
⊢ Computable (σ := Bool) fun (a : α) ↦ decide (p a)

Tactic:
obtain ⟨k, pk, hk⟩ :=
        Partrec.merge (h₁.map (Computable.const true).to₂) (h₂.map (Computable.const false).to₂)
        (by
          intro a x hx y hy
          simp only [Part.mem_map_iff, Part.mem_assert_iff, Part.mem_some_iff, exists_prop,
            and_true, exists_const] at hx hy
          cases hy.1 hx.1)

Premises used: Partrec.merge, Bool.true, Computable.const, Partrec.map, Bool.false, Computable.to₂
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
inst_1 : DecidablePred p
h : REPred p ∧ REPred fun (a : α) ↦ ¬p a
h₁ : REPred p
h₂ : REPred fun (a : α) ↦ ¬p a
k : α →. Bool
pk : Partrec k
hk :
  ∀ (a : α) (x : Bool),
    x ∈ k a ↔
      Membership.mem (γ := Part Bool)
          (Part.map (fun (b : Unit) ↦ true) (Part.assert (p a) fun (x : p a) ↦ Part.some ())) x ∨
        Membership.mem (γ := Part Bool)
          (Part.map (fun (b : Unit) ↦ false)
            (Part.assert ((fun (a : α) ↦ ¬p a) a) fun (x : (fun (a : α) ↦ ¬p a) a) ↦ Part.some ()))
          x
⊢ Computable (σ := Bool) fun (a : α) ↦ decide (p a)

Tactic:
Partrec.of_eq pk fun n => Part.eq_some_iff.2 ?_

Premises used: Iff.mpr, Part.eq_some_iff, Partrec.of_eq, Computable
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
inst_1 : DecidablePred p
h : REPred p ∧ REPred fun (a : α) ↦ ¬p a
h₁ : REPred p
h₂ : REPred fun (a : α) ↦ ¬p a
k : α →. Bool
pk : Partrec k
hk :
  ∀ (a : α) (x : Bool),
    x ∈ k a ↔
      Membership.mem (γ := Part Bool)
          (Part.map (fun (b : Unit) ↦ true) (Part.assert (p a) fun (x : p a) ↦ Part.some ())) x ∨
        Membership.mem (γ := Part Bool)
          (Part.map (fun (b : Unit) ↦ false)
            (Part.assert ((fun (a : α) ↦ ¬p a) a) fun (x : (fun (a : α) ↦ ¬p a) a) ↦ Part.some ()))
          x
refine : ∀ (n : α), (fun (a : α) ↦ decide (p a)) n ∈ k n
⊢ Computable (σ := Bool) fun (a : α) ↦ decide (p a)

Tactic:
refine Partrec.of_eq pk fun n => Part.eq_some_iff.2 ?_

Premises used: Iff.mpr, Part.eq_some_iff, Partrec.of_eq
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
inst_1 : DecidablePred p
h : REPred p ∧ REPred fun (a : α) ↦ ¬p a
h₁ : REPred p
h₂ : REPred fun (a : α) ↦ ¬p a
k : α →. Bool
pk : Partrec k
hk :
  ∀ (a : α) (x : Bool),
    x ∈ k a ↔
      Membership.mem (γ := Part Bool)
          (Part.map (fun (b : Unit) ↦ true) (Part.assert (p a) fun (x : p a) ↦ Part.some ())) x ∨
        Membership.mem (γ := Part Bool)
          (Part.map (fun (b : Unit) ↦ false)
            (Part.assert ((fun (a : α) ↦ ¬p a) a) fun (x : (fun (a : α) ↦ ¬p a) a) ↦ Part.some ()))
          x
n : α
rw :
  Membership.mem (γ := Part Bool) (Part.map (fun (b : Unit) ↦ true) (Part.assert (p n) fun (x : p n) ↦ Part.some ()))
      ((fun (a : α) ↦ decide (p a)) n) ∨
    Membership.mem (γ := Part Bool)
      (Part.map (fun (b : Unit) ↦ false)
        (Part.assert ((fun (a : α) ↦ ¬p a) n) fun (x : (fun (a : α) ↦ ¬p a) n) ↦ Part.some ()))
      ((fun (a : α) ↦ decide (p a)) n)
⊢ (fun (a : α) ↦ decide (p a)) n ∈ k n

Tactic:
rw [hk]
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
inst_1 : DecidablePred p
h : REPred p ∧ REPred fun (a : α) ↦ ¬p a
h₁ : REPred p
h₂ : REPred fun (a : α) ↦ ¬p a
k : α →. Bool
pk : Partrec k
hk :
  ∀ (a : α) (x : Bool),
    x ∈ k a ↔
      Membership.mem (γ := Part Bool)
          (Part.map (fun (b : Unit) ↦ true) (Part.assert (p a) fun (x : p a) ↦ Part.some ())) x ∨
        Membership.mem (γ := Part Bool)
          (Part.map (fun (b : Unit) ↦ false)
            (Part.assert ((fun (a : α) ↦ ¬p a) a) fun (x : (fun (a : α) ↦ ¬p a) a) ↦ Part.some ()))
          x
n : α
simp : p n ∨ ¬p n
⊢ Membership.mem (γ := Part Bool) (Part.map (fun (b : Unit) ↦ true) (Part.assert (p n) fun (x : p n) ↦ Part.some ()))
      ((fun (a : α) ↦ decide (p a)) n) ∨
    Membership.mem (γ := Part Bool)
      (Part.map (fun (b : Unit) ↦ false)
        (Part.assert ((fun (a : α) ↦ ¬p a) n) fun (x : (fun (a : α) ↦ ¬p a) n) ↦ Part.some ()))
      ((fun (a : α) ↦ decide (p a)) n)

Tactic:
simp only [Part.mem_map_iff, Part.mem_assert_iff, Part.mem_some_iff, exists_prop, and_true,
        true_eq_decide_iff, and_self, exists_const, false_eq_decide_iff]

Premises used: and_true, and_self, Part.mem_some_iff, false_eq_decide_iff, exists_prop, exists_const, Part.mem_map_iff, true_eq_decide_iff, Part.mem_assert_iff
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
inst_1 : DecidablePred p
h : REPred p ∧ REPred fun (a : α) ↦ ¬p a
h₁ : REPred p
h₂ : REPred fun (a : α) ↦ ¬p a
k : α →. Bool
pk : Partrec k
hk :
  ∀ (a : α) (x : Bool),
    x ∈ k a ↔
      Membership.mem (γ := Part Bool)
          (Part.map (fun (b : Unit) ↦ true) (Part.assert (p a) fun (x : p a) ↦ Part.some ())) x ∨
        Membership.mem (γ := Part Bool)
          (Part.map (fun (b : Unit) ↦ false)
            (Part.assert ((fun (a : α) ↦ ¬p a) a) fun (x : (fun (a : α) ↦ ¬p a) a) ↦ Part.some ()))
          x
n : α
⊢ p n ∨ ¬p n

Tactic:
apply Decidable.em

Premises used: Decidable.em
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
⊢ ComputablePred p ↔ REPred p ∧ REPred fun (a : α) ↦ ¬p a

Tactic:
computable_iff_re_compl_re

Premises used: ComputablePred.computable_iff_re_compl_re
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
⊢ ComputablePred p ↔ REPred p ∧ REPred fun (a : α) ↦ ¬p a

Tactic:
exact computable_iff_re_compl_re

Premises used: ComputablePred.computable_iff_re_compl_re
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
⊢ ComputablePred p ↔ REPred p ∧ REPred fun (a : α) ↦ ¬p a

Tactic:
classical exact computable_iff_re_compl_re

Premises used: ComputablePred.computable_iff_re_compl_re
-- Module: Mathlib.Computability.RecursiveIn
Goal:
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
⊢ RecursiveIn O f ↔ Nat.RecursiveIn O f

Tactic:
simp [RecursiveIn, Part.map_id']

Premises used: RecursiveIn, Part.map_id'
-- Module: Mathlib.Computability.RecursiveIn
Goal:
f g : ℕ →. ℕ
O : Set (ℕ →. ℕ)
hf : Nat.RecursiveIn O f
H : ∀ (n : ℕ), f n = g n
⊢ Nat.RecursiveIn O g

Tactic:
(funext H : f = g) ▸ hf

Premises used: Eq.rec, funext
-- Module: Mathlib.Computability.RecursiveIn
Goal:
f : ℕ →. ℕ
g : ℕ → ℕ
O : Set (ℕ →. ℕ)
hf : Nat.RecursiveIn O f
H : ∀ (n : ℕ), g n ∈ f n
⊢ Nat.RecursiveIn O (↑g : ℕ →. ℕ)

Tactic:
of_eq hf fun n => eq_some_iff.2 (H n)

Premises used: Iff.mpr, Part.eq_some_iff, Nat.RecursiveIn.of_eq
-- Module: Mathlib.Computability.RecursiveIn
Goal:
O O' : Set (ℕ →. ℕ)
f : ℕ →. ℕ
hO : ∀ g ∈ O, Nat.RecursiveIn O' g
⊢ Nat.RecursiveIn O' fun (x : ℕ) ↦ 0

Tactic:
constructor
-- Module: Mathlib.Computability.RecursiveIn
Goal:
O O' : Set (ℕ →. ℕ)
f : ℕ →. ℕ
hO : ∀ g ∈ O, Nat.RecursiveIn O' g
⊢ Nat.RecursiveIn O' (↑Nat.succ : ℕ →. ℕ)

Tactic:
constructor
-- Module: Mathlib.Computability.RecursiveIn
Goal:
O O' : Set (ℕ →. ℕ)
f : ℕ →. ℕ
hO : ∀ g ∈ O, Nat.RecursiveIn O' g
⊢ Nat.RecursiveIn O' fun (n : ℕ) ↦ (↑(Option.some (unpair n).1) : Part ℕ)

Tactic:
constructor
-- Module: Mathlib.Computability.RecursiveIn
Goal:
O O' : Set (ℕ →. ℕ)
f : ℕ →. ℕ
hO : ∀ g ∈ O, Nat.RecursiveIn O' g
⊢ Nat.RecursiveIn O' fun (n : ℕ) ↦ (↑(Option.some (unpair n).2) : Part ℕ)

Tactic:
constructor
-- Module: Mathlib.Computability.RecursiveIn
Goal:
O O' : Set (ℕ →. ℕ)
f : ℕ →. ℕ
hO : ∀ g ∈ O, Nat.RecursiveIn O' g
g : ℕ →. ℕ
hg : g ∈ O
⊢ Nat.RecursiveIn O' g

Tactic:
hO g hg
-- Module: Mathlib.Computability.RecursiveIn
Goal:
O O' : Set (ℕ →. ℕ)
f : ℕ →. ℕ
hO : ∀ g ∈ O, Nat.RecursiveIn O' g
g : ℕ →. ℕ
hg : g ∈ O
⊢ Nat.RecursiveIn O' g

Tactic:
exact hO g hg
-- Module: Mathlib.Computability.RecursiveIn
Goal:
O O' : Set (ℕ →. ℕ)
f : ℕ →. ℕ
hO : ∀ g ∈ O, Nat.RecursiveIn O' g
f_1 h : ℕ →. ℕ
hf : Nat.RecursiveIn O f_1
hh : Nat.RecursiveIn O h
ihf : Nat.RecursiveIn O' f_1
ihg : Nat.RecursiveIn O' h
⊢ Nat.RecursiveIn O' fun (n : ℕ) ↦ Nat.pair <$> f_1 n <*> h n

Tactic:
.pair ihf ihg

Premises used: Nat.RecursiveIn.pair
-- Module: Mathlib.Computability.RecursiveIn
Goal:
O O' : Set (ℕ →. ℕ)
f : ℕ →. ℕ
hO : ∀ g ∈ O, Nat.RecursiveIn O' g
f_1 h : ℕ →. ℕ
hf : Nat.RecursiveIn O f_1
hh : Nat.RecursiveIn O h
ihf : Nat.RecursiveIn O' f_1
ihg : Nat.RecursiveIn O' h
⊢ Nat.RecursiveIn O' fun (n : ℕ) ↦ Nat.pair <$> f_1 n <*> h n

Tactic:
exact .pair ihf ihg
-- Module: Mathlib.Computability.RecursiveIn
Goal:
O O' : Set (ℕ →. ℕ)
f : ℕ →. ℕ
hO : ∀ g ∈ O, Nat.RecursiveIn O' g
f_1 h : ℕ →. ℕ
hf : Nat.RecursiveIn O f_1
hh : Nat.RecursiveIn O h
ihf : Nat.RecursiveIn O' f_1
ihg : Nat.RecursiveIn O' h
⊢ Nat.RecursiveIn O' fun (n : ℕ) ↦ h n >>= f_1

Tactic:
.comp ihf ihg

Premises used: Nat.RecursiveIn.comp
-- Module: Mathlib.Computability.RecursiveIn
Goal:
O O' : Set (ℕ →. ℕ)
f : ℕ →. ℕ
hO : ∀ g ∈ O, Nat.RecursiveIn O' g
f_1 h : ℕ →. ℕ
hf : Nat.RecursiveIn O f_1
hh : Nat.RecursiveIn O h
ihf : Nat.RecursiveIn O' f_1
ihg : Nat.RecursiveIn O' h
⊢ Nat.RecursiveIn O' fun (n : ℕ) ↦ h n >>= f_1

Tactic:
exact .comp ihf ihg
-- Module: Mathlib.Computability.RecursiveIn
Goal:
O O' : Set (ℕ →. ℕ)
f : ℕ →. ℕ
hO : ∀ g ∈ O, Nat.RecursiveIn O' g
f_1 h : ℕ →. ℕ
hf : Nat.RecursiveIn O f_1
hh : Nat.RecursiveIn O h
ihf : Nat.RecursiveIn O' f_1
ihg : Nat.RecursiveIn O' h
⊢ Nat.RecursiveIn O' fun (p : ℕ) ↦
    match (motive := ℕ × ℕ → Part ℕ) unpair p with
    | (a, n) =>
      Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (f_1 a)
        (fun (y : ℕ) (IH : Part ℕ) ↦ do
          let i ← IH
          h (Nat.pair a (Nat.pair y i)))
        n

Tactic:
.prec ihf ihg

Premises used: Nat.RecursiveIn.prec
-- Module: Mathlib.Computability.RecursiveIn
Goal:
O O' : Set (ℕ →. ℕ)
f : ℕ →. ℕ
hO : ∀ g ∈ O, Nat.RecursiveIn O' g
f_1 h : ℕ →. ℕ
hf : Nat.RecursiveIn O f_1
hh : Nat.RecursiveIn O h
ihf : Nat.RecursiveIn O' f_1
ihg : Nat.RecursiveIn O' h
⊢ Nat.RecursiveIn O' fun (p : ℕ) ↦
    match (motive := ℕ × ℕ → Part ℕ) unpair p with
    | (a, n) =>
      Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (f_1 a)
        (fun (y : ℕ) (IH : Part ℕ) ↦ do
          let i ← IH
          h (Nat.pair a (Nat.pair y i)))
        n

Tactic:
exact .prec ihf ihg
-- Module: Mathlib.Computability.RecursiveIn
Goal:
O O' : Set (ℕ →. ℕ)
f : ℕ →. ℕ
hO : ∀ g ∈ O, Nat.RecursiveIn O' g
f_1 : ℕ →. ℕ
hf : Nat.RecursiveIn O f_1
ihf : Nat.RecursiveIn O' f_1
⊢ Nat.RecursiveIn O' fun (a : ℕ) ↦ Nat.rfind fun (n : ℕ) ↦ (fun (m : ℕ) ↦ decide (m = 0)) <$> f_1 (Nat.pair a n)

Tactic:
.rfind ihf

Premises used: Nat.RecursiveIn.rfind
-- Module: Mathlib.Computability.RecursiveIn
Goal:
O O' : Set (ℕ →. ℕ)
f : ℕ →. ℕ
hO : ∀ g ∈ O, Nat.RecursiveIn O' g
f_1 : ℕ →. ℕ
hf : Nat.RecursiveIn O f_1
ihf : Nat.RecursiveIn O' f_1
⊢ Nat.RecursiveIn O' fun (a : ℕ) ↦ Nat.rfind fun (n : ℕ) ↦ (fun (m : ℕ) ↦ decide (m = 0)) <$> f_1 (Nat.pair a n)

Tactic:
exact .rfind ihf
-- Module: Mathlib.Computability.RecursiveIn
Goal:
O O' : Set (ℕ →. ℕ)
f : ℕ →. ℕ
hf : Nat.RecursiveIn O f
hO : ∀ g ∈ O, Nat.RecursiveIn O' g
zero : Nat.RecursiveIn O' fun (x : ℕ) ↦ 0
succ : Nat.RecursiveIn O' (↑Nat.succ : ℕ →. ℕ)
left : Nat.RecursiveIn O' fun (n : ℕ) ↦ (↑(Option.some (unpair n).1) : Part ℕ)
right : Nat.RecursiveIn O' fun (n : ℕ) ↦ (↑(Option.some (unpair n).2) : Part ℕ)
oracle : ∀ (g : ℕ →. ℕ) (hg : g ∈ O), Nat.RecursiveIn O' g
pair :
  ∀ {f h : ℕ →. ℕ},
    Nat.RecursiveIn O f →
      Nat.RecursiveIn O h →
        ∀ (ihf : Nat.RecursiveIn O' f) (ihg : Nat.RecursiveIn O' h),
          Nat.RecursiveIn O' fun (n : ℕ) ↦ Nat.pair <$> f n <*> h n
comp :
  ∀ {f h : ℕ →. ℕ},
    Nat.RecursiveIn O f →
      Nat.RecursiveIn O h →
        ∀ (ihf : Nat.RecursiveIn O' f) (ihg : Nat.RecursiveIn O' h), Nat.RecursiveIn O' fun (n : ℕ) ↦ h n >>= f
prec :
  ∀ {f h : ℕ →. ℕ},
    Nat.RecursiveIn O f →
      Nat.RecursiveIn O h →
        ∀ (ihf : Nat.RecursiveIn O' f) (ihg : Nat.RecursiveIn O' h),
          Nat.RecursiveIn O' fun (p : ℕ) ↦
            match (motive := ℕ × ℕ → Part ℕ) unpair p with
            | (a, n) =>
              Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (f a)
                (fun (y : ℕ) (IH : Part ℕ) ↦ do
                  let i ← IH
                  h (Nat.pair a (Nat.pair y i)))
                n
rfind :
  ∀ {f : ℕ →. ℕ},
    Nat.RecursiveIn O f →
      ∀ (ihf : Nat.RecursiveIn O' f),
        Nat.RecursiveIn O' fun (a : ℕ) ↦ Nat.rfind fun (n : ℕ) ↦ (fun (m : ℕ) ↦ decide (m = 0)) <$> f (Nat.pair a n)
⊢ Nat.RecursiveIn O' f

Tactic:
induction hf with
  | zero | succ | left | right => constructor
  | oracle g hg => exact hO g hg
  | pair _ _ ihf ihg => exact .pair ihf ihg
  | comp _ _ ihf ihg => exact .comp ihf ihg
  | prec _ _ ihf ihg => exact .prec ihf ihg
  | rfind _ ihf => exact .rfind ihf

Premises used: Nat.RecursiveIn.comp, Nat.RecursiveIn.rfind, Nat.RecursiveIn.oracle, Nat.RecursiveIn.prec, Nat.RecursiveIn.right, Nat.RecursiveIn.pair, Nat.RecursiveIn.left, Nat.RecursiveIn.zero, Nat.RecursiveIn.succ
-- Module: Mathlib.Computability.RecursiveIn
Goal:
O O' : Set (ℕ →. ℕ)
f : ℕ →. ℕ
hf : Nat.RecursiveIn O f
hO : ∀ g ∈ O, Nat.RecursiveIn O' g
⊢ Nat.RecursiveIn O' f

Tactic:
induction hf with
  | zero | succ | left | right => constructor
  | oracle g hg => exact hO g hg
  | pair _ _ ihf ihg => exact .pair ihf ihg
  | comp _ _ ihf ihg => exact .comp ihf ihg
  | prec _ _ ihf ihg => exact .prec ihf ihg
  | rfind _ ihf => exact .rfind ihf

Premises used: Nat.RecursiveIn.comp, Nat.RecursiveIn.rfind, Nat.RecursiveIn.oracle, Nat.RecursiveIn.prec, Nat.RecursiveIn.right, Nat.RecursiveIn.pair, Nat.RecursiveIn.left, Nat.RecursiveIn.zero, Nat.RecursiveIn.succ
-- Module: Mathlib.Computability.RecursiveIn
Goal:
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
hO : ∀ g ∈ O, Nat.Partrec g
⊢ Nat.Partrec fun (x : ℕ) ↦ 0

Tactic:
constructor
-- Module: Mathlib.Computability.RecursiveIn
Goal:
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
hO : ∀ g ∈ O, Nat.Partrec g
⊢ Nat.Partrec (↑Nat.succ : ℕ →. ℕ)

Tactic:
constructor
-- Module: Mathlib.Computability.RecursiveIn
Goal:
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
hO : ∀ g ∈ O, Nat.Partrec g
⊢ Nat.Partrec fun (n : ℕ) ↦ (↑(Option.some (unpair n).1) : Part ℕ)

Tactic:
constructor
-- Module: Mathlib.Computability.RecursiveIn
Goal:
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
hO : ∀ g ∈ O, Nat.Partrec g
⊢ Nat.Partrec fun (n : ℕ) ↦ (↑(Option.some (unpair n).2) : Part ℕ)

Tactic:
constructor
-- Module: Mathlib.Computability.RecursiveIn
Goal:
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
hO : ∀ g ∈ O, Nat.Partrec g
g : ℕ →. ℕ
gIn : g ∈ O
⊢ Nat.Partrec g

Tactic:
hO g gIn
-- Module: Mathlib.Computability.RecursiveIn
Goal:
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
hO : ∀ g ∈ O, Nat.Partrec g
g : ℕ →. ℕ
gIn : g ∈ O
⊢ Nat.Partrec g

Tactic:
exact hO g gIn
-- Module: Mathlib.Computability.RecursiveIn
Goal:
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
hO : ∀ g ∈ O, Nat.Partrec g
f_1 h : ℕ →. ℕ
hf : Nat.RecursiveIn O f_1
hh : Nat.RecursiveIn O h
ih₁ : Nat.Partrec f_1
ih₂ : Nat.Partrec h
⊢ Nat.Partrec fun (n : ℕ) ↦ Nat.pair <$> f_1 n <*> h n

Tactic:
.pair ih₁ ih₂

Premises used: Nat.Partrec.pair
-- Module: Mathlib.Computability.RecursiveIn
Goal:
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
hO : ∀ g ∈ O, Nat.Partrec g
f_1 h : ℕ →. ℕ
hf : Nat.RecursiveIn O f_1
hh : Nat.RecursiveIn O h
ih₁ : Nat.Partrec f_1
ih₂ : Nat.Partrec h
⊢ Nat.Partrec fun (n : ℕ) ↦ Nat.pair <$> f_1 n <*> h n

Tactic:
exact .pair ih₁ ih₂
-- Module: Mathlib.Computability.RecursiveIn
Goal:
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
hO : ∀ g ∈ O, Nat.Partrec g
f_1 h : ℕ →. ℕ
hf : Nat.RecursiveIn O f_1
hh : Nat.RecursiveIn O h
ih₁ : Nat.Partrec f_1
ih₂ : Nat.Partrec h
⊢ Nat.Partrec fun (n : ℕ) ↦ h n >>= f_1

Tactic:
.comp ih₁ ih₂

Premises used: Nat.Partrec.comp
-- Module: Mathlib.Computability.RecursiveIn
Goal:
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
hO : ∀ g ∈ O, Nat.Partrec g
f_1 h : ℕ →. ℕ
hf : Nat.RecursiveIn O f_1
hh : Nat.RecursiveIn O h
ih₁ : Nat.Partrec f_1
ih₂ : Nat.Partrec h
⊢ Nat.Partrec fun (n : ℕ) ↦ h n >>= f_1

Tactic:
exact .comp ih₁ ih₂
-- Module: Mathlib.Computability.RecursiveIn
Goal:
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
hO : ∀ g ∈ O, Nat.Partrec g
f_1 h : ℕ →. ℕ
hf : Nat.RecursiveIn O f_1
hh : Nat.RecursiveIn O h
ih₁ : Nat.Partrec f_1
ih₂ : Nat.Partrec h
⊢ Nat.Partrec fun (p : ℕ) ↦
    match (motive := ℕ × ℕ → Part ℕ) unpair p with
    | (a, n) =>
      Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (f_1 a)
        (fun (y : ℕ) (IH : Part ℕ) ↦ do
          let i ← IH
          h (Nat.pair a (Nat.pair y i)))
        n

Tactic:
.prec ih₁ ih₂

Premises used: Nat.Partrec.prec