awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact .prec ih₁ ih₂
-- Module: Mathlib.Computability.RecursiveIn
Goal:
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
hO : ∀ g ∈ O, Nat.Partrec g
f_1 : ℕ →. ℕ
hf : Nat.RecursiveIn O f_1
ih : Nat.Partrec f_1
⊢ Nat.Partrec fun (a : ℕ) ↦ Nat.rfind fun (n : ℕ) ↦ (fun (m : ℕ) ↦ decide (m = 0)) <$> f_1 (Nat.pair a n)

Tactic:
.rfind ih

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

Tactic:
exact .rfind ih
-- Module: Mathlib.Computability.RecursiveIn
Goal:
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
hO : ∀ g ∈ O, Nat.Partrec g
hf : Nat.RecursiveIn O f
zero : Nat.Partrec fun (x : ℕ) ↦ 0
succ : Nat.Partrec (↑Nat.succ : ℕ →. ℕ)
left : Nat.Partrec fun (n : ℕ) ↦ (↑(Option.some (unpair n).1) : Part ℕ)
right : Nat.Partrec fun (n : ℕ) ↦ (↑(Option.some (unpair n).2) : Part ℕ)
oracle : ∀ (g : ℕ →. ℕ) (gIn : g ∈ O), Nat.Partrec g
pair :
  ∀ {f h : ℕ →. ℕ},
    Nat.RecursiveIn O f →
      Nat.RecursiveIn O h →
        ∀ (ih₁ : Nat.Partrec f) (ih₂ : Nat.Partrec h), Nat.Partrec fun (n : ℕ) ↦ Nat.pair <$> f n <*> h n
comp :
  ∀ {f h : ℕ →. ℕ},
    Nat.RecursiveIn O f →
      Nat.RecursiveIn O h → ∀ (ih₁ : Nat.Partrec f) (ih₂ : Nat.Partrec h), Nat.Partrec fun (n : ℕ) ↦ h n >>= f
prec :
  ∀ {f h : ℕ →. ℕ},
    Nat.RecursiveIn O f →
      Nat.RecursiveIn O h →
        ∀ (ih₁ : Nat.Partrec f) (ih₂ : Nat.Partrec h),
          Nat.Partrec 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 →
      ∀ (ih : Nat.Partrec f),
        Nat.Partrec fun (a : ℕ) ↦ Nat.rfind fun (n : ℕ) ↦ (fun (m : ℕ) ↦ decide (m = 0)) <$> f (Nat.pair a n)
⊢ Nat.Partrec f

Tactic:
induction hf with
  | zero | succ | left | right => constructor
  | oracle g gIn => exact hO g gIn
  | pair _ _ ih₁ ih₂ => exact .pair ih₁ ih₂
  | comp _ _ ih₁ ih₂ => exact .comp ih₁ ih₂
  | prec _ _ ih₁ ih₂ => exact .prec ih₁ ih₂
  | rfind _ ih => exact .rfind ih

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
hf : Nat.RecursiveIn O f
⊢ Nat.Partrec f

Tactic:
induction hf with
  | zero | succ | left | right => constructor
  | oracle g gIn => exact hO g gIn
  | pair _ _ ih₁ ih₂ => exact .pair ih₁ ih₂
  | comp _ _ ih₁ ih₂ => exact .comp ih₁ ih₂
  | prec _ _ ih₁ ih₂ => exact .prec ih₁ ih₂
  | rfind _ ih => exact .rfind ih

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 (ℕ →. ℕ)
⊢ Nat.RecursiveIn O (pure 0)

Tactic:
constructor
-- Module: Mathlib.Computability.RecursiveIn
Goal:
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
⊢ Nat.RecursiveIn O (↑Nat.succ : ℕ →. ℕ)

Tactic:
constructor
-- Module: Mathlib.Computability.RecursiveIn
Goal:
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
⊢ Nat.RecursiveIn O (↑fun (n : ℕ) ↦ (unpair n).1 : ℕ →. ℕ)

