awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
x : List α
S S' : Set σ
h : Disjoint S (List.foldl M.reverse.stepSet S' x)
⊢ Disjoint S' (List.foldr (fun (x : α) (y : Set σ) ↦ M.stepSet y x) S x)
have nil : ∀ {S S' : Set σ} (h : Disjoint S (List.foldl M.reverse.stepSet S' [])),
  Disjoint S' (List.foldr (fun (x : α) (y : Set σ) ↦ M.stepSet y x) S [])
Tactic: induction x generalizing S S' with
  | nil =>
    rw [disjoint_comm]
    exact h
  | cons x xs ih =>
    rw [List.foldl_cons] at h
    rw [List.foldr_cons, ← NFA.disjoint_stepSet_reverse, disjoint_comm]
    exact ih h
Cleared hypotheses: x, S, S', h
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
x : List α
S S' : Set σ
h : Disjoint S (List.foldl M.reverse.stepSet S' x)
nil :
  ∀ {S S' : Set σ} (h : Disjoint S (List.foldl M.reverse.stepSet S' [])),
    Disjoint S' (List.foldr (fun (x : α) (y : Set σ) ↦ M.stepSet y x) S [])
⊢ Disjoint S' (List.foldr (fun (x : α) (y : Set σ) ↦ M.stepSet y x) S x)
have cons : ∀ (x : α) (xs : List α)
  (ih :
    ∀ {S S' : Set σ} (h : Disjoint S (List.foldl M.reverse.stepSet S' xs)),
      Disjoint S' (List.foldr (fun (x : α) (y : Set σ) ↦ M.stepSet y x) S xs))
  {S S' : Set σ} (h : Disjoint S (List.foldl M.reverse.stepSet S' (x :: xs))),
  Disjoint S' (List.foldr (fun (x : α) (y : Set σ) ↦ M.stepSet y x) S (x :: xs))
Tactic: induction x generalizing S S' with
  | nil =>
    rw [disjoint_comm]
    exact h
  | cons x xs ih =>
    rw [List.foldl_cons] at h
    rw [List.foldr_cons, ← NFA.disjoint_stepSet_reverse, disjoint_comm]
    exact ih h
Cleared hypotheses: x, S, S', h
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
L : Language α
h : L.IsRegular
σ : Type
w : Fintype σ
M : DFA α σ
hM : M.accepts = L
⊢ M.toNFA.reverse.toDFA.accepts = L.reverse
have h₁ : ∀ (x : List α), x ∈ M.toNFA.reverse.toDFA.accepts ↔ x ∈ L.reverse
Tactic: ext
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
p : ℕ →. Bool
H : ∃ (n : ℕ), true ∈ p n ∧ ∀ k < n, (p k).Dom
⊢ ∀ (a : ℕ), Acc (lbp p) a
have let : ∀ (n : ℕ) (pn : true ∈ p n ∧ ∀ k < n, (p k).Dom) (a : ℕ), Acc (lbp p) a
Tactic: let ⟨n, pn⟩ := H
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
p : ℕ →. Bool
H : ∃ (n : ℕ), true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
⊢ ∀ (a : ℕ), Acc (lbp p) a
have suffices : ∀ (m k : ℕ), n ≤ k + m → Acc (lbp p) k
Tactic: suffices ∀ m k, n ≤ k + m → Acc (lbp p) k by exact fun a => this _ _ (Nat.le_add_left _ _)
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
p : ℕ →. Bool
H : ∃ (n : ℕ), true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
k : ℕ
kn : n ≤ k + 0
⊢ Acc (lbp p) k
have zero : ∀ (y : ℕ) (r : lbp p y k), Acc (lbp p) y
Tactic: refine ⟨_, fun y r => ?_⟩
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
p : ℕ →. Bool
H : ∃ (n : ℕ), true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
k : ℕ
kn : n ≤ k + 0
y : ℕ
r : lbp p y k
⊢ Acc (lbp p) y
have zero : ∀ (a : ∀ k_1 ≤ k, false ∈ p k_1), Acc (lbp p) (k + 1)
Tactic: rcases r with ⟨rfl, a⟩
Cleared hypotheses: y, r
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
p : ℕ →. Bool
H : ∃ (n : ℕ), true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
IH : ∀ (k : ℕ) (kn : n ≤ k + m), Acc (lbp p) k
k : ℕ
kn : n ≤ k + (m + 1)
⊢ Acc (lbp p) k
have succ : ∀ (y : ℕ) (r : lbp p y k), Acc (lbp p) y
Tactic: refine ⟨_, fun y r => ?_⟩
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
p : ℕ →. Bool
H : ∃ (n : ℕ), true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
IH : ∀ (k : ℕ) (kn : n ≤ k + m), Acc (lbp p) k
k : ℕ
kn : n ≤ k + (m + 1)
y : ℕ
r : lbp p y k
⊢ Acc (lbp p) y
have succ : ∀ (a : ∀ k_1 ≤ k, false ∈ p k_1), Acc (lbp p) (k + 1)
Tactic: rcases r with ⟨rfl, a⟩
Cleared hypotheses: y, r
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
p : ℕ →. Bool
H : ∃ (n : ℕ), true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
IH : ∀ (k : ℕ) (kn : n ≤ k + m), Acc (lbp p) k
k : ℕ
kn : n ≤ k + (m + 1)
a : ∀ k_1 ≤ k, false ∈ p k_1
⊢ n ≤ k + 1 + m
have rw : n ≤ k + m + 1
Tactic: rw [Nat.add_right_comm]
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
p : ℕ →. Bool
H : ∃ (n : ℕ), true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
m k : ℕ
kn : n ≤ k + m
⊢ Acc (lbp p) k
have zero : ∀ (k : ℕ) (kn : n ≤ k + 0), Acc (lbp p) k
Tactic: induction m generalizing k with (refine ⟨_, fun y r => ?_⟩; rcases r with ⟨rfl, a⟩)
    | zero => injection mem_unique pn.1 (a _ kn)
    | succ m IH => exact IH _ (by rw [Nat.add_right_comm]; exact kn)
