awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
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 ()
have 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
Tactic: refine
    (Partrec.cond hf (Decidable.Partrec.const' (Part.some ())) Partrec.none).of_eq fun n =>
      Part.ext fun a => ?_
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
Goal:
α : Type u_1
inst : Primcodable α
f : α → Bool
hf : Computable f
hp : ComputablePred fun (a : α) ↦ f a = true
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
have 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 a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
Goal:
α : Type u_1
inst : Primcodable α
f : α → Bool
hf : Computable f
hp : ComputablePred fun (a : α) ↦ f a = true
n : α
⊢ (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
have 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
Tactic: cases f n
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
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
⊢ (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
have 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
Tactic: cases f n
-- Lean 4 proof step from Mathlib.Computability.RE (hypothesis)
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
⊢ x = y
have hx₁ : 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
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Computability.RE (hypothesis)
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
⊢ x = y
have hy₁ : ¬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
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
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
⊢ Computable (σ := Bool) fun (a : α) ↦ decide (p a)
have 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)
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)
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
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)
have refine : ∀ (n : α), (fun (a : α) ↦ decide (p a)) n ∈ k n
Tactic: refine Partrec.of_eq pk fun n => Part.eq_some_iff.2 ?_
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
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 : α
⊢ (fun (a : α) ↦ decide (p a)) n ∈ k n
have 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)
Tactic: rw [hk]
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
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 : α
⊢ 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)
have simp : p n ∨ ¬p 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]
-- Lean 4 proof step from Mathlib.Computability.RecursiveIn (goal)
Goal:
O O' : Set (ℕ →. ℕ)
f : ℕ →. ℕ
hf : Nat.RecursiveIn O f
hO : ∀ g ∈ O, Nat.RecursiveIn O' g
⊢ Nat.RecursiveIn O' f
have zero : Nat.RecursiveIn O' fun (x : ℕ) ↦ 0
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
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Computability.RecursiveIn (goal)
Goal:
O O' : Set (ℕ →. ℕ)
f : ℕ →. ℕ
hf : Nat.RecursiveIn O f
hO : ∀ g ∈ O, Nat.RecursiveIn O' g
zero : Nat.RecursiveIn O' fun (x : ℕ) ↦ 0
⊢ Nat.RecursiveIn O' f
have succ : Nat.RecursiveIn O' (↑Nat.succ : ℕ →. ℕ)
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
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Computability.RecursiveIn (goal)
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 : ℕ →. ℕ)
⊢ Nat.RecursiveIn O' f
have left : Nat.RecursiveIn O' fun (n : ℕ) ↦ (↑(Option.some (unpair n).1) : Part ℕ)
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
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Computability.RecursiveIn (goal)
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 ℕ)
⊢ Nat.RecursiveIn O' f
have right : Nat.RecursiveIn O' fun (n : ℕ) ↦ (↑(Option.some (unpair n).2) : Part ℕ)
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
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Computability.RecursiveIn (goal)
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
⊢ Nat.RecursiveIn O' f
have 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
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
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Computability.RecursiveIn (goal)
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
⊢ Nat.RecursiveIn O' f
have 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
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
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Computability.RecursiveIn (goal)
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
⊢ Nat.RecursiveIn O' f
have 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
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
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Computability.RecursiveIn (goal)
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
⊢ Nat.RecursiveIn O' f
have 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)
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
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Computability.RecursiveIn (goal)
Goal:
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
hO : ∀ g ∈ O, Nat.Partrec g
hf : Nat.RecursiveIn O f
⊢ Nat.Partrec f
have zero : Nat.Partrec fun (x : ℕ) ↦ 0
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
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Computability.RecursiveIn (goal)
Goal:
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
hO : ∀ g ∈ O, Nat.Partrec g
hf : Nat.RecursiveIn O f
zero : Nat.Partrec fun (x : ℕ) ↦ 0
⊢ Nat.Partrec f
have succ : Nat.Partrec (↑Nat.succ : ℕ →. ℕ)
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
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Computability.RecursiveIn (goal)
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 : ℕ →. ℕ)
⊢ Nat.Partrec f
have left : Nat.Partrec fun (n : ℕ) ↦ (↑(Option.some (unpair n).1) : Part ℕ)
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
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Computability.RecursiveIn (goal)
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 ℕ)
⊢ Nat.Partrec f
have right : Nat.Partrec fun (n : ℕ) ↦ (↑(Option.some (unpair n).2) : Part ℕ)
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
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Computability.RecursiveIn (goal)
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
⊢ Nat.Partrec f
have 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
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
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Computability.RecursiveIn (goal)
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
⊢ Nat.Partrec f
have 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
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
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Computability.RecursiveIn (goal)
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
⊢ Nat.Partrec f
have 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
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
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Computability.RecursiveIn (goal)
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
⊢ Nat.Partrec f
have 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)
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
Cleared hypotheses: hf