Tactic:
constructor
-- Module: Mathlib.Computability.RecursiveIn
Goal:
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
⊢ Nat.RecursiveIn O (↑fun (n : ℕ) ↦ (unpair n).2 : ℕ →. ℕ)

Tactic:
constructor
-- Module: Mathlib.Computability.RecursiveIn
Goal:
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
f_1 g : ℕ →. ℕ
h : Nat.Partrec f_1
h_1 : Nat.Partrec g
ih₁ : Nat.RecursiveIn O f_1
ih₂ : Nat.RecursiveIn O g
⊢ Nat.RecursiveIn O fun (n : ℕ) ↦ Nat.pair <$> f_1 n <*> g n

Tactic:
.pair ih₁ ih₂

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

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

Tactic:
.comp ih₁ ih₂

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

Tactic:
exact .comp ih₁ ih₂
-- Module: Mathlib.Computability.RecursiveIn
Goal:
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
f_1 g : ℕ →. ℕ
h : Nat.Partrec f_1
h_1 : Nat.Partrec g
ih₁ : Nat.RecursiveIn O f_1
ih₂ : Nat.RecursiveIn O g
⊢ Nat.RecursiveIn O
    (unpaired fun (a n : ℕ) ↦
      Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (f_1 a)
        (fun (y : ℕ) (IH : Part ℕ) ↦ do
          let i ← IH
          g (Nat.pair a (Nat.pair y i)))
        n)

Tactic:
.prec ih₁ ih₂

Premises used: Nat.RecursiveIn.prec
-- Module: Mathlib.Computability.RecursiveIn
Goal:
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
f_1 g : ℕ →. ℕ
h : Nat.Partrec f_1
h_1 : Nat.Partrec g
ih₁ : Nat.RecursiveIn O f_1
ih₂ : Nat.RecursiveIn O g
⊢ Nat.RecursiveIn O
    (unpaired fun (a n : ℕ) ↦
      Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (f_1 a)
        (fun (y : ℕ) (IH : Part ℕ) ↦ do
          let i ← IH
          g (Nat.pair a (Nat.pair y i)))
        n)

Tactic:
exact .prec ih₁ ih₂
-- Module: Mathlib.Computability.RecursiveIn
Goal:
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
f_1 : ℕ →. ℕ
h : Nat.Partrec f_1
ih : 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 ih

Premises used: Nat.RecursiveIn.rfind
-- Module: Mathlib.Computability.RecursiveIn
Goal:
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
f_1 : ℕ →. ℕ
h : Nat.Partrec f_1
ih : 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 ih
-- Module: Mathlib.Computability.RecursiveIn
Goal:
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
pF : Nat.Partrec f
zero : Nat.RecursiveIn O (pure 0)
succ : Nat.RecursiveIn O (↑Nat.succ : ℕ →. ℕ)
left : Nat.RecursiveIn O (↑fun (n : ℕ) ↦ (unpair n).1 : ℕ →. ℕ)
right : Nat.RecursiveIn O (↑fun (n : ℕ) ↦ (unpair n).2 : ℕ →. ℕ)
pair :
  ∀ {f g : ℕ →. ℕ},
    Nat.Partrec f →
      Nat.Partrec g →
        ∀ (ih₁ : Nat.RecursiveIn O f) (ih₂ : Nat.RecursiveIn O g),
          Nat.RecursiveIn O fun (n : ℕ) ↦ Nat.pair <$> f n <*> g n
comp :
  ∀ {f g : ℕ →. ℕ},
    Nat.Partrec f →
      Nat.Partrec g →
        ∀ (ih₁ : Nat.RecursiveIn O f) (ih₂ : Nat.RecursiveIn O g), Nat.RecursiveIn O fun (n : ℕ) ↦ g n >>= f
prec :
  ∀ {f g : ℕ →. ℕ},
    Nat.Partrec f →
      Nat.Partrec g →
        ∀ (ih₁ : Nat.RecursiveIn O f) (ih₂ : Nat.RecursiveIn O g),
          Nat.RecursiveIn O
            (unpaired fun (a n : ℕ) ↦
              Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (f a)
                (fun (y : ℕ) (IH : Part ℕ) ↦ do
                  let i ← IH
                  g (Nat.pair a (Nat.pair y i)))
                n)