Cleared hypotheses: m, k, kn
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
p : ℕ →. Bool
H : ∃ (n : ℕ), true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
m k : ℕ
kn : n ≤ k + m
zero : ∀ (k : ℕ) (kn : n ≤ k + 0), Acc (lbp p) k
⊢ Acc (lbp p) k
have zero₁ : ∀ (k : ℕ) (kn : n ≤ k + 0) (a : ∀ k_1 ≤ k, false ∈ p k_1), Acc (lbp p) (k + 1)
Tactic: induction m generalizing k with (refine ⟨_, fun y r => ?_⟩; rcases r with ⟨rfl, a⟩)
    | zero => injection mem_unique pn.1 (a _ kn)
    | succ m IH => exact IH _ (by rw [Nat.add_right_comm]; exact kn)
Cleared hypotheses: m, k, kn
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
p : ℕ →. Bool
H : ∃ (n : ℕ), true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
m k : ℕ
kn : n ≤ k + m
zero : ∀ (k : ℕ) (kn : n ≤ k + 0), Acc (lbp p) k
zero₁ : ∀ (k : ℕ) (kn : n ≤ k + 0) (a : ∀ k_1 ≤ k, false ∈ p k_1), Acc (lbp p) (k + 1)
⊢ Acc (lbp p) k
have succ : ∀ (m : ℕ) (IH : ∀ (k : ℕ) (kn : n ≤ k + m), Acc (lbp p) k) (k : ℕ) (kn : n ≤ k + (m + 1)), Acc (lbp p) k
Tactic: induction m generalizing k with (refine ⟨_, fun y r => ?_⟩; rcases r with ⟨rfl, a⟩)
    | zero => injection mem_unique pn.1 (a _ kn)
    | succ m IH => exact IH _ (by rw [Nat.add_right_comm]; exact kn)
Cleared hypotheses: m, k, kn
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
p : ℕ →. Bool
H : ∃ (n : ℕ), true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
m k : ℕ
kn : n ≤ k + m
zero : ∀ (k : ℕ) (kn : n ≤ k + 0), Acc (lbp p) k
zero₁ : ∀ (k : ℕ) (kn : n ≤ k + 0) (a : ∀ k_1 ≤ k, false ∈ p k_1), Acc (lbp p) (k + 1)
succ : ∀ (m : ℕ) (IH : ∀ (k : ℕ) (kn : n ≤ k + m), Acc (lbp p) k) (k : ℕ) (kn : n ≤ k + (m + 1)), Acc (lbp p) k
⊢ Acc (lbp p) k
have succ₁ : ∀ (m : ℕ) (IH : ∀ (k : ℕ) (kn : n ≤ k + m), Acc (lbp p) k) (k : ℕ) (kn : n ≤ k + (m + 1))
  (a : ∀ k_1 ≤ k, false ∈ p k_1), Acc (lbp p) (k + 1)
Tactic: induction m generalizing k with (refine ⟨_, fun y r => ?_⟩; rcases r with ⟨rfl, a⟩)
    | zero => injection mem_unique pn.1 (a _ kn)
    | succ m IH => exact IH _ (by rw [Nat.add_right_comm]; exact kn)
