awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
m : ℕ
IH : (y : ℕ) → lbp p y m → (∀ n < y, false ∈ p n) → { n : ℕ // true ∈ p n ∧ ∀ m < n, false ∈ p m }
al : ∀ n < m, false ∈ p n
n : ℕ
h₁ : true ∈ p n
h₂ : ∀ k < n, (p k).Dom
h₃ : m = n
⊢ (p n).Dom

Tactic:
exact h₁.fst

Premises used: Exists.fst
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
m : ℕ
IH : (y : ℕ) → lbp p y m → (∀ n < y, false ∈ p n) → { n : ℕ // true ∈ p n ∧ ∀ m < n, false ∈ p m }
al : ∀ n < m, false ∈ p n
n : ℕ
h₁ : true ∈ p n
h₂ : ∀ k < n, (p k).Dom
h₃ : n < m
⊢ (p m).Dom

Tactic:
injection mem_unique h₁ (al _ h₃)

Premises used: Part.mem_unique
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
H : ∃ (n : ℕ), true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
IH : (y : ℕ) → lbp p y m → (∀ n < y, false ∈ p n) → { n : ℕ // true ∈ p n ∧ ∀ m < n, false ∈ p m }
al : ∀ n < m, false ∈ p n
⊢ (p m).Dom

Tactic:
have pm : (p m).Dom := by
        rcases H with ⟨n, h₁, h₂⟩
        rcases lt_trichotomy m n with (h₃ | h₃ | h₃)
        · exact h₂ _ h₃
        · rw [h₃]
          exact h₁.fst
        · injection mem_unique h₁ (al _ h₃)
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
H : ∃ (n : ℕ), Bool.true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
IH : (y : ℕ) → lbp p y m → (∀ n < y, Bool.false ∈ p n) → { n : ℕ // Bool.true ∈ p n ∧ ∀ m < n, Bool.false ∈ p m }
al : ∀ n < m, Bool.false ∈ p n
pm : (p m).Dom
false : (e : (p m).get pm = Bool.false) → { n : ℕ // Bool.true ∈ p n ∧ ∀ m < n, Bool.false ∈ p m }
true : (e : (p m).get pm = Bool.true) → { n : ℕ // Bool.true ∈ p n ∧ ∀ m < n, Bool.false ∈ p m }
⊢ { n : ℕ // Bool.true ∈ p n ∧ ∀ m < n, Bool.false ∈ p m }

Tactic:
cases e : (p m).get pm

Premises used: Part.get
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
H : ∃ (n : ℕ), true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
IH : (y : ℕ) → lbp p y m → (∀ n < y, Bool.false ∈ p n) → { n : ℕ // true ∈ p n ∧ ∀ m < n, Bool.false ∈ p m }
al : ∀ n < m, Bool.false ∈ p n
pm : (p m).Dom
e : (p m).get pm = Bool.false
false : ∀ k ≤ m, Bool.false ∈ p k
⊢ { n : ℕ // true ∈ p n ∧ ∀ m < n, Bool.false ∈ p m }

Tactic:
suffices ∀ᵉ k ≤ m, false ∈ p k from IH _ ⟨rfl, this⟩ fun n h => this _ (le_of_lt_succ h)
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
H : ∃ (n : ℕ), true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
IH : (y : ℕ) → lbp p y m → (∀ n < y, Bool.false ∈ p n) → { n : ℕ // true ∈ p n ∧ ∀ m < n, Bool.false ∈ p m }
al : ∀ n < m, Bool.false ∈ p n
pm : (p m).Dom
e : (p m).get pm = Bool.false
n : ℕ
h : n ≤ m
false : ∀ (h : n < m), Bool.false ∈ p n
false₁ : ∀ (h : n = m), Bool.false ∈ p n
⊢ Bool.false ∈ p n

Tactic:
rcases h.lt_or_eq_dec with h | h

Premises used: LE.le.lt_or_eq_dec
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
H : ∃ (n : ℕ), true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
IH : (y : ℕ) → lbp p y m → (∀ n < y, false ∈ p n) → { n : ℕ // true ∈ p n ∧ ∀ m < n, false ∈ p m }
al : ∀ n < m, false ∈ p n
pm : (p m).Dom
e : (p m).get pm = false
n : ℕ
h_1 : n ≤ m
h : n < m
⊢ false ∈ p n

Tactic:
al _ h
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
H : ∃ (n : ℕ), true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
IH : (y : ℕ) → lbp p y m → (∀ n < y, false ∈ p n) → { n : ℕ // true ∈ p n ∧ ∀ m < n, false ∈ p m }
al : ∀ n < m, false ∈ p n
pm : (p m).Dom
e : (p m).get pm = false
n : ℕ
h_1 : n ≤ m
h : n < m
⊢ false ∈ p n

Tactic:
exact al _ h
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
H : ∃ (n : ℕ), true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
IH : (y : ℕ) → lbp p y m → (∀ n < y, Bool.false ∈ p n) → { n : ℕ // true ∈ p n ∧ ∀ m < n, Bool.false ∈ p m }
al : ∀ n < m, Bool.false ∈ p n
pm : (p m).Dom
e : (p m).get pm = Bool.false
n : ℕ
h_1 : n ≤ m
h : n = m
false : Bool.false ∈ p m
⊢ Bool.false ∈ p n

Tactic:
rw [h]
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
H : ∃ (n : ℕ), true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
IH : (y : ℕ) → lbp p y m → (∀ n < y, false ∈ p n) → { n : ℕ // true ∈ p n ∧ ∀ m < n, false ∈ p m }
al : ∀ n < m, false ∈ p n
pm : (p m).Dom
e : (p m).get pm = false
n : ℕ
h_1 : n ≤ m
h : n = m
⊢ false ∈ p m

Tactic:
⟨_, e⟩

Premises used: Part.Mem, Exists.intro
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
H : ∃ (n : ℕ), true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
IH : (y : ℕ) → lbp p y m → (∀ n < y, false ∈ p n) → { n : ℕ // true ∈ p n ∧ ∀ m < n, false ∈ p m }
al : ∀ n < m, false ∈ p n
pm : (p m).Dom
e : (p m).get pm = false
n : ℕ
h_1 : n ≤ m
h : n = m
⊢ false ∈ p m

Tactic:
exact ⟨_, e⟩
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
H : ∃ (n : ℕ), true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
IH : (y : ℕ) → lbp p y m → (∀ n < y, false ∈ p n) → { n : ℕ // true ∈ p n ∧ ∀ m < n, false ∈ p m }
al : ∀ n < m, false ∈ p n
pm : (p m).Dom
e : (p m).get pm = true
⊢ { n : ℕ // true ∈ p n ∧ ∀ m < n, false ∈ p m }

Tactic:
exact ⟨m, ⟨_, e⟩, al⟩
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
n : ℕ
h : n ∈ rfind p
⊢ true ∈ p n

Tactic:
h.snd ▸ (rfindX p h.fst).2.1

Premises used: Eq.rec, Nat.rfindX, Exists.fst, Exists.snd, And.left, Subtype.property
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
n : ℕ
h : n ∈ rfind p
⊢ ∀ {m : ℕ}, m < n → false ∈ p m

Tactic:
@(h.snd ▸ @((rfindX p h.fst).2.2))

Premises used: Eq.rec, Nat.rfindX, Exists.fst, Exists.snd, And.right, Subtype.property
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
⊢ (rfind p).Dom ↔ ∃ (n : ℕ), true ∈ p n ∧ ∀ {m : ℕ}, m < n → (p m).Dom

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
⊢ (rfind p).Dom ↔ ∃ (n : ℕ), true ∈ p n ∧ ∀ {m : ℕ}, m ≤ n → (p m).Dom

Tactic:
exists_congr fun _ =>
    and_congr_right fun pn =>
      ⟨fun H _ h => (Decidable.eq_or_lt_of_le h).elim (fun e => e.symm ▸ pn.fst) (H _), fun H _ h =>
        H (le_of_lt h)⟩

Premises used: le_of_lt, Eq.rec, Exists.fst, and_congr_right, exists_congr, Decidable.eq_or_lt_of_le, Iff.intro, Or.elim, Eq.symm
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
n : ℕ
h : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m
h₁ : true ∈ p n
h₂ : ∀ {m : ℕ}, m < n → false ∈ p m
let : ∀ (m : ℕ) (hm : m ∈ rfind p), n ∈ rfind p
⊢ n ∈ rfind p

Tactic:
let ⟨m, hm⟩ := dom_iff_mem.1 <| (@rfind_dom p).2 ⟨_, h₁, fun {m} mn => (h₂ mn).fst⟩
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
n : ℕ
h : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m
h₁ : true ∈ p n
h₂ : ∀ {m : ℕ}, m < n → false ∈ p m
m : ℕ
hm : m ∈ rfind p
inl : ∀ (h : m < n), n ∈ rfind p
inr : ∀ (h : m = n), n ∈ rfind p
inr₁ : ∀ (h : n < m), n ∈ rfind p
⊢ n ∈ rfind p

Tactic:
rcases lt_trichotomy m n with (h | h | h)

Premises used: lt_trichotomy
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
n : ℕ
h_1 : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m
h₁ : true ∈ p n
h₂ : ∀ {m : ℕ}, m < n → false ∈ p m
m : ℕ
hm : m ∈ rfind p
h : m < n
⊢ n ∈ rfind p

Tactic:
injection mem_unique (h₂ h) (rfind_spec hm)

Premises used: Nat.rfind_spec, Part.mem_unique
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
n : ℕ
h_1 : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m
h₁ : true ∈ p n
h₂ : ∀ {m : ℕ}, m < n → false ∈ p m
m : ℕ
hm : m ∈ rfind p
h : m = n
inr inr₁ inr₂ inr₃ : m ∈ rfind p
⊢ n ∈ rfind p

Tactic:
rwa [← h]
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
n : ℕ
h_1 : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m
h₁ : true ∈ p n
h₂ : ∀ {m : ℕ}, m < n → false ∈ p m
m : ℕ
hm : m ∈ rfind p
h : n < m
⊢ n ∈ rfind p

Tactic:
injection mem_unique h₁ (rfind_min hm h)

Premises used: Nat.rfind_min, Part.mem_unique
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ → Bool
m : ℕ
pm : p m = true
this : true ∈ (↑p : ℕ →. Bool) m
n : ℕ
hn : n ∈ rfind (↑p : ℕ →. Bool)
h : m < n
⊢ False

Tactic:
injection mem_unique this (rfind_min hn h)

Premises used: Nat.rfind_min, Part.mem_unique
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
p0 : p 0 = Part.none
⊢ rfind p = Part.none

Tactic:
eq_none_iff.2 fun _ h =>
    let ⟨_, _, h₂⟩ := rfind_dom'.1 h.fst
    (p0 ▸ h₂ (zero_le _) : (@Part.none Bool).Dom)

Premises used: Iff.mpr, Nat.zero_le, False, Eq.rec, Exists.fst, Part.eq_none_iff, Nat.rfind_dom', Iff.mp, _private.0.Nat.rfind_zero_none.match_1
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
f : ℕ → Option α
a : α
h : a ∈ rfindOpt f
⊢ ∃ (n : ℕ), a ∈ f n

Tactic:
let ⟨n, _, h₂⟩ := mem_bind_iff.1 h
  ⟨n, mem_coe.1 h₂⟩

Premises used: Part.mem_bind_iff, Membership.mem, Exists, Part.mem_coe, _private.0.Nat.rfindOpt_spec.match_1, Exists.intro, Iff.mp
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
f : ℕ → Option α
h : ∃ (n : ℕ) (a : α), a ∈ f n
⊢ ∃ (n : ℕ), (f n).isSome = true

Tactic:
have h' : ∃ n, (f n).isSome := h.imp fun n => Option.isSome_iff_exists.2
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
f : ℕ → Option α
h : ∃ (n : ℕ) (a : α), a ∈ f n
h' : ∃ (n : ℕ), (f n).isSome = true
⊢ (f (Nat.find (p := fun (n : ℕ) ↦ (f n).isSome = true) h')).isSome = true

Tactic:
have s := Nat.find_spec h'
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
f : ℕ → Option α
h : ∃ (n : ℕ) (a : α), a ∈ f n
h' : ∃ (n : ℕ), (f n).isSome = true
s : (f (Nat.find (p := fun (n : ℕ) ↦ (f n).isSome = true) h')).isSome = true
⊢ Membership.mem (γ := Part Bool)
    ((fun (n : ℕ) ↦ (↑(Option.some (f n).isSome) : Part Bool)) (Nat.find (p := fun (n : ℕ) ↦ (f n).isSome = true) h'))
    true

Tactic:
simpa using s.symm

Premises used: Eq.symm
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
f : ℕ → Option α
h : ∃ (n : ℕ) (a : α), a ∈ f n
h' : ∃ (n : ℕ), (f n).isSome = true
s : (f (Nat.find (p := fun (n : ℕ) ↦ (f n).isSome = true) h')).isSome = true
⊢ (rfind fun (n : ℕ) ↦ (↑(Option.some (f n).isSome) : Part Bool)).Dom

Tactic:
have fd : (rfind fun n => (f n).isSome).Dom :=
      ⟨Nat.find h', by simpa using s.symm, fun _ _ => trivial⟩
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
f : ℕ → Option α
h : ∃ (n : ℕ) (a : α), a ∈ f n
h' : ∃ (n : ℕ), (f n).isSome = true
s : (f (Nat.find (p := fun (n : ℕ) ↦ (f n).isSome = true) h')).isSome = true
fd : (rfind fun (n : ℕ) ↦ (↑(Option.some (f n).isSome) : Part Bool)).Dom
⊢ (rfindOpt f).Dom

Tactic:
⟨fd, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
f : ℕ → Option α
h : ∃ (n : ℕ) (a : α), a ∈ f n
h' : ∃ (n : ℕ), (f n).isSome = true
s : (f (Nat.find (p := fun (n : ℕ) ↦ (f n).isSome = true) h')).isSome = true
fd : (rfind fun (n : ℕ) ↦ (↑(Option.some (f n).isSome) : Part Bool)).Dom
refine :
  Dom.{u_1} (α := α)
    ((fun (b : (rfind fun (n : ℕ) ↦ (↑(Option.some (f n).isSome) : Part Bool)).Dom) ↦
        ((fun (n : ℕ) ↦ (↑(f n) : Part α)) ((rfind fun (n : ℕ) ↦ (↑(Option.some (f n).isSome) : Part Bool)).get b) :
          Part α))
      fd)
⊢ (rfindOpt f).Dom

Tactic:
refine ⟨fd, ?_⟩
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
f : ℕ → Option α
h : ∃ (n : ℕ) (a : α), a ∈ f n
h' : ∃ (n : ℕ), (f n).isSome = true
s : (f (Nat.find (p := fun (n : ℕ) ↦ (f n).isSome = true) h')).isSome = true
fd : (rfind fun (n : ℕ) ↦ (↑(Option.some (f n).isSome) : Part Bool)).Dom
⊢ true ∈
    (↑(Option.some (f ((rfind fun (n : ℕ) ↦ (↑(Option.some (f n).isSome) : Part Bool)).get fd)).isSome) : Part Bool)

Tactic:
have := rfind_spec (get_mem fd)
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
f : ℕ → Option α
h : ∃ (n : ℕ) (a : α), a ∈ f n
h' : ∃ (n : ℕ), (f n).isSome = true
s : (f (Nat.find (p := fun (n : ℕ) ↦ (f n).isSome = true) h')).isSome = true
fd : (rfind fun (n : ℕ) ↦ (↑(Option.some (f n).isSome) : Part Bool)).Dom
this :
  true ∈
    (↑(Option.some (f ((rfind fun (n : ℕ) ↦ (↑(Option.some (f n).isSome) : Part Bool)).get fd)).isSome) : Part Bool)
⊢ Dom.{u_1} (α := α)
    ((fun (b : (rfind fun (n : ℕ) ↦ (↑(Option.some (f n).isSome) : Part Bool)).Dom) ↦
        ((fun (n : ℕ) ↦ (↑(f n) : Part α)) ((rfind fun (n : ℕ) ↦ (↑(Option.some (f n).isSome) : Part Bool)).get b) :
          Part α))
      fd)

Tactic:
simpa using this
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
f : ℕ → Option α
H : ∀ {a : α} {m n : ℕ}, m ≤ n → a ∈ f m → a ∈ f n
a : α
h_1 : ∃ (n : ℕ), a ∈ f n
n : ℕ
h : a ∈ f n
⊢ (rfindOpt f).Dom

Tactic:
have h' := rfindOpt_dom.2 ⟨_, _, h⟩
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
f : ℕ → Option α
H : ∀ {a : α} {m n : ℕ}, m ≤ n → a ∈ f m → a ∈ f n
a : α
h_1 : ∃ (n : ℕ), a ∈ f n
n : ℕ
h : a ∈ f n
h' : (rfindOpt f).Dom
obtain : ∀ (k : ℕ) (hk : (rfindOpt f).get h' ∈ f k), a ∈ rfindOpt f
⊢ a ∈ rfindOpt f

Tactic:
obtain ⟨k, hk⟩ := rfindOpt_spec ⟨h', rfl⟩

Premises used: Nat.rfindOpt_spec, Exists.intro, rfl
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
f : ℕ → Option α
H : ∀ {a : α} {m n : ℕ}, m ≤ n → a ∈ f m → a ∈ f n
a : α
h_1 : ∃ (n : ℕ), a ∈ f n
n : ℕ
h : a ∈ f n
h' : (rfindOpt f).Dom
k : ℕ
hk : (rfindOpt f).get h' ∈ f k
⊢ Option.some a = Option.some ((rfindOpt f).get h')

Tactic:
have := (H (le_max_left _ _) h).symm.trans (H (le_max_right _ _) hk)
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
f : ℕ → Option α
H : ∀ {a : α} {m n : ℕ}, m ≤ n → a ∈ f m → a ∈ f n
a : α
h_1 : ∃ (n : ℕ), a ∈ f n
n : ℕ
h : a ∈ f n
h' : (rfindOpt f).Dom
k : ℕ
hk : (rfindOpt f).get h' ∈ f k
this : Option.some a = Option.some ((rfindOpt f).get h')
⊢ a = (rfindOpt f).get h'

Tactic:
simp at this
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
f : ℕ → Option α
H : ∀ {a : α} {m n : ℕ}, m ≤ n → a ∈ f m → a ∈ f n
a : α
h_1 : ∃ (n : ℕ), a ∈ f n
n : ℕ
h : a ∈ f n
h' : (rfindOpt f).Dom
k : ℕ
hk : (rfindOpt f).get h' ∈ f k
this : a = (rfindOpt f).get h'
⊢ a ∈ rfindOpt f

Tactic:
simp [this, get_mem]

Premises used: Part.get_mem
-- Module: Mathlib.Computability.Partrec
Goal:
f g : ℕ →. ℕ
hf : Nat.Partrec f
H : ∀ (n : ℕ), f n = g n
⊢ Nat.Partrec g

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

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

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

Premises used: Iff.mpr, Part.eq_some_iff, Nat.Partrec.of_eq
-- Module: Mathlib.Computability.Partrec
Goal:
f : ℕ → ℕ
⊢ Nat.Partrec (↑fun (x : ℕ) ↦ 0 : ℕ →. ℕ)

Tactic:
zero

Premises used: Part.some, Nat.Partrec.zero, PFun.pure, PFun.lift
-- Module: Mathlib.Computability.Partrec
Goal:
f : ℕ → ℕ
⊢ Nat.Partrec (↑fun (x : ℕ) ↦ 0 : ℕ →. ℕ)

Tactic:
exact zero

Premises used: Nat.Partrec.zero
-- Module: Mathlib.Computability.Partrec
Goal:
f : ℕ → ℕ
⊢ Nat.Partrec (↑Nat.succ : ℕ →. ℕ)

Tactic:
succ

Premises used: Nat.Partrec.succ
-- Module: Mathlib.Computability.Partrec
Goal:
f : ℕ → ℕ
⊢ Nat.Partrec (↑Nat.succ : ℕ →. ℕ)

Tactic:
exact succ

Premises used: Nat.Partrec.succ
-- Module: Mathlib.Computability.Partrec
Goal:
f : ℕ → ℕ
⊢ Nat.Partrec (↑fun (n : ℕ) ↦ (unpair n).1 : ℕ →. ℕ)

Tactic:
left

Premises used: Nat.Partrec.left
-- Module: Mathlib.Computability.Partrec
Goal:
f : ℕ → ℕ
⊢ Nat.Partrec (↑fun (n : ℕ) ↦ (unpair n).1 : ℕ →. ℕ)

Tactic:
exact left

Premises used: Nat.Partrec.left
-- Module: Mathlib.Computability.Partrec
Goal:
f : ℕ → ℕ
⊢ Nat.Partrec (↑fun (n : ℕ) ↦ (unpair n).2 : ℕ →. ℕ)

Tactic:
right

Premises used: Nat.Partrec.right
-- Module: Mathlib.Computability.Partrec
Goal:
f : ℕ → ℕ
⊢ Nat.Partrec (↑fun (n : ℕ) ↦ (unpair n).2 : ℕ →. ℕ)

Tactic:
exact right

Premises used: Nat.Partrec.right
-- Module: Mathlib.Computability.Partrec
Goal:
f f_1 g : ℕ → ℕ
h : Nat.Primrec f_1
h_1 : Nat.Primrec g
pf : Nat.Partrec (↑f_1 : ℕ →. ℕ)
pg : Nat.Partrec (↑g : ℕ →. ℕ)
⊢ Nat.Partrec (↑fun (n : ℕ) ↦ Nat.pair (f_1 n) (g n) : ℕ →. ℕ)

Tactic:
(pf.pair pg).of_eq_tot fun n => ?_

Premises used: Nat.Partrec.pair, Nat.Partrec.of_eq_tot
-- Module: Mathlib.Computability.Partrec
Goal:
f f_1 g : ℕ → ℕ
h : Nat.Primrec f_1
h_1 : Nat.Primrec g
pf : Nat.Partrec (↑f_1 : ℕ →. ℕ)
pg : Nat.Partrec (↑g : ℕ →. ℕ)
pair : ∀ (n : ℕ), Nat.pair (f_1 n) (g n) ∈ Nat.pair <$> (↑f_1 : ℕ →. ℕ) n <*> (↑g : ℕ →. ℕ) n
⊢ Nat.Partrec (↑fun (n : ℕ) ↦ Nat.pair (f_1 n) (g n) : ℕ →. ℕ)

Tactic:
refine (pf.pair pg).of_eq_tot fun n => ?_

Premises used: Nat.Partrec.pair, Nat.Partrec.of_eq_tot
-- Module: Mathlib.Computability.Partrec
Goal:
f f_1 g : ℕ → ℕ
h : Nat.Primrec f_1
h_1 : Nat.Primrec g
pf : Nat.Partrec (↑f_1 : ℕ →. ℕ)
pg : Nat.Partrec (↑g : ℕ →. ℕ)
n : ℕ
⊢ Nat.pair (f_1 n) (g n) ∈ Nat.pair <$> (↑f_1 : ℕ →. ℕ) n <*> (↑g : ℕ →. ℕ) n

Tactic:
simp [Seq.seq]

Premises used: Seq.seq
-- Module: Mathlib.Computability.Partrec
Goal:
f f_1 g : ℕ → ℕ
h : Nat.Primrec f_1
h_1 : Nat.Primrec g
pf : Nat.Partrec (↑f_1 : ℕ →. ℕ)
pg : Nat.Partrec (↑g : ℕ →. ℕ)
n : ℕ
⊢ f_1 (g n) ∈ (↑g : ℕ →. ℕ) n >>= (↑f_1 : ℕ →. ℕ)

Tactic:
simp
-- Module: Mathlib.Computability.Partrec
Goal:
f f_1 g : ℕ → ℕ
h : Nat.Primrec f_1
h_1 : Nat.Primrec g
pf : Nat.Partrec (↑f_1 : ℕ →. ℕ)
pg : Nat.Partrec (↑g : ℕ →. ℕ)
⊢ Nat.Partrec (↑fun (n : ℕ) ↦ f_1 (g n) : ℕ →. ℕ)

Tactic:
refine (pf.comp pg).of_eq_tot fun n => (by simp)

Premises used: Nat.Partrec.comp, Nat.Partrec.of_eq_tot
-- Module: Mathlib.Computability.Partrec
Goal:
f f_1 g : ℕ → ℕ
h : Nat.Primrec f_1
h_1 : Nat.Primrec g
pf : Nat.Partrec (↑f_1 : ℕ →. ℕ)
pg : Nat.Partrec (↑g : ℕ →. ℕ)
⊢ Nat.Partrec
    (↑(unpaired fun (z n : ℕ) ↦
          Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f_1 z) (fun (y IH : ℕ) ↦ g (Nat.pair z (Nat.pair y IH))) n) :
      ℕ →. ℕ)

Tactic:
(pf.prec pg).of_eq_tot fun n => ?_

Premises used: Nat.Partrec.prec, Nat.Partrec.of_eq_tot
-- Module: Mathlib.Computability.Partrec
Goal:
f f_1 g : ℕ → ℕ
h : Nat.Primrec f_1
h_1 : Nat.Primrec g
pf : Nat.Partrec (↑f_1 : ℕ →. ℕ)
pg : Nat.Partrec (↑g : ℕ →. ℕ)
prec :
  ∀ (n : ℕ),
    Membership.mem (γ := Part ℕ)
      (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)
        n)
      (unpaired
        (fun (z n : ℕ) ↦
          Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f_1 z) (fun (y IH : ℕ) ↦ g (Nat.pair z (Nat.pair y IH))) n)
        n)
⊢ Nat.Partrec
    (↑(unpaired fun (z n : ℕ) ↦
          Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f_1 z) (fun (y IH : ℕ) ↦ g (Nat.pair z (Nat.pair y IH))) n) :
      ℕ →. ℕ)

Tactic:
refine (pf.prec pg).of_eq_tot fun n => ?_

Premises used: Nat.Partrec.prec, Nat.Partrec.of_eq_tot
-- Module: Mathlib.Computability.Partrec
Goal:
f f_1 g : ℕ → ℕ
h : Nat.Primrec f_1
h_1 : Nat.Primrec g
pf : Nat.Partrec (↑f_1 : ℕ →. ℕ)
pg : Nat.Partrec (↑g : ℕ →. ℕ)
n : ℕ
prec :
  Membership.mem (α := ℕ) (γ := Part ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (Part.some (f_1 (unpair n).1))
        (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ Part.some (g (Nat.pair (unpair n).1 (Nat.pair y i))))
        (unpair n).2 :
      Part ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f_1 (unpair n).1) (fun (y IH : ℕ) ↦ g (Nat.pair (unpair n).1 (Nat.pair y IH)))
        (unpair n).2 :
      ℕ)
⊢ Membership.mem (γ := Part ℕ)
    (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)
      n)
    (unpaired
      (fun (z n : ℕ) ↦ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f_1 z) (fun (y IH : ℕ) ↦ g (Nat.pair z (Nat.pair y IH))) n)
      n)

Tactic:
simp only [unpaired, PFun.coe_val, bind_eq_bind]

Premises used: PFun.coe_val, Nat.unpaired, Part.bind_eq_bind
-- Module: Mathlib.Computability.Partrec
Goal:
f f_1 g : ℕ → ℕ
h : Nat.Primrec f_1
h_1 : Nat.Primrec g
pf : Nat.Partrec (↑f_1 : ℕ →. ℕ)
pg : Nat.Partrec (↑g : ℕ →. ℕ)
n : ℕ
⊢ Membership.mem (α := ℕ) (γ := Part ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (Part.some (f_1 (unpair n).1))
        (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ Part.some (g (Nat.pair (unpair n).1 (Nat.pair y i)))) 0 :
      Part ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f_1 (unpair n).1) (fun (y IH : ℕ) ↦ g (Nat.pair (unpair n).1 (Nat.pair y IH)))
        0 :
      ℕ)

Tactic:
simp
-- Module: Mathlib.Computability.Partrec
Goal:
f f_1 g : ℕ → ℕ
h : Nat.Primrec f_1
h_1 : Nat.Primrec g
pf : Nat.Partrec (↑f_1 : ℕ →. ℕ)
pg : Nat.Partrec (↑g : ℕ →. ℕ)
n m : ℕ
IH :
  Membership.mem (α := ℕ) (γ := Part ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (Part.some (f_1 (unpair n).1))
        (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ Part.some (g (Nat.pair (unpair n).1 (Nat.pair y i)))) m :
      Part ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f_1 (unpair n).1) (fun (y IH : ℕ) ↦ g (Nat.pair (unpair n).1 (Nat.pair y IH)))
        m :
      ℕ)
prec :
  ∃ (a : ℕ),
    Membership.mem (γ := Part ℕ)
        (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (Part.some (f_1 (unpair n).1))
            (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ Part.some (g (Nat.pair (unpair n).1 (Nat.pair y i)))) m :
          Part ℕ)
        a ∧
      g
          (Nat.pair (unpair n).1
            (Nat.pair m
              (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f_1 (unpair n).1)
                (fun (y IH : ℕ) ↦ g (Nat.pair (unpair n).1 (Nat.pair y IH))) m))) =
        g (Nat.pair (unpair n).1 (Nat.pair m a))
⊢ Membership.mem (α := ℕ) (γ := Part ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (Part.some (f_1 (unpair n).1))
        (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ Part.some (g (Nat.pair (unpair n).1 (Nat.pair y i))))
        (m + 1) :
      Part ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f_1 (unpair n).1) (fun (y IH : ℕ) ↦ g (Nat.pair (unpair n).1 (Nat.pair y IH)))
        (m + 1) :
      ℕ)

Tactic:
simp only [mem_bind_iff, mem_some_iff]

Premises used: Part.mem_bind_iff, Part.mem_some_iff
-- Module: Mathlib.Computability.Partrec
Goal:
f f_1 g : ℕ → ℕ
h : Nat.Primrec f_1
h_1 : Nat.Primrec g
pf : Nat.Partrec (↑f_1 : ℕ →. ℕ)
pg : Nat.Partrec (↑g : ℕ →. ℕ)
n m : ℕ
IH :
  Membership.mem (α := ℕ) (γ := Part ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (Part.some (f_1 (unpair n).1))
        (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ Part.some (g (Nat.pair (unpair n).1 (Nat.pair y i)))) m :
      Part ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f_1 (unpair n).1) (fun (y IH : ℕ) ↦ g (Nat.pair (unpair n).1 (Nat.pair y IH)))
        m :
      ℕ)
⊢ ∃ (a : ℕ),
    Membership.mem (γ := Part ℕ)
        (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (Part.some (f_1 (unpair n).1))
            (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ Part.some (g (Nat.pair (unpair n).1 (Nat.pair y i)))) m :
          Part ℕ)
        a ∧
      g
          (Nat.pair (unpair n).1
            (Nat.pair m
              (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f_1 (unpair n).1)
                (fun (y IH : ℕ) ↦ g (Nat.pair (unpair n).1 (Nat.pair y IH))) m))) =
        g (Nat.pair (unpair n).1 (Nat.pair m a))

Tactic:
⟨_, IH, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Computability.Partrec
Goal:
f f_1 g : ℕ → ℕ
h : Nat.Primrec f_1
h_1 : Nat.Primrec g
pf : Nat.Partrec (↑f_1 : ℕ →. ℕ)
pg : Nat.Partrec (↑g : ℕ →. ℕ)
n m : ℕ
IH :
  Membership.mem (α := ℕ) (γ := Part ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (Part.some (f_1 (unpair n).1))
        (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ Part.some (g (Nat.pair (unpair n).1 (Nat.pair y i)))) m :
      Part ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f_1 (unpair n).1) (fun (y IH : ℕ) ↦ g (Nat.pair (unpair n).1 (Nat.pair y IH)))
        m :
      ℕ)
⊢ ∃ (a : ℕ),
    Membership.mem (γ := Part ℕ)
        (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (Part.some (f_1 (unpair n).1))
            (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ Part.some (g (Nat.pair (unpair n).1 (Nat.pair y i)))) m :
          Part ℕ)
        a ∧
      g
          (Nat.pair (unpair n).1
            (Nat.pair m
              (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f_1 (unpair n).1)
                (fun (y IH : ℕ) ↦ g (Nat.pair (unpair n).1 (Nat.pair y IH))) m))) =
        g (Nat.pair (unpair n).1 (Nat.pair m a))

Tactic:
exact ⟨_, IH, rfl⟩