rfind :
  ∀ {f : ℕ →. ℕ},
    Nat.Partrec f →
      ∀ (ih : 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 pF with
  | zero | succ | left | right => constructor
  | pair _ _ ih₁ ih₂ => exact .pair ih₁ ih₂
  | comp _ _ ih₁ ih₂ => exact .comp ih₁ ih₂
  | prec _ _ ih₁ ih₂ => exact .prec ih₁ ih₂
  | rfind _ ih => exact .rfind ih

Premises used: Nat.Partrec.comp, Nat.Partrec.prec, Nat.Partrec.zero, Nat.Partrec.rfind, Nat.Partrec.right, Nat.Partrec.pair, Nat.Partrec.succ, Nat.Partrec.left
-- Module: Mathlib.Computability.RecursiveIn
Goal:
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
pF : Nat.Partrec f
⊢ Nat.RecursiveIn O f

Tactic:
induction pF with
  | zero | succ | left | right => constructor
  | pair _ _ ih₁ ih₂ => exact .pair ih₁ ih₂
  | comp _ _ ih₁ ih₂ => exact .comp ih₁ ih₂
  | prec _ _ ih₁ ih₂ => exact .prec ih₁ ih₂
  | rfind _ ih => exact .rfind ih

Premises used: Nat.Partrec.comp, Nat.Partrec.prec, Nat.Partrec.zero, Nat.Partrec.rfind, Nat.Partrec.right, Nat.Partrec.pair, Nat.Partrec.succ, Nat.Partrec.left
-- Module: Mathlib.Computability.RecursiveIn
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f : α →. σ
O : Set (ℕ →. ℕ)
hf : Partrec f
⊢ RecursiveIn O f

Tactic:
Nat.Partrec.recursiveIn hf

Premises used: RecursiveIn, Nat.Partrec.recursiveIn
-- Module: Mathlib.Computability.RecursiveIn
Goal:
O : Set (ℕ →. ℕ)
f : ℕ → ℕ
hf : Nat.Primrec f
⊢ Nat.RecursiveIn O fun (n : ℕ) ↦ (↑(Option.some (f n)) : Part ℕ)

Tactic:
Nat.Partrec.recursiveIn (Nat.Partrec.of_primrec hf)

Premises used: Nat.Partrec.recursiveIn, Nat.Partrec.of_primrec
-- Module: Mathlib.Computability.RecursiveIn
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → β
O : Set (ℕ →. ℕ)
hf : Computable f
⊢ ComputableIn O f

Tactic:
hf.partrec.recursiveIn

Premises used: Computable.partrec, Partrec.recursiveIn, ComputableIn, PFun.lift
-- Module: Mathlib.Computability.RecursiveIn
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f : α → σ
O : Set (ℕ →. ℕ)
hf : Primrec f
⊢ ComputableIn O f

Tactic:
(Primrec.to_comp hf).computableIn

Premises used: Primrec.to_comp, Computable.computableIn
-- Module: Mathlib.Computability.RecursiveIn
Goal:
α : Type u_1
β : Type u_2
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → β → σ
O : Set (ℕ →. ℕ)
hf : Primrec₂ f
⊢ ComputableIn₂ O f

Tactic:
hf.computableIn

Premises used: ComputableIn₂, Primrec.computableIn
-- Module: Mathlib.Computability.RecursiveIn
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f : α → σ
O : Set (ℕ →. ℕ)
hf : ComputableIn O f
⊢ RecursiveIn.{u_1, u_4} (α := α) (σ := σ) O fun (a : α) ↦ Part.some (f a)

Tactic:
hf

Premises used: ComputableIn
-- Module: Mathlib.Computability.RecursiveIn
Goal:
α : Type u_1
β : Type u_2
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → β → σ
O : Set (ℕ →. ℕ)
hf : ComputableIn₂ O f
⊢ RecursiveIn₂.{u_1, u_2, u_4} (β := β) (σ := σ) O fun (a : α) ↦ (↑(f a) : β →. σ)

Tactic:
hf

Premises used: RecursiveIn₂, ComputableIn, PFun.lift
-- Module: Mathlib.Computability.RecursiveIn
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
O : Set (ℕ →. ℕ)
f g : α →. σ
hf : RecursiveIn O f
H : ∀ (x : α), f x = g x
⊢ RecursiveIn O g

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

Premises used: Eq.rec, funext
-- Module: Mathlib.Computability.RecursiveIn
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
O : Set (ℕ →. ℕ)
f : α →. σ
g : α → σ
hf : RecursiveIn O f
H : ∀ (n : α), g n ∈ f n
⊢ RecursiveIn O (↑g : α →. σ)

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

Premises used: Iff.mpr, Part.eq_some_iff, RecursiveIn.of_eq
-- Module: Mathlib.Computability.RecursiveIn
Goal:
O : Set (ℕ →. ℕ)
g : ℕ →. ℕ
hg : g ∈ O
rw : Nat.RecursiveIn O g
⊢ RecursiveIn O g

Tactic:
rw [iff_nat]

Premises used: RecursiveIn.iff_nat
-- Module: Mathlib.Computability.RecursiveIn
Goal:
O : Set (ℕ →. ℕ)
g : ℕ →. ℕ
hg : g ∈ O
⊢ Nat.RecursiveIn O g

Tactic:
.oracle g hg

Premises used: Nat.RecursiveIn.oracle
-- Module: Mathlib.Computability.RecursiveIn
Goal:
O : Set (ℕ →. ℕ)
g : ℕ →. ℕ
hg : g ∈ O
⊢ Nat.RecursiveIn O g

Tactic:
exact .oracle g hg
-- Module: Mathlib.Computability.RecursiveIn
Goal:
α : Type u_1
inst : Primcodable α
O : Set (ℕ →. ℕ)
⊢ RecursiveIn.{u_1, u_1} (α := α) O Part.some

Tactic:
Partrec.some.recursiveIn

Premises used: Partrec.some, Partrec.recursiveIn
-- Module: Mathlib.Computability.RecursiveIn
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
O : Set (ℕ →. ℕ)
⊢ RecursiveIn.{u_1, u_4} (α := α) (σ := σ) O fun (x : α) ↦ Part.none

Tactic:
Partrec.none.recursiveIn

Premises used: Partrec.recursiveIn, Partrec.none
-- Module: Mathlib.Computability.RecursiveIn
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
O O' : Set (ℕ →. ℕ)
f : α →. σ
hf : RecursiveIn O f
hO : ∀ g ∈ O, RecursiveIn O' g
⊢ ∀ g ∈ O, Nat.RecursiveIn O' g

Tactic:
simpa only [RecursiveIn.iff_nat] using hO

Premises used: RecursiveIn.iff_nat
-- Module: Mathlib.Computability.RecursiveIn
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f : α →. σ
O₁ O₂ : Set (ℕ →. ℕ)
hsub : O₁ ⊆ O₂
hf : RecursiveIn O₁ f
⊢ RecursiveIn O₂ f

Tactic:
hf.subst (fun g hg => .oracle g (hsub hg))

Premises used: RecursiveIn.subst, RecursiveIn.oracle
-- Module: Mathlib.Computability.RecursiveIn
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f : α →. σ
O : Set (ℕ →. ℕ)
hO : ∀ g ∈ O, Partrec g
hf : RecursiveIn O f
⊢ ∀ g ∈ O, Nat.Partrec g

Tactic:
simpa only [Partrec.nat_iff] using hO

Premises used: Partrec.nat_iff
-- Module: Mathlib.Computability.RecursiveIn
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f : α →. σ
s : Part ℕ
hf : RecursiveIn {fun (x : ℕ) ↦ s} f
g : ℕ →. ℕ
hg : Membership.mem (γ := Set (ℕ →. ℕ)) {fun (x : ℕ) ↦ s} g
rw : Partrec (α := ℕ) (σ := ℕ) fun (x : ℕ) ↦ s
⊢ Partrec g

Tactic:
rw [Set.mem_singleton_iff.mp hg]

Premises used: Set.mem_singleton_iff, Iff.mp
-- Module: Mathlib.Computability.RecursiveIn
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f : α →. σ
s : Part ℕ
hf : RecursiveIn {fun (x : ℕ) ↦ s} f
g : ℕ →. ℕ
hg : Membership.mem (γ := Set (ℕ →. ℕ)) {fun (x : ℕ) ↦ s} g
⊢ Partrec (α := ℕ) (σ := ℕ) fun (x : ℕ) ↦ s

Tactic:
.const' s

Premises used: Partrec.const'
-- Module: Mathlib.Computability.RecursiveIn
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f : α →. σ
s : Part ℕ
hf : RecursiveIn {fun (x : ℕ) ↦ s} f
g : ℕ →. ℕ
hg : Membership.mem (γ := Set (ℕ →. ℕ)) {fun (x : ℕ) ↦ s} g
⊢ Partrec (α := ℕ) (σ := ℕ) fun (x : ℕ) ↦ s

Tactic:
exact .const' s
-- Module: Mathlib.Computability.RecursiveIn
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f : α →. σ
⊢ RecursiveIn ∅ f ↔ Partrec f

Tactic:
⟨fun hf => hf.partrec_of_oracle (Set.forall_mem_empty.mpr ⟨⟩), fun hf => hf.recursiveIn⟩

Premises used: Iff.mpr, RecursiveIn.partrec_of_oracle, Partrec.recursiveIn, Iff.intro, Set.forall_mem_empty, True.intro
-- Module: Mathlib.Computability.RecursiveIn
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f : α →. σ
⊢ Partrec f ↔ ∀ (g : ℕ →. ℕ), RecursiveIn {g} f

Tactic:
⟨fun hf _ => hf.recursiveIn, fun hf => (hf (fun _ => .none)).partrec_of_const⟩

Premises used: Part.none, RecursiveIn.partrec_of_const, Partrec.recursiveIn, Iff.intro
-- Module: Mathlib.Computability.RecursiveIn
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
O : Set (ℕ →. ℕ)
s : σ
⊢ ComputableIn.{u_1, u_4} (σ := σ) O fun (x : α) ↦ s

Tactic:
(Primrec.const s).computableIn

Premises used: Primrec.const, Primrec.computableIn
-- Module: Mathlib.Computability.RecursiveIn
Goal:
α : Type u_1
inst : Primcodable α
O : Set (ℕ →. ℕ)
⊢ ComputableIn.{u_1, u_1} (α := α) O id

Tactic:
Primrec.id.computableIn

Premises used: Primrec.computableIn, Primrec.id
-- Module: Mathlib.Computability.RecursiveIn
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
O : Set (ℕ →. ℕ)
⊢ ComputableIn (α := α × β) O Prod.fst

Tactic:
Primrec.fst.computableIn

Premises used: Primrec.fst, Primrec.computableIn
-- Module: Mathlib.Computability.RecursiveIn
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
O : Set (ℕ →. ℕ)
⊢ ComputableIn (α := α × β) O Prod.snd

Tactic:
Primrec.snd.computableIn

Premises used: Primrec.snd, Primrec.computableIn
-- Module: Mathlib.Computability.RecursiveIn
Goal:
O : Set (ℕ →. ℕ)
⊢ ComputableIn O Nat.unpair

Tactic:
Primrec.unpair.computableIn

Premises used: Primrec.unpair, Primrec.computableIn
-- Module: Mathlib.Computability.RecursiveIn
Goal:
O : Set (ℕ →. ℕ)
⊢ ComputableIn O Nat.succ

Tactic:
Primrec.succ.computableIn

Premises used: Primrec.computableIn, Primrec.succ
-- Module: Mathlib.Computability.RecursiveIn
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
O : Set (ℕ →. ℕ)
⊢ ComputableIn (α := α) (σ := α ⊕ β) O Sum.inl

Tactic:
Primrec.sumInl.computableIn

Premises used: Primrec.sumInl, Primrec.computableIn
-- Module: Mathlib.Computability.RecursiveIn
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
O : Set (ℕ →. ℕ)
⊢ ComputableIn (α := β) (σ := α ⊕ β) O Sum.inr

Tactic:
Primrec.sumInr.computableIn

Premises used: Primrec.computableIn, Primrec.sumInr
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → β
q : β → Prop
h : Computable f
⊢ (fun (a : α) ↦ q (f a)) ≤₀ q

Tactic:
⟨f, h, fun _ => Iff.rfl⟩

Premises used: Iff.rfl, ManyOneReducible, And.intro, Exists.intro
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
⊢ ∀ (a : α), p a ↔ p (id a)

Tactic:
simp
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
f : α → β
c₁ : Computable f
h₁ : ∀ (a : α), p a ↔ q (f a)
g : β → γ
c₂ : Computable g
h₂ : ∀ (a : β), q a ↔ r (g a)
a : α
h rw : p a
⊢ r ((g ∘ f) a)

Tactic:
rw [comp_apply, ← h₂, ← h₁]

Premises used: Function.comp_apply
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
f : α → β
c₁ : Computable f
h₁ : ∀ (a : α), p a ↔ q (f a)
g : β → γ
c₂ : Computable g
h₂ : ∀ (a : β), q a ↔ r (g a)
a : α
h : p a
⊢ p a

Tactic:
assumption
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
f : α → β
c₁ : Computable f
h₁ : ∀ (a : α), p a ↔ q (f a)
g : β → γ
c₂ : Computable g
h₂ : ∀ (a : β), q a ↔ r (g a)
a : α
h : r ((g ∘ f) a)
rwa : q (f a)
rwa₁ rwa₂ rwa₃ rwa₄ : r (g (f a))
⊢ p a

Tactic:
rwa [h₁, h₂]
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → β
q : β → Prop
h : Computable f
i : Injective f
⊢ (fun (a : α) ↦ q (f a)) ≤₁ q

Tactic:
⟨f, h, i, fun _ => Iff.rfl⟩

Premises used: OneOneReducible, Iff.rfl, And.intro, Exists.intro
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
f : α → β
c₁ : Computable f
i₁ : Injective f
h₁ : ∀ (a : α), p a ↔ q (f a)
g : β → γ
c₂ : Computable g
i₂ : Injective g
h₂ : ∀ (a : β), q a ↔ r (g a)
a : α
h rw : p a
⊢ r ((g ∘ f) a)

Tactic:
rw [comp_apply, ← h₂, ← h₁]

Premises used: Function.comp_apply
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
f : α → β
c₁ : Computable f
i₁ : Injective f
h₁ : ∀ (a : α), p a ↔ q (f a)
g : β → γ
c₂ : Computable g
i₂ : Injective g
h₂ : ∀ (a : β), q a ↔ r (g a)
a : α
h : p a
⊢ p a

Tactic:
assumption
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
f : α → β
c₁ : Computable f
i₁ : Injective f
h₁ : ∀ (a : α), p a ↔ q (f a)
g : β → γ
c₂ : Computable g
i₂ : Injective g
h₂ : ∀ (a : β), q a ↔ r (g a)
a : α
h : r ((g ∘ f) a)
rwa : q (f a)
rwa₁ rwa₂ rwa₃ rwa₄ : r (g (f a))
⊢ p a

Tactic:
rwa [h₁, h₂]
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
e : α ≃ β
q : β → Prop
h : Computable.{u_1, u_2} (α := α) (σ := β) (⇑e : (a : α) → β)
⊢ OneOneReducible.{u_1, u_2} (α := α) (q ∘ (⇑e : (a : α) → β)) q

Tactic:
OneOneReducible.mk _ h e.injective

Premises used: OneOneReducible.mk, Equiv.injective
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
e : α ≃ β
q : β → Prop
h : Computable.{u_2, u_1} (α := β) (σ := α) (⇑e.symm : (a : β) → α)
⊢ OneOneReducible.{u_2, u_1} (α := β) (β := α)
    (comp.{u_2 + 1, u_1 + 1, 1} (β := α) (q ∘ (⇑e : (a : α) → β)) (⇑e.symm : (a : β) → α)) (q ∘ (⇑e : (a : α) → β))

Tactic:
OneOneReducible.of_equiv _ h

Premises used: OneOneReducible.of_equiv
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
e : α ≃ β
q : β → Prop
h : Computable.{u_2, u_1} (α := β) (σ := α) (⇑e.symm : (a : β) → α)
h₁ : q = comp.{u_2 + 1, u_1 + 1, 1} (β := α) (q ∘ (⇑e : (a : α) → β)) (⇑e.symm : (a : β) → α)
⊢ OneOneReducible.{u_2, u_1} (β := α) q (q ∘ (⇑e : (a : α) → β))

Tactic:
convert! OneOneReducible.of_equiv _ h

Premises used: OneOneReducible.of_equiv
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
e : α ≃ β
q : β → Prop
h : Computable.{u_2, u_1} (α := β) (σ := α) (⇑e.symm : (a : β) → α)
h₁ : ∀ (x : β), q x = comp.{u_2 + 1, u_1 + 1, 1} (β := α) (q ∘ (⇑e : (a : α) → β)) (⇑e.symm : (a : β) → α) x
⊢ q = comp.{u_2 + 1, u_1 + 1, 1} (β := α) (q ∘ (⇑e : (a : α) → β)) (⇑e.symm : (a : β) → α)

Tactic:
funext
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
e : α ≃ β
q : β → Prop
h : Computable.{u_2, u_1} (α := β) (σ := α) (⇑e.symm : (a : β) → α)
x : β
⊢ q x = comp.{u_2 + 1, u_1 + 1, 1} (β := α) (q ∘ (⇑e : (a : α) → β)) (⇑e.symm : (a : β) → α) x

Tactic:
simp
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
p : α → Prop
q : β → Prop
h₁ : p ≤₀ q
h₂ : ComputablePred q
rcases : ∀ (f : α → β) (c : Computable f) (hf : ∀ (a : α), p a ↔ q (f a)), ComputablePred p
⊢ ComputablePred p

Tactic:
rcases h₁ with ⟨f, c, hf⟩
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
p : α → Prop
q : β → Prop
h₂ : ComputablePred q
f : α → β
c : Computable f
hf : ∀ (a : α), p a ↔ q (f a)
rw : ComputablePred fun (a : α) ↦ q (f a)
⊢ ComputablePred p

Tactic:
rw [show p = fun a => q (f a) from Set.ext hf]

Premises used: Set.ext
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
p : α → Prop
q : β → Prop
h₂ : ComputablePred q
f : α → β
c : Computable f
hf : ∀ (a : α), p a ↔ q (f a)
rcases :
  ∀ (g : β → Bool) (hg : Computable g) (h₂ : ComputablePred fun (a : β) ↦ g a = true)
    (hf : ∀ (a : α), p a ↔ (fun (a : β) ↦ g a = true) (f a)),
    ComputablePred fun (a : α) ↦ (fun (a : β) ↦ g a = true) (f a)
⊢ ComputablePred fun (a : α) ↦ q (f a)

Tactic:
rcases computable_iff.1 h₂ with ⟨g, hg, rfl⟩

Premises used: Iff.mp, ComputablePred.computable_iff, rfl
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
p : α → Prop
f : α → β
c : Computable f
g : β → Bool
hg : Computable g
h₂ : ComputablePred fun (a : β) ↦ g a = true
hf : ∀ (a : α), p a ↔ (fun (a : β) ↦ g a = true) (f a)
⊢ DecidablePred fun (a : α) ↦ (fun (a : β) ↦ g a = true) (f a)

Tactic:
infer_instance