Cleared hypotheses: m, k, kn
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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
have rcases : ∀ (n : ℕ) (h₁ : true ∈ p n) (h₂ : ∀ k < n, (p k).Dom), (p m).Dom
Tactic: rcases H with ⟨n, h₁, h₂⟩
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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
⊢ (p m).Dom
have inl : ∀ (h₃ : m < n), (p m).Dom
Tactic: rcases lt_trichotomy m n with (h₃ | h₃ | h₃)
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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
inl : ∀ (h₃ : m < n), (p m).Dom
⊢ (p m).Dom
have inr : ∀ (h₃ : m = n), (p m).Dom
Tactic: rcases lt_trichotomy m n with (h₃ | h₃ | h₃)
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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
inl : ∀ (h₃ : m < n), (p m).Dom
inr : ∀ (h₃ : m = n), (p m).Dom
⊢ (p m).Dom
have inr₁ : ∀ (h₃ : n < m), (p m).Dom
Tactic: rcases lt_trichotomy m n with (h₃ | h₃ | h₃)
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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 m).Dom
have inr : (p n).Dom
Tactic: rw [h₃]
-- Lean 4 proof step from Mathlib.Computability.Partrec (hypothesis)
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
⊢ { n : ℕ // true ∈ p n ∧ ∀ m < n, false ∈ p m }
have pm : (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₃)
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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
⊢ { n : ℕ // true ∈ p n ∧ ∀ m < n, false ∈ p m }
have false : (e : (p m).get pm = false) → { n : ℕ // true ∈ p n ∧ ∀ m < n, false ∈ p m }
Tactic: cases e : (p m).get pm
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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
false : (e : (p m).get pm = Bool.false) → { n : ℕ // true ∈ p n ∧ ∀ m < n, Bool.false ∈ p m }
⊢ { n : ℕ // true ∈ p n ∧ ∀ m < n, Bool.false ∈ p m }
have true : (e : (p m).get pm = true) → { n : ℕ // true ∈ p n ∧ ∀ m < n, Bool.false ∈ p m }
Tactic: cases e : (p m).get pm
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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 : ℕ // true ∈ p n ∧ ∀ m < n, false ∈ p m }
have false : ∀ k ≤ m, false ∈ p k
Tactic: suffices ∀ᵉ k ≤ m, false ∈ p k from IH _ ⟨rfl, this⟩ fun n h => this _ (le_of_lt_succ h)
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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 : n ≤ m
⊢ false ∈ p n
have false : ∀ (h : n < m), false ∈ p n
Tactic: rcases h.lt_or_eq_dec with h | h
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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
⊢ Bool.false ∈ p n
have false₁ : ∀ (h : n = m), Bool.false ∈ p n
Tactic: rcases h.lt_or_eq_dec with h | h
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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
have false : false ∈ p m
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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
⊢ n ∈ rfind p
have let : ∀ (m : ℕ) (hm : m ∈ rfind p), n ∈ rfind p
Tactic: let ⟨m, hm⟩ := dom_iff_mem.1 <| (@rfind_dom p).2 ⟨_, h₁, fun {m} mn => (h₂ mn).fst⟩
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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
⊢ n ∈ rfind p
have inl : ∀ (h : m < n), n ∈ rfind p
Tactic: rcases lt_trichotomy m n with (h | h | h)
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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
⊢ n ∈ rfind p
have inr : ∀ (h : m = n), n ∈ rfind p
Tactic: rcases lt_trichotomy m n with (h | h | h)
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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
⊢ n ∈ rfind p
have inr₁ : ∀ (h : n < m), n ∈ rfind p
Tactic: rcases lt_trichotomy m n with (h | h | h)
-- Lean 4 proof step from Mathlib.Computability.Partrec (hypothesis)
Goal:
α : Type u_1
f : ℕ → Option α
h : ∃ (n : ℕ) (a : α), a ∈ f n
⊢ (rfindOpt f).Dom
have h' : ∃ (n : ℕ), (f n).isSome = true
Tactic: have h' : ∃ n, (f n).isSome := h.imp fun n => Option.isSome_iff_exists.2
-- Lean 4 proof step from Mathlib.Computability.Partrec (hypothesis)
Goal:
α : Type u_1
f : ℕ → Option α
h : ∃ (n : ℕ) (a : α), a ∈ f n
h' : ∃ (n : ℕ), (f n).isSome = true
⊢ (rfindOpt f).Dom
have s : (f (Nat.find (p := fun (n : ℕ) ↦ (f n).isSome = true) h')).isSome = true
Tactic: have s := Nat.find_spec h'
-- Lean 4 proof step from Mathlib.Computability.Partrec (hypothesis)
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
⊢ (rfindOpt f).Dom
have fd : (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⟩
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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
have 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)
Tactic: refine ⟨fd, ?_⟩
-- Lean 4 proof step from Mathlib.Computability.Partrec (hypothesis)
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
⊢ 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)
have this : 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)
-- Lean 4 proof step from Mathlib.Computability.Partrec (hypothesis)
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
⊢ a ∈ rfindOpt f
have h' : (rfindOpt f).Dom
Tactic: have h' := rfindOpt_dom.2 ⟨_, _, h⟩
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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
⊢ a ∈ rfindOpt f
have obtain : ∀ (k : ℕ) (hk : (rfindOpt f).get h' ∈ f k), a ∈ rfindOpt f
Tactic: obtain ⟨k, hk⟩ := rfindOpt_spec ⟨h', rfl⟩
-- Lean 4 proof step from Mathlib.Computability.Partrec (hypothesis)
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
⊢ a ∈ rfindOpt f
have this : Option.some a = Option.some ((rfindOpt f).get h')
Tactic: have := (H (le_max_left _ _) h).symm.trans (H (le_max_right _ _) hk)
-- Lean 4 proof step from Mathlib.Computability.Partrec (hypothesis)
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
have this₁ : a = (rfindOpt f).get h'
Tactic: simp at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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) : ℕ →. ℕ)
have pair : ∀ (n : ℕ), Nat.pair (f_1 n) (g n) ∈ Nat.pair <$> (↑f_1 : ℕ →. ℕ) n <*> (↑g : ℕ →. ℕ) n
Tactic: refine (pf.pair pg).of_eq_tot fun n => ?_
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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) :
      ℕ →. ℕ)
have 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)
Tactic: refine (pf.prec pg).of_eq_tot fun n => ?_
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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 ℕ)
    (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)
have 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 :
    ℕ)
Tactic: simp only [unpaired, PFun.coe_val, bind_eq_bind]
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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 :
      ℕ)
⊢ 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) :
      ℕ)
have 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))
Tactic: simp only [mem_bind_iff, mem_some_iff]
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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))))
        (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 :
      ℕ)
have prec : ∀ (x : ℕ),
  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)))) x :
      Part ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f_1 (unpair n).1) (fun (y IH : ℕ) ↦ g (Nat.pair (unpair n).1 (Nat.pair y IH)))
        x :
      ℕ)
Tactic: induction n.unpair.2 with
    | zero => simp
    | succ m IH =>
      simp only [mem_bind_iff, mem_some_iff]
      exact ⟨_, IH, rfl⟩
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
f : ℕ → ℕ
hf : Nat.Primrec f
⊢ Nat.Partrec (↑f : ℕ →. ℕ)
have zero : Nat.Partrec (↑fun (x : ℕ) ↦ 0 : ℕ →. ℕ)
Tactic: induction hf with
  | zero => exact zero
  | succ => exact succ
  | left => exact left
  | right => exact right
  | pair _ _ pf pg =>
    refine (pf.pair pg).of_eq_tot fun n => ?_
    simp [Seq.seq]
  | comp _ _ pf pg =>
    refine (pf.comp pg).of_eq_tot fun n => (by simp)
  | prec _ _ pf pg =>
    refine (pf.prec pg).of_eq_tot fun n => ?_
    simp only [unpaired, PFun.coe_val, bind_eq_bind]
    induction n.unpair.2 with
    | zero => simp
    | succ m IH =>
      simp only [mem_bind_iff, mem_some_iff]
      exact ⟨_, IH, rfl⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
f : ℕ → ℕ
hf : Nat.Primrec f
zero : Nat.Partrec (↑fun (x : ℕ) ↦ 0 : ℕ →. ℕ)
⊢ Nat.Partrec (↑f : ℕ →. ℕ)
have succ : Nat.Partrec (↑Nat.succ : ℕ →. ℕ)
Tactic: induction hf with
  | zero => exact zero
  | succ => exact succ
  | left => exact left
  | right => exact right
  | pair _ _ pf pg =>
    refine (pf.pair pg).of_eq_tot fun n => ?_
    simp [Seq.seq]
  | comp _ _ pf pg =>
    refine (pf.comp pg).of_eq_tot fun n => (by simp)
  | prec _ _ pf pg =>
    refine (pf.prec pg).of_eq_tot fun n => ?_
    simp only [unpaired, PFun.coe_val, bind_eq_bind]
    induction n.unpair.2 with
    | zero => simp
    | succ m IH =>
      simp only [mem_bind_iff, mem_some_iff]
      exact ⟨_, IH, rfl⟩
Cleared hypotheses: hf