awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
x : List α
s₂ : σ
left : s₂ ∈ M.accept
s₁ : σ
left_1 : s₁ ∈ M.start
h : ∃ (x' : List (Option α)), x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ :
  ∀ (w : List (Option α)),
    w.reduceOption = x →
      M.IsPath s₁ s₂ w →
        ∃ (s₁ : σ) (s₂ : σ) (x' : List (Option α)),
          s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
h₁ :
  ∀ (w : List (Option α)),
    w.reduceOption = x →
      M.IsPath s₁ s₂ w →
        ∃ (s₂ : σ) (x' : List (Option α)), s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
⊢ ∃ (s₁ : σ) (s₂ : σ) (x' : List (Option α)), s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
have w : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → σ
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
x : List α
s₂ : σ
left : s₂ ∈ M.accept
s₁ : σ
left_1 : s₁ ∈ M.start
h : ∃ (x' : List (Option α)), x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ :
  ∀ (w : List (Option α)),
    w.reduceOption = x →
      M.IsPath s₁ s₂ w →
        ∃ (s₁ : σ) (s₂ : σ) (x' : List (Option α)),
          s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
h₁ :
  ∀ (w : List (Option α)),
    w.reduceOption = x →
      M.IsPath s₁ s₂ w →
        ∃ (s₂ : σ) (x' : List (Option α)), s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
w : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → σ
h₂ :
  ∀ (w : List (Option α)),
    w.reduceOption = x →
      M.IsPath s₁ s₂ w →
        ∃ (s₂ : σ) (x' : List (Option α)), s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
w₁ : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → σ
⊢ ∃ (s₁ : σ) (s₂ : σ) (x' : List (Option α)), s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
have h₃ : ∀ (w : List (Option α)),
  w.reduceOption = x →
    M.IsPath s₁ s₂ w → ∃ (x' : List (Option α)), s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
x : List α
s₂ : σ
left : s₂ ∈ M.accept
s₁ : σ
left_1 : s₁ ∈ M.start
h : ∃ (x' : List (Option α)), x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ :
  ∀ (w : List (Option α)),
    w.reduceOption = x →
      M.IsPath s₁ s₂ w →
        ∃ (s₁ : σ) (s₂ : σ) (x' : List (Option α)),
          s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
h₁ :
  ∀ (w : List (Option α)),
    w.reduceOption = x →
      M.IsPath s₁ s₂ w →
        ∃ (s₂ : σ) (x' : List (Option α)), s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
w : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → σ
h₂ :
  ∀ (w : List (Option α)),
    w.reduceOption = x →
      M.IsPath s₁ s₂ w →
        ∃ (s₂ : σ) (x' : List (Option α)), s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
w₁ : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → σ
h₃ :
  ∀ (w : List (Option α)),
    w.reduceOption = x →
      M.IsPath s₁ s₂ w →
        ∃ (x' : List (Option α)), s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
h₄ w₂ : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → σ
h₅ :
  ∀ (w : List (Option α)),
    w.reduceOption = x →
      M.IsPath s₁ s₂ w →
        ∃ (x' : List (Option α)), s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
h₆ w₃ : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → σ
⊢ ∃ (s₁ : σ) (s₂ : σ) (x' : List (Option α)), s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
have h₇ : ∀ (w : List (Option α)),
  w.reduceOption = x → M.IsPath s₁ s₂ w → s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ w.reduceOption = x ∧ M.IsPath s₁ s₂ w
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
x : List α
s₂ : σ
left : s₂ ∈ M.accept
s₁ : σ
left_1 : s₁ ∈ M.start
h : ∃ (x' : List (Option α)), x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ :
  ∀ (w : List (Option α)),
    w.reduceOption = x →
      M.IsPath s₁ s₂ w →
        ∃ (s₁ : σ) (s₂ : σ) (x' : List (Option α)),
          s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
h₁ :
  ∀ (w : List (Option α)),
    w.reduceOption = x →
      M.IsPath s₁ s₂ w →
        ∃ (s₂ : σ) (x' : List (Option α)), s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
w : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → σ
h₂ :
  ∀ (w : List (Option α)),
    w.reduceOption = x →
      M.IsPath s₁ s₂ w →
        ∃ (s₂ : σ) (x' : List (Option α)), s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
w₁ : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → σ
h₃ :
  ∀ (w : List (Option α)),
    w.reduceOption = x →
      M.IsPath s₁ s₂ w →
        ∃ (x' : List (Option α)), s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
h₄ w₂ : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → σ
h₅ :
  ∀ (w : List (Option α)),
    w.reduceOption = x →
      M.IsPath s₁ s₂ w →
        ∃ (x' : List (Option α)), s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
h₆ w₃ : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → σ
h₇ :
  ∀ (w : List (Option α)),
    w.reduceOption = x → M.IsPath s₁ s₂ w → s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ w.reduceOption = x ∧ M.IsPath s₁ s₂ w
⊢ ∃ (s₁ : σ) (s₂ : σ) (x' : List (Option α)), s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
have h₈ : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → List (Option α)
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
x : List α
s₂ : σ
left : s₂ ∈ M.accept
s₁ : σ
left_1 : s₁ ∈ M.start
h : ∃ (x' : List (Option α)), x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ :
  ∀ (w : List (Option α)),
    w.reduceOption = x →
      M.IsPath s₁ s₂ w →
        ∃ (s₁ : σ) (s₂ : σ) (x' : List (Option α)),
          s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
h₁ :
  ∀ (w : List (Option α)),
    w.reduceOption = x →
      M.IsPath s₁ s₂ w →
        ∃ (s₂ : σ) (x' : List (Option α)), s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
w : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → σ
h₂ :
  ∀ (w : List (Option α)),
    w.reduceOption = x →
      M.IsPath s₁ s₂ w →
        ∃ (s₂ : σ) (x' : List (Option α)), s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
w₁ : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → σ
h₃ :
  ∀ (w : List (Option α)),
    w.reduceOption = x →
      M.IsPath s₁ s₂ w →
        ∃ (x' : List (Option α)), s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
h₄ w₂ : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → σ
h₅ :
  ∀ (w : List (Option α)),
    w.reduceOption = x →
      M.IsPath s₁ s₂ w →
        ∃ (x' : List (Option α)), s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
h₆ w₃ : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → σ
h₇ :
  ∀ (w : List (Option α)),
    w.reduceOption = x → M.IsPath s₁ s₂ w → s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ w.reduceOption = x ∧ M.IsPath s₁ s₂ w
h₈ : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → List (Option α)
h₉ w₄ : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → σ
h₁₀ :
  ∀ (w : List (Option α)),
    w.reduceOption = x → M.IsPath s₁ s₂ w → s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ w.reduceOption = x ∧ M.IsPath s₁ s₂ w
h₁₁ : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → List (Option α)
h₁₂ w₅ : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → σ
⊢ ∃ (s₁ : σ) (s₂ : σ) (x' : List (Option α)), s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
have h₁₃ : ∀ (w : List (Option α)), w.reduceOption = x → M.IsPath s₁ s₂ w → s₁ ∈ M.start
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
x : List α
s₂ : σ
left : s₂ ∈ M.accept
s₁ : σ
left_1 : s₁ ∈ M.start
h : ∃ (x' : List (Option α)), x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ :
  ∀ (w : List (Option α)),
    w.reduceOption = x →
      M.IsPath s₁ s₂ w →
        ∃ (s₁ : σ) (s₂ : σ) (x' : List (Option α)),
          s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
h₁ :
  ∀ (w : List (Option α)),
    w.reduceOption = x →
      M.IsPath s₁ s₂ w →
        ∃ (s₂ : σ) (x' : List (Option α)), s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
w : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → σ
h₂ :
  ∀ (w : List (Option α)),
    w.reduceOption = x →
      M.IsPath s₁ s₂ w →
        ∃ (s₂ : σ) (x' : List (Option α)), s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
w₁ : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → σ
h₃ :
  ∀ (w : List (Option α)),
    w.reduceOption = x →
      M.IsPath s₁ s₂ w →
        ∃ (x' : List (Option α)), s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
h₄ w₂ : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → σ
h₅ :
  ∀ (w : List (Option α)),
    w.reduceOption = x →
      M.IsPath s₁ s₂ w →
        ∃ (x' : List (Option α)), s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
h₆ w₃ : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → σ
h₇ :
  ∀ (w : List (Option α)),
    w.reduceOption = x → M.IsPath s₁ s₂ w → s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ w.reduceOption = x ∧ M.IsPath s₁ s₂ w
h₈ : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → List (Option α)
h₉ w₄ : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → σ
h₁₀ :
  ∀ (w : List (Option α)),
    w.reduceOption = x → M.IsPath s₁ s₂ w → s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ w.reduceOption = x ∧ M.IsPath s₁ s₂ w
h₁₁ : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → List (Option α)
h₁₂ w₅ : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → σ
h₁₃ : ∀ (w : List (Option α)), w.reduceOption = x → M.IsPath s₁ s₂ w → s₁ ∈ M.start
⊢ ∃ (s₁ : σ) (s₂ : σ) (x' : List (Option α)), s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
have h₁₄ : ∀ (w : List (Option α)), w.reduceOption = x → M.IsPath s₁ s₂ w → s₂ ∈ M.accept ∧ w.reduceOption = x ∧ M.IsPath s₁ s₂ w
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (hypothesis)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
x : List α
s₁ s₂ : σ
x' : List (Option α)
hs₁ : s₁ ∈ M.start
hs₂ : s₂ ∈ M.accept
h : x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
⊢ x ∈ M.accepts
have this : s₂ ∈ M.evalFrom M.start x
Tactic: have := M.mem_evalFrom_iff_exists.mpr ⟨_, hs₁, M.mem_evalFrom_iff_exists_path.mpr ⟨_, h⟩⟩
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
⊢ M.toεNFA.εClosure S = S
have h : ∀ (a : σ), a ∈ M.toεNFA.εClosure S ↔ a ∈ S
Tactic: ext a
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
a : σ
⊢ a ∈ M.toεNFA.εClosure S ↔ a ∈ S
have h : a ∈ M.toεNFA.εClosure S → a ∈ S
Tactic: refine ⟨?_, εNFA.εClosure.base _⟩
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
start : Set σ
⊢ M.toεNFA.evalFrom start = M.evalFrom start
have rw : List.foldl M.toεNFA.stepSet start = List.foldl M.stepSet start
Tactic: rw [evalFrom, εNFA.evalFrom, toεNFA_εClosure]
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
start : Set σ
this : M.toεNFA.stepSet = M.stepSet
⊢ List.foldl M.toεNFA.stepSet start = List.foldl M.stepSet start
have rw : List.foldl M.stepSet start = List.foldl M.stepSet start
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
start : Set σ
⊢ List.foldl M.toεNFA.stepSet start = List.foldl M.stepSet start
have suffices : M.toεNFA.stepSet = M.stepSet
Tactic: suffices εNFA.stepSet (toεNFA M) = stepSet M by rw [this]
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
start : Set σ
⊢ M.toεNFA.stepSet = M.stepSet
have h : ∀ (S : Set σ) (s : α) (x : σ), x ∈ M.toεNFA.stepSet S s ↔ x ∈ M.stepSet S s
Tactic: ext S s
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
start S : Set σ
s : α
x : σ
⊢ x ∈ M.toεNFA.stepSet S s ↔ x ∈ M.stepSet S s
have h : (∃ i ∈ S, x ∈ M.toεNFA.εClosure (M.toεNFA.step i (some s))) ↔ ∃ i ∈ S, x ∈ M.step i s
Tactic: simp only [stepSet, εNFA.stepSet, exists_prop, Set.mem_iUnion]
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
start S : Set σ
s : α
x : σ
⊢ (∃ i ∈ S, x ∈ M.toεNFA.εClosure (M.toεNFA.step i (some s))) ↔ ∃ i ∈ S, x ∈ M.step i s
have h : ∀ (a : σ), a ∈ S ∧ x ∈ M.toεNFA.εClosure (M.toεNFA.step a (some s)) ↔ a ∈ S ∧ x ∈ M.step a s
Tactic: apply exists_congr
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
start S : Set σ
s : α
x : σ
⊢ ∀ (a : σ), a ∈ S ∧ x ∈ M.toεNFA.εClosure (M.toεNFA.step a (some s)) ↔ a ∈ S ∧ x ∈ M.step a s
have h : ∀ a ∈ S, x ∈ M.toεNFA.εClosure (M.toεNFA.step a (some s)) ↔ x ∈ M.step a s
Tactic: simp only [and_congr_right_iff]
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
start S : Set σ
s : α
x a : σ
h : a ∈ S
⊢ x ∈ M.toεNFA.εClosure (M.toεNFA.step a (some s)) ↔ x ∈ M.step a s
have h : x ∈ M.toεNFA.step a (some s) ↔ x ∈ M.step a s
Tactic: rw [M.toεNFA_εClosure]
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
⊢ M.toεNFA.accepts = M.accepts
have rw : {x : List α | ∃ S ∈ M.toεNFA.accept, S ∈ M.evalFrom M.toεNFA.start x} = M.accepts
Tactic: rw [εNFA.accepts, εNFA.eval, toεNFA_evalFrom_match]
-- Lean 4 proof step from Mathlib.Computability.Halting (goal)
Goal:
C : Set (ℕ →. ℕ)
h : ComputablePred fun (c : Code) ↦ c.eval ∈ C
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
⊢ g ∈ C
have obtain : ∀ (w : DecidablePred fun (c : Code) ↦ c.eval ∈ C)
  (h : Computable (σ := Bool) fun (a : Code) ↦ decide ((fun (c : Code) ↦ c.eval ∈ C) a)), g ∈ C
Tactic: obtain ⟨_, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.Halting (goal)
Goal:
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w : DecidablePred fun (c : Code) ↦ c.eval ∈ C
h : Computable (σ := Bool) fun (a : Code) ↦ decide ((fun (c : Code) ↦ c.eval ∈ C) a)
⊢ g ∈ C
have obtain : ∀ (c : Code)
  (e :
    c.eval = fun (b : ℕ) ↦
      bif decide ((fun (c : Code) ↦ c.eval ∈ C) (c, b).1) then (fun (a : Code) (b : ℕ) ↦ g (a, b).2) (c, b).1 (c, b).2
      else (fun (a : Code) (b : ℕ) ↦ f (a, b).2) (c, b).1 (c, b).2),
  g ∈ C
Tactic: obtain ⟨c, e⟩ :=
    fixed_point₂
      (Partrec.cond (h.comp fst) ((Partrec.nat_iff.2 hg).comp snd).to₂
          ((Partrec.nat_iff.2 hf).comp snd).to₂).to₂
-- Lean 4 proof step from Mathlib.Computability.Halting (hypothesis)
Goal:
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w : DecidablePred fun (c : Code) ↦ c.eval ∈ C
h : Computable (σ := Bool) fun (a : Code) ↦ decide ((fun (c : Code) ↦ c.eval ∈ C) a)
c : Code
e :
  c.eval = fun (b : ℕ) ↦
    bif decide ((fun (c : Code) ↦ c.eval ∈ C) (c, b).1) then (fun (a : Code) (b : ℕ) ↦ g (a, b).2) (c, b).1 (c, b).2
    else (fun (a : Code) (b : ℕ) ↦ f (a, b).2) (c, b).1 (c, b).2
⊢ g ∈ C
have e₁ : c.eval = fun (b : ℕ) ↦ if c.eval ∈ C then g b else f b
Tactic: simp only [Bool.cond_decide] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Computability.Halting (goal)
Goal:
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w : DecidablePred fun (c : Code) ↦ c.eval ∈ C
h : Computable (σ := Bool) fun (a : Code) ↦ decide ((fun (c : Code) ↦ c.eval ∈ C) a)
c : Code
e : c.eval = fun (b : ℕ) ↦ if c.eval ∈ C then g b else f b
⊢ g ∈ C
have pos : ∀ (H : c.eval ∈ C), g ∈ C
Tactic: by_cases H : eval c ∈ C
-- Lean 4 proof step from Mathlib.Computability.Halting (goal)
Goal:
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w : DecidablePred fun (c : Code) ↦ c.eval ∈ C
h : Computable (σ := Bool) fun (a : Code) ↦ decide ((fun (c : Code) ↦ c.eval ∈ C) a)
c : Code
e : c.eval = fun (b : ℕ) ↦ if c.eval ∈ C then g b else f b
pos : ∀ (H : c.eval ∈ C), g ∈ C
⊢ g ∈ C
have neg : ∀ (H : c.eval ∉ C), g ∈ C
Tactic: by_cases H : eval c ∈ C
-- Lean 4 proof step from Mathlib.Computability.Halting (goal)
Goal:
C : Set Code
H : ∀ (cf cg : Code), cf.eval = cg.eval → (cf ∈ C ↔ cg ∈ C)
hC : ∀ (f : Code), f ∈ C ↔ f.eval ∈ eval '' C
h : C = ∅ ∨ C = Set.univ
⊢ ComputablePred fun (c : Code) ↦ c ∈ C
have inl : ∀
  (H :
    ∀ (cf cg : Code), cf.eval = cg.eval → (Membership.mem (γ := Set Code) ∅ cf ↔ Membership.mem (γ := Set Code) ∅ cg))
  (hC : ∀ (f : Code), Membership.mem (γ := Set Code) ∅ f ↔ f.eval ∈ eval '' ∅),
  ComputablePred fun (c : Code) ↦ Membership.mem (γ := Set Code) ∅ c
Tactic: obtain rfl | rfl := h
Cleared hypotheses: C, H, hC, h
-- Lean 4 proof step from Mathlib.Computability.Halting (goal)
Goal:
C : Set Code
H : ∀ (cf cg : Code), cf.eval = cg.eval → (cf ∈ C ↔ cg ∈ C)
hC : ∀ (f : Code), f ∈ C ↔ f.eval ∈ eval '' C
h : C = ∅ ∨ C = Set.univ
inl :
  ∀
    (H :
      ∀ (cf cg : Code), cf.eval = cg.eval → (Membership.mem (γ := Set Code) ∅ cf ↔ Membership.mem (γ := Set Code) ∅ cg))
    (hC : ∀ (f : Code), Membership.mem (γ := Set Code) ∅ f ↔ f.eval ∈ eval '' ∅),
    ComputablePred fun (c : Code) ↦ Membership.mem (γ := Set Code) ∅ c
⊢ ComputablePred fun (c : Code) ↦ c ∈ C
have inr : ∀
  (H :
    ∀ (cf cg : Code),
      cf.eval = cg.eval → (Membership.mem (γ := Set Code) Set.univ cf ↔ Membership.mem (γ := Set Code) Set.univ cg))
  (hC : ∀ (f : Code), Membership.mem (γ := Set Code) Set.univ f ↔ f.eval ∈ eval '' Set.univ),
  ComputablePred fun (c : Code) ↦ Membership.mem (γ := Set Code) Set.univ c
Tactic: obtain rfl | rfl := h
Cleared hypotheses: C, H, hC, h
-- Lean 4 proof step from Mathlib.Computability.Halting (goal)
Goal:
C : Set Code
H : ∀ (cf cg : Code), cf.eval = cg.eval → (cf ∈ C ↔ cg ∈ C)
hC : ∀ (f : Code), f ∈ C ↔ f.eval ∈ eval '' C
h : C = ∅ ∨ C = Set.univ
⊢ ComputablePred fun (c : Code) ↦ c ∈ C
have inl : ∀
  (H :
    ∀ (cf cg : Code), cf.eval = cg.eval → (Membership.mem (γ := Set Code) ∅ cf ↔ Membership.mem (γ := Set Code) ∅ cg))
  (hC : ∀ (f : Code), Membership.mem (γ := Set Code) ∅ f ↔ f.eval ∈ eval '' ∅),
  ComputablePred fun (c : Code) ↦ Membership.mem (γ := Set Code) ∅ c
Tactic: {
          obtain rfl | rfl := h <;> simpa [ComputablePred, Set.mem_empty_iff_false] using
            Computable.const _}
Cleared hypotheses: C, H, hC, h
-- Lean 4 proof step from Mathlib.Computability.Halting (goal)
Goal:
C : Set Code
H : ∀ (cf cg : Code), cf.eval = cg.eval → (cf ∈ C ↔ cg ∈ C)
hC : ∀ (f : Code), f ∈ C ↔ f.eval ∈ eval '' C
h : C = ∅ ∨ C = Set.univ
inl :
  ∀
    (H :
      ∀ (cf cg : Code), cf.eval = cg.eval → (Membership.mem (γ := Set Code) ∅ cf ↔ Membership.mem (γ := Set Code) ∅ cg))
    (hC : ∀ (f : Code), Membership.mem (γ := Set Code) ∅ f ↔ f.eval ∈ eval '' ∅),
    ComputablePred fun (c : Code) ↦ Membership.mem (γ := Set Code) ∅ c
⊢ ComputablePred fun (c : Code) ↦ c ∈ C
have inr : ∀
  (H :
    ∀ (cf cg : Code),
      cf.eval = cg.eval → (Membership.mem (γ := Set Code) Set.univ cf ↔ Membership.mem (γ := Set Code) Set.univ cg))
  (hC : ∀ (f : Code), Membership.mem (γ := Set Code) Set.univ f ↔ f.eval ∈ eval '' Set.univ),
  ComputablePred fun (c : Code) ↦ Membership.mem (γ := Set Code) Set.univ c
Tactic: {
          obtain rfl | rfl := h <;> simpa [ComputablePred, Set.mem_empty_iff_false] using
            Computable.const _}
Cleared hypotheses: C, H, hC, h
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l m : Language α
a b x : List α
n : ℕ
⊢ (if n + 1 = 0 then 0 else 1) = HAdd.hAdd (α := Language α) (if n = 0 then 0 else 1) 1
have zero : (if HAdd.hAdd (α := ℕ) 0 1 = 0 then 0 else 1) = HAdd.hAdd (α := Language α) (if Eq (α := ℕ) 0 0 then 0 else 1) 1
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l m : Language α
a b x : List α
n : ℕ
zero : (if HAdd.hAdd (α := ℕ) 0 1 = 0 then 0 else 1) = HAdd.hAdd (α := Language α) (if Eq (α := ℕ) 0 0 then 0 else 1) 1
⊢ (if n + 1 = 0 then 0 else 1) = HAdd.hAdd (α := Language α) (if n = 0 then 0 else 1) 1
have succ : ∀ (n : ℕ), (if n + 1 + 1 = 0 then 0 else 1) = HAdd.hAdd (α := Language α) (if n + 1 = 0 then 0 else 1) 1
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
l : Language α
x : List α
⊢ x ∈ l∗ ↔ ∃ (S : List (List α)), x = S.flatten ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []
have mp : x ∈ l∗ → ∃ (S : List (List α)), x = S.flatten ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []
Tactic: constructor
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
l : Language α
x : List α
mp : x ∈ l∗ → ∃ (S : List (List α)), x = S.flatten ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []
⊢ x ∈ l∗ ↔ ∃ (S : List (List α)), x = S.flatten ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []
have mpr : (∃ (S : List (List α)), x = S.flatten ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []) → x ∈ l∗
Tactic: constructor
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
l : Language α
S : List (List α)
h : ∀ y ∈ S, y ∈ l
⊢ ∃ (S_1 : List (List α)), S.flatten = S_1.flatten ∧ ∀ y ∈ S_1, y ∈ l ∧ y ≠ []
have mp : ∀ (y : List α) (hy : y ∈ filter (fun (l : List α) ↦ !l.isEmpty) S), y ∈ l ∧ y ≠ []
Tactic: refine ⟨S.filter fun l ↦ !List.isEmpty l,
      by simp [List.flatten_filter_not_isEmpty], fun y hy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Computability.Language (hypothesis)
Goal:
α : Type u_1
l : Language α
S : List (List α)
h : ∀ y ∈ S, y ∈ l
y : List α
hy : y ∈ filter (fun (l : List α) ↦ !l.isEmpty) S
⊢ y ∈ l ∧ y ≠ []
have hy₁ : y ∈ S ∧ ¬y = []
Tactic: simp only [mem_filter, Bool.not_eq_eq_eq_not, Bool.not_true, isEmpty_eq_false_iff, ne_eq] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
l : Language α
⊢ l∗ = {x : List α | ∃ (S : List (List α)), x = S.flatten ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []}
have h : ∀ (x : List α),
  x ∈ l∗ ↔
    Membership.mem (γ := Language α) {x : List α | ∃ (S : List (List α)), x = S.flatten ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []} x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
l : Language α
n : ℕ
ihn : ∀ {x : List α}, x ∈ l ^ n ↔ ∃ (S : List (List α)), x = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l
x : List α
⊢ x ∈ l ^ (n + 1) ↔ ∃ (S : List (List α)), x = S.flatten ∧ S.length = n + 1 ∧ ∀ y ∈ S, y ∈ l
have succ : (∃ a ∈ l, ∃ (b : List α), (∃ (S : List (List α)), b = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l) ∧ a ++ b = x) ↔
  ∃ (S : List (List α)), x = S.flatten ∧ S.length = n + 1 ∧ ∀ y ∈ S, y ∈ l
Tactic: simp only [pow_succ', mem_mul, ihn]