awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
n : ℕ
h_1 : M.IsPath s₁ s₂ (List.replicate n none)
h : Eq.{u + 1} (α := List α) [] []
h₁ : M.IsPath s₁ s₂ (List.replicate n none)
h₂ : Eq.{u + 1} (α := List α) [] []
h₃ : M.IsPath s₁ s₂ (List.replicate n none)
h₄ : Eq.{u + 1} (α := List α) [] []
h₅ : M.IsPath s₁ s₂ (List.replicate n none)
h₆ : Eq.{u + 1} (α := List α) [] []
h₇ : M.IsPath s₁ s₂ (List.replicate n none)
⊢ Eq.{u + 1} (α := List α) [] [] ∧ M.IsPath s₁ s₂ (List.replicate n none)

Tactic:
trivial
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
nil :
  (∃ (x' : List (Option α)), (∃ (n : ℕ), x' = List.replicate n none) ∧ M.IsPath s₁ s₂ x') →
    ∃ (n : ℕ), M.IsPath s₁ s₂ (List.replicate n none)
⊢ (∃ (x' : List (Option α)), x'.reduceOption = [] ∧ M.IsPath s₁ s₂ x') →
    ∃ (n : ℕ), M.IsPath s₁ s₂ (List.replicate n none)

Tactic:
simp_rw [List.reduceOption_eq_nil_iff]

Premises used: List.reduceOption_eq_nil_iff
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
n : ℕ
h : M.IsPath s₁ s₂ (List.replicate n none)
⊢ ∃ (n : ℕ), M.IsPath s₁ s₂ (List.replicate n none)

Tactic:
⟨n, h⟩

Premises used: Exists.intro
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
n : ℕ
h : M.IsPath s₁ s₂ (List.replicate n none)
⊢ ∃ (n : ℕ), M.IsPath s₁ s₂ (List.replicate n none)

Tactic:
exact ⟨n, h⟩
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
x : List α
a : α
ih : ∀ {s₂ : σ}, s₂ ∈ M.evalFrom {s₁} x ↔ ∃ (x' : List (Option α)), x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
s₂ : σ
append_singleton :
  (∃ t ∈ M.evalFrom {s₁} x, s₂ ∈ M.εClosure (M.step t (some a))) ↔
    ∃ (x' : List (Option α)), x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x'
⊢ s₂ ∈ M.evalFrom {s₁} (x ++ [a]) ↔ ∃ (x' : List (Option α)), x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x'

Tactic:
rw [evalFrom_append_singleton, mem_stepSet_iff]

Premises used: εNFA.evalFrom_append_singleton, εNFA.mem_stepSet_iff
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
x : List α
a : α
ih : ∀ {s₂ : σ}, s₂ ∈ M.evalFrom {s₁} x ↔ ∃ (x' : List (Option α)), x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
s₂ : σ
append_singleton :
  (∃ t ∈ M.evalFrom {s₁} x, s₂ ∈ M.εClosure (M.step t (some a))) →
    ∃ (x' : List (Option α)), x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x'
append_singleton₁ :
  (∃ (x' : List (Option α)), x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x') →
    ∃ t ∈ M.evalFrom {s₁} x, s₂ ∈ M.εClosure (M.step t (some a))
⊢ (∃ t ∈ M.evalFrom {s₁} x, s₂ ∈ M.εClosure (M.step t (some a))) ↔
    ∃ (x' : List (Option α)), x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x'

Tactic:
constructor
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
x : List α
a : α
ih : ∀ {s₂ : σ}, s₂ ∈ M.evalFrom {s₁} x ↔ ∃ (x' : List (Option α)), x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
s₂ t : σ
ht : t ∈ M.evalFrom {s₁} x
h : s₂ ∈ M.εClosure (M.step t (some a))
append_singleton :
  ∀ (x' : List (Option α)),
    x'.reduceOption = x → M.IsPath s₁ t x' → ∃ (x' : List (Option α)), x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x'
⊢ ∃ (x' : List (Option α)), x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x'

Tactic:
obtain ⟨x', _, _⟩ := ih.mp ht

Premises used: Iff.mp
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
x : List α
a : α
ih : ∀ {s₂ : σ}, s₂ ∈ M.evalFrom {s₁} x ↔ ∃ (x' : List (Option α)), x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
s₂ t : σ
ht : t ∈ M.evalFrom {s₁} x
h : s₂ ∈ M.εClosure (M.step t (some a))
x' : List (Option α)
left : x'.reduceOption = x
right : M.IsPath s₁ t x'
append_singleton :
  ∀ (h : ∃ t_1 ∈ M.step t (some a), s₂ ∈ M.εClosure {t_1}) (x' : List (Option α)),
    x'.reduceOption = x → M.IsPath s₁ t x' → ∃ (x' : List (Option α)), x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x'
⊢ ∃ (x' : List (Option α)), x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x'

Tactic:
rw [mem_εClosure_iff_exists] at h

Premises used: εNFA.mem_εClosure_iff_exists
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
x : List α
a : α
ih : ∀ {s₂ : σ}, s₂ ∈ M.evalFrom {s₁} x ↔ ∃ (x' : List (Option α)), x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
s₂ t : σ
ht : t ∈ M.evalFrom {s₁} x
h : ∃ t_1 ∈ M.step t (some a), s₂ ∈ M.εClosure {t_1}
x' : List (Option α)
left : x'.reduceOption = x
right : M.IsPath s₁ t x'
⊢ ∃ t_1 ∈ M.step t (some a), ∃ (n : ℕ), M.IsPath t_1 s₂ (List.replicate n none)

Tactic:
simp_rw [mem_εClosure_iff_exists_path] at h

Premises used: εNFA.mem_εClosure_iff_exists_path
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
x : List α
a : α
ih : ∀ {s₂ : σ}, s₂ ∈ M.evalFrom {s₁} x ↔ ∃ (x' : List (Option α)), x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
s₂ t : σ
ht : t ∈ M.evalFrom {s₁} x
x' : List (Option α)
left : x'.reduceOption = x
right : M.IsPath s₁ t x'
h : ∃ t_1 ∈ M.step t (some a), ∃ (n : ℕ), M.IsPath t_1 s₂ (List.replicate n none)
append_singleton :
  ∀ u ∈ M.step t (some a),
    ∀ (n : ℕ),
      M.IsPath u s₂ (List.replicate n none) → ∃ (x' : List (Option α)), x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x'
⊢ ∃ (x' : List (Option α)), x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x'

Tactic:
obtain ⟨u, _, n, _⟩ := h
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
x : List α
a : α
ih : ∀ {s₂ : σ}, s₂ ∈ M.evalFrom {s₁} x ↔ ∃ (x' : List (Option α)), x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
s₂ t : σ
ht : t ∈ M.evalFrom {s₁} x
x' : List (Option α)
left : x'.reduceOption = x
right : M.IsPath s₁ t x'
u : σ
left_1 : u ∈ M.step t (some a)
n : ℕ
h_1 : M.IsPath u s₂ (List.replicate n none)
h :
  (x' ++ some a :: List.replicate n none).reduceOption = x ++ [a] ∧
    M.IsPath s₁ s₂ (x' ++ some a :: List.replicate n none)
⊢ ∃ (x' : List (Option α)), x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x'

Tactic:
use x' ++ some a :: List.replicate n none

Premises used: List.replicate, Option.some, Option.none
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
x : List α
a : α
ih : ∀ {s₂ : σ}, s₂ ∈ M.evalFrom {s₁} x ↔ ∃ (x' : List (Option α)), x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
s₂ t : σ
ht : t ∈ M.evalFrom {s₁} x
x' : List (Option α)
left : x'.reduceOption = x
right : M.IsPath s₁ t x'
u : σ
left_1 : u ∈ M.step t (some a)
n : ℕ
h_1 : M.IsPath u s₂ (List.replicate n none)
h : x'.reduceOption ++ [a] = x ++ [a] ∧ ∃ (t : σ), M.IsPath s₁ t x' ∧ M.IsPath t s₂ (some a :: List.replicate n none)
⊢ (x' ++ some a :: List.replicate n none).reduceOption = x ++ [a] ∧
    M.IsPath s₁ s₂ (x' ++ some a :: List.replicate n none)

Tactic:
rw [List.reduceOption_append, List.reduceOption_cons_of_some,
        List.reduceOption_replicate_none, isPath_append]

Premises used: List.reduceOption_replicate_none, εNFA.isPath_append, List.reduceOption_cons_of_some, List.reduceOption_append
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
x : List α
a : α
ih : ∀ {s₂ : σ}, s₂ ∈ M.evalFrom {s₁} x ↔ ∃ (x' : List (Option α)), x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
s₂ t : σ
ht : t ∈ M.evalFrom {s₁} x
x' : List (Option α)
left : x'.reduceOption = x
right : M.IsPath s₁ t x'
u : σ
left_1 : u ∈ M.step t (some a)
n : ℕ
h_1 : M.IsPath u s₂ (List.replicate n none)
h : x'.reduceOption ++ [a] = x ++ [a]
h₁ : ∃ (t : σ), M.IsPath s₁ t x' ∧ M.IsPath t s₂ (some a :: List.replicate n none)
h₂ h₃ h₄ : x'.reduceOption ++ [a] = x ++ [a]
h₅ h₆ h₇ : ∃ (t : σ), M.IsPath s₁ t x' ∧ M.IsPath t s₂ (some a :: List.replicate n none)
h₈ h₉ : x'.reduceOption ++ [a] = x ++ [a]
h₁₀ h₁₁ : ∃ (t : σ), M.IsPath s₁ t x' ∧ M.IsPath t s₂ (some a :: List.replicate n none)
h₁₂ : M.IsPath s₁ t x' ∧ M.IsPath t s₂ (some a :: List.replicate n none)
h₁₃ : σ
h₁₄ : M.IsPath s₁ t x' ∧ M.IsPath t s₂ (some a :: List.replicate n none)
h₁₅ : σ
h₁₆ : M.IsPath s₁ t x'
h₁₇ : M.IsPath t s₂ (some a :: List.replicate n none)
h₁₈ : σ
h₁₉ : M.IsPath s₁ t x'
h₂₀ : M.IsPath t s₂ (some a :: List.replicate n none)
h₂₁ : σ
h₂₂ h₂₃ : M.IsPath t s₂ (some a :: List.replicate n none)
⊢ x'.reduceOption ++ [a] = x ++ [a] ∧ ∃ (t : σ), M.IsPath s₁ t x' ∧ M.IsPath t s₂ (some a :: List.replicate n none)

Tactic:
tauto
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
x : List α
a : α
ih : ∀ {s₂ : σ}, s₂ ∈ M.evalFrom {s₁} x ↔ ∃ (x' : List (Option α)), x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
s₂ : σ
append_singleton :
  (∃ (x' : List (Option α)),
      (∃ (l₁ : List (Option α)) (l₂ : List (Option α)),
          x' = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = x ∧ ∃ (n : ℕ), l₂ = List.replicate n none) ∧
        M.IsPath s₁ s₂ x') →
    ∃ t ∈ M.evalFrom {s₁} x, s₂ ∈ M.εClosure (M.step t (some a))
⊢ (∃ (x' : List (Option α)), x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x') →
    ∃ t ∈ M.evalFrom {s₁} x, s₂ ∈ M.εClosure (M.step t (some a))

Tactic:
simp_rw [← List.concat_eq_append, List.reduceOption_eq_concat_iff,
        List.reduceOption_eq_nil_iff]

Premises used: List.reduceOption_eq_nil_iff, List.concat_eq_append, List.reduceOption_eq_concat_iff
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
x : List α
a : α
ih : ∀ {s₂ : σ}, s₂ ∈ M.evalFrom {s₁} x ↔ ∃ (x' : List (Option α)), x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
s₂ : σ
x' : List (Option α)
left : x'.reduceOption = x
n : ℕ
h : M.IsPath s₁ s₂ (x' ++ some a :: List.replicate n none)
⊢ ∃ (t : σ), M.IsPath s₁ t x' ∧ M.IsPath t s₂ (some a :: List.replicate n none)

Tactic:
rw [isPath_append] at h

Premises used: εNFA.isPath_append
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
x : List α
a : α
ih : ∀ {s₂ : σ}, s₂ ∈ M.evalFrom {s₁} x ↔ ∃ (x' : List (Option α)), x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
s₂ : σ
x' : List (Option α)
left : x'.reduceOption = x
n : ℕ
h : ∃ (t : σ), M.IsPath s₁ t x' ∧ M.IsPath t s₂ (some a :: List.replicate n none)
append_singleton :
  ∀ (t : σ),
    M.IsPath s₁ t x' →
      ∀ u ∈ M.step t (some a),
        M.IsPath u s₂ (List.replicate n none) → ∃ t ∈ M.evalFrom {s₁} x, s₂ ∈ M.εClosure (M.step t (some a))
⊢ ∃ t ∈ M.evalFrom {s₁} x, s₂ ∈ M.εClosure (M.step t (some a))

Tactic:
obtain ⟨t, _, _ | u⟩ := h
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
x : List α
a : α
ih : ∀ {s₂ : σ}, s₂ ∈ M.evalFrom {s₁} x ↔ ∃ (x' : List (Option α)), x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
s₂ : σ
x' : List (Option α)
left : x'.reduceOption = x
n : ℕ
t : σ
left_1 : M.IsPath s₁ t x'
u : σ
h_1 : u ∈ M.step t (some a)
h_2 : M.IsPath u s₂ (List.replicate n none)
h : t ∈ M.evalFrom {s₁} x ∧ s₂ ∈ M.εClosure (M.step t (some a))
⊢ ∃ t ∈ M.evalFrom {s₁} x, s₂ ∈ M.εClosure (M.step t (some a))

Tactic:
use t
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
x : List α
a : α
ih : ∀ {s₂ : σ}, s₂ ∈ M.evalFrom {s₁} x ↔ ∃ (x' : List (Option α)), x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
s₂ : σ
x' : List (Option α)
left : x'.reduceOption = x
n : ℕ
t : σ
left_1 : M.IsPath s₁ t x'
u : σ
h_1 : u ∈ M.step t (some a)
h_2 : M.IsPath u s₂ (List.replicate n none)
h :
  (∃ (x' : List (Option α)), x'.reduceOption = x ∧ M.IsPath s₁ t x') ∧ ∃ t_1 ∈ M.step t (some a), s₂ ∈ M.εClosure {t_1}
⊢ t ∈ M.evalFrom {s₁} x ∧ s₂ ∈ M.εClosure (M.step t (some a))

Tactic:
rw [mem_εClosure_iff_exists, ih]

Premises used: εNFA.mem_εClosure_iff_exists
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
x : List α
a : α
ih : ∀ {s₂ : σ}, s₂ ∈ M.evalFrom {s₁} x ↔ ∃ (x' : List (Option α)), x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
s₂ : σ
x' : List (Option α)
left : x'.reduceOption = x
n : ℕ
t : σ
left_1 : M.IsPath s₁ t x'
u : σ
h_1 : u ∈ M.step t (some a)
h_2 : M.IsPath u s₂ (List.replicate n none)
h :
  (∃ (x' : List (Option α)), x'.reduceOption = x ∧ M.IsPath s₁ t x') ∧
    ∃ t_1 ∈ M.step t (some a), ∃ (n : ℕ), M.IsPath t_1 s₂ (List.replicate n none)
⊢ (∃ (x' : List (Option α)), x'.reduceOption = x ∧ M.IsPath s₁ t x') ∧ ∃ t_1 ∈ M.step t (some a), s₂ ∈ M.εClosure {t_1}

Tactic:
simp_rw [mem_εClosure_iff_exists_path]

Premises used: εNFA.mem_εClosure_iff_exists_path
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
x : List α
a : α
ih : ∀ {s₂ : σ}, s₂ ∈ M.evalFrom {s₁} x ↔ ∃ (x' : List (Option α)), x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
s₂ : σ
x' : List (Option α)
left : x'.reduceOption = x
n : ℕ
t : σ
left_1 : M.IsPath s₁ t x'
u : σ
h_1 : u ∈ M.step t (some a)
h_2 : M.IsPath u s₂ (List.replicate n none)
h : ∃ (x' : List (Option α)), x'.reduceOption = x ∧ M.IsPath s₁ t x'
h₁ : ∃ t_1 ∈ M.step t (some a), ∃ (n : ℕ), M.IsPath t_1 s₂ (List.replicate n none)
h₂ h₃ h₄ : ∃ (x' : List (Option α)), x'.reduceOption = x ∧ M.IsPath s₁ t x'
h₅ h₆ h₇ : ∃ t_1 ∈ M.step t (some a), ∃ (n : ℕ), M.IsPath t_1 s₂ (List.replicate n none)
h₈ h₉ : ∃ (x' : List (Option α)), x'.reduceOption = x ∧ M.IsPath s₁ t x'
h₁₀ h₁₁ : ∃ t_1 ∈ M.step t (some a), ∃ (n : ℕ), M.IsPath t_1 s₂ (List.replicate n none)
h₁₂ : u ∈ M.step t (some a) ∧ ∃ (n : ℕ), M.IsPath u s₂ (List.replicate n none)
h₁₃ : σ
h₁₄ : u ∈ M.step t (some a) ∧ ∃ (n : ℕ), M.IsPath u s₂ (List.replicate n none)
h₁₅ : σ
⊢ (∃ (x' : List (Option α)), x'.reduceOption = x ∧ M.IsPath s₁ t x') ∧
    ∃ t_1 ∈ M.step t (some a), ∃ (n : ℕ), M.IsPath t_1 s₂ (List.replicate n none)

Tactic:
tauto
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
x : List α
nil : ∀ {s₂ : σ}, s₂ ∈ M.evalFrom {s₁} [] ↔ ∃ (x' : List (Option α)), x'.reduceOption = [] ∧ M.IsPath s₁ s₂ x'
append_singleton :
  ∀ (x : List α) (a : α)
    (ih : ∀ {s₂ : σ}, s₂ ∈ M.evalFrom {s₁} x ↔ ∃ (x' : List (Option α)), x'.reduceOption = x ∧ M.IsPath s₁ s₂ x')
    {s₂ : σ}, s₂ ∈ M.evalFrom {s₁} (x ++ [a]) ↔ ∃ (x' : List (Option α)), x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x'
⊢ s₂ ∈ M.evalFrom {s₁} x ↔ ∃ (x' : List (Option α)), x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'

Tactic:
induction x using List.reverseRecOn generalizing s₂ with
  | nil =>
    rw [evalFrom_nil, mem_εClosure_iff_exists_path]
    constructor
    · intro ⟨n, _⟩
      use List.replicate n none
      rw [List.reduceOption_replicate_none]
      trivial
    · simp_rw [List.reduceOption_eq_nil_iff]
      intro ⟨_, ⟨n, rfl⟩, h⟩
      exact ⟨n, h⟩
  | append_singleton x a ih =>
    rw [evalFrom_append_singleton, mem_stepSet_iff]
    constructor
    · intro ⟨t, ht, h⟩
      obtain ⟨x', _, _⟩ := ih.mp ht
      rw [mem_εClosure_iff_exists] at h
      simp_rw [mem_εClosure_iff_exists_path] at h
      obtain ⟨u, _, n, _⟩ := h
      use x' ++ some a :: List.replicate n none
      rw [List.reduceOption_append, List.reduceOption_cons_of_some,
        List.reduceOption_replicate_none, isPath_append]
      tauto
    · simp_rw [← List.concat_eq_append, List.reduceOption_eq_concat_iff,
        List.reduceOption_eq_nil_iff]
      intro ⟨_, ⟨x', _, rfl, _, n, rfl⟩, h⟩
      rw [isPath_append] at h
      obtain ⟨t, _, _ | u⟩ := h
      use t
      rw [mem_εClosure_iff_exists, ih]
      simp_rw [mem_εClosure_iff_exists_path]
      tauto

Premises used: List.reduceOption_eq_nil_iff, List.reduceOption_replicate_none, εNFA.mem_εClosure_iff_exists_path, εNFA.evalFrom_append_singleton, List.concat_eq_append, εNFA.isPath_append, εNFA.mem_εClosure_iff_exists, List.reduceOption_cons_of_some, List.reduceOption_append, εNFA.evalFrom_nil, List.reduceOption_eq_concat_iff, εNFA.mem_stepSet_iff
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
x : List α
s₂ : σ
left : s₂ ∈ M.accept
h : s₂ ∈ M.eval x
⊢ ∃ t ∈ M.start, s₂ ∈ M.evalFrom {t} x

Tactic:
rw [eval, mem_evalFrom_iff_exists] at h

Premises used: εNFA.mem_evalFrom_iff_exists, εNFA.eval
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
x : List α
s₂ : σ
left : s₂ ∈ M.accept
h : ∃ t ∈ M.start, s₂ ∈ M.evalFrom {t} x
obtain :
  ∀ s₁ ∈ M.start,
    ∀ (h : s₂ ∈ M.evalFrom {s₁} x),
      ∃ (s₁ : σ) (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'

Tactic:
obtain ⟨s₁, _, h⟩ := h
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
x : List α
s₂ : σ
left : s₂ ∈ M.accept
s₁ : σ
left_1 : s₁ ∈ M.start
h : s₂ ∈ M.evalFrom {s₁} x
⊢ ∃ (x' : List (Option α)), x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'

Tactic:
rw [mem_evalFrom_iff_exists_path] at h

Premises used: εNFA.mem_evalFrom_iff_exists_path
-- Module: Mathlib.Computability.EpsilonNFA
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'
⊢ s₂ ∈ M.evalFrom M.start x

Tactic:
have := M.mem_evalFrom_iff_exists.mpr ⟨_, hs₁, M.mem_evalFrom_iff_exists_path.mpr ⟨_, h⟩⟩
-- Module: Mathlib.Computability.EpsilonNFA
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'
this : s₂ ∈ M.evalFrom M.start x
⊢ x ∈ M.accepts

Tactic:
⟨s₂, hs₂, this⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, εNFA.accepts
-- Module: Mathlib.Computability.EpsilonNFA
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'
this : s₂ ∈ M.evalFrom M.start x
⊢ x ∈ M.accepts

Tactic:
exact ⟨s₂, hs₂, this⟩
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
start : Set σ
⊢ M.toNFA.evalFrom (M.εClosure start) = M.evalFrom start

Tactic:
rfl

Premises used: εNFA.stepSet, εNFA.evalFrom, rfl
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
⊢ M.toNFA.accepts = M.accepts

Tactic:
rfl

Premises used: Set.Mem, εNFA.stepSet, setOf, εNFA.eval, εNFA.evalFrom, εNFA.accepts, rfl
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
inst : Fintype σ
x : List α
hx : x ∈ M.accepts
hlen : Fintype.card.{v} (Set σ) ≤ x.length
⊢ ∃ (a : List α) (b : List α) (c : List α),
    x = a ++ b ++ c ∧
      a.length + b.length ≤ Fintype.card.{v} (Set σ) ∧ b ≠ [] ∧ HMul.hMul (α := Language α) {a} {b}∗ * {c} ≤ M.accepts

Tactic:
M.toNFA.pumping_lemma hx hlen

Premises used: NFA.pumping_lemma, Set.Mem, εNFA.stepSet, setOf, εNFA.eval, εNFA.evalFrom, εNFA.accepts
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
h : ∀ (a : σ), a ∈ M.toεNFA.εClosure S ↔ a ∈ S
⊢ M.toεNFA.εClosure S = S

Tactic:
ext a
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
a : σ
⊢ a ∈ M.toεNFA.εClosure S ↔ a ∈ S

Tactic:
⟨?_, εNFA.εClosure.base _⟩

Premises used: εNFA.εClosure.base, Iff.intro
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
a : σ
h : a ∈ M.toεNFA.εClosure S → a ∈ S
⊢ a ∈ M.toεNFA.εClosure S ↔ a ∈ S

Tactic:
refine ⟨?_, εNFA.εClosure.base _⟩
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
a : σ
h : a ∈ S
⊢ a ∈ S

Tactic:
h
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
a : σ
h : a ∈ S
⊢ a ∈ S

Tactic:
exact h
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
a s : σ
h_1 : M.toεNFA.εClosure S s
h : a ∈ M.toεNFA.step s none
⊢ a ∈ S

Tactic:
cases h
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
start : Set σ
rw : List.foldl M.toεNFA.stepSet start = List.foldl M.stepSet start
⊢ M.toεNFA.evalFrom start = M.evalFrom start

Tactic:
rw [evalFrom, εNFA.evalFrom, toεNFA_εClosure]

Premises used: NFA.evalFrom, εNFA.evalFrom, NFA.toεNFA_εClosure
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
start : Set σ
this : M.toεNFA.stepSet = M.stepSet
rw rw₁ : List.foldl M.stepSet start = List.foldl M.stepSet start
⊢ List.foldl M.toεNFA.stepSet start = List.foldl M.stepSet start

Tactic:
rw [this]
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
start : Set σ
suffices : M.toεNFA.stepSet = M.stepSet
⊢ List.foldl M.toεNFA.stepSet start = List.foldl M.stepSet start

Tactic:
suffices εNFA.stepSet (toεNFA M) = stepSet M by rw [this]
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
start : Set σ
h : ∀ (S : Set σ) (s : α) (x : σ), x ∈ M.toεNFA.stepSet S s ↔ x ∈ M.stepSet S s
⊢ M.toεNFA.stepSet = M.stepSet

Tactic:
ext S s
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
start S : Set σ
s : α
x : σ
h : (∃ i ∈ S, x ∈ M.toεNFA.εClosure (M.toεNFA.step i (some s))) ↔ ∃ i ∈ S, x ∈ M.step i s
⊢ x ∈ M.toεNFA.stepSet S s ↔ x ∈ M.stepSet S s

Tactic:
simp only [stepSet, εNFA.stepSet, exists_prop, Set.mem_iUnion]

Premises used: εNFA.stepSet, Set.mem_iUnion, exists_prop, NFA.stepSet
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
start S : Set σ
s : α
x : σ
h : ∀ (a : σ), a ∈ S ∧ x ∈ M.toεNFA.εClosure (M.toεNFA.step a (some s)) ↔ a ∈ S ∧ x ∈ M.step a s
⊢ (∃ i ∈ S, x ∈ M.toεNFA.εClosure (M.toεNFA.step i (some s))) ↔ ∃ i ∈ S, x ∈ M.step i s

Tactic:
apply exists_congr

Premises used: exists_congr
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
start S : Set σ
s : α
x : σ
h : ∀ a ∈ S, x ∈ M.toεNFA.εClosure (M.toεNFA.step a (some s)) ↔ x ∈ M.step a s
⊢ ∀ (a : σ), a ∈ S ∧ x ∈ M.toεNFA.εClosure (M.toεNFA.step a (some s)) ↔ a ∈ S ∧ x ∈ M.step a s

Tactic:
simp only [and_congr_right_iff]

Premises used: and_congr_right_iff
-- Module: Mathlib.Computability.EpsilonNFA
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)
⊢ a ∈ S → (x ∈ M.toεNFA.εClosure (M.toεNFA.step a (some s)) ↔ x ∈ M.step a s)

Tactic:
_
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
start S : Set σ
s : α
x a : σ
h_1 : a ∈ S
h : x ∈ M.toεNFA.step a (some s) ↔ x ∈ M.step a s
⊢ x ∈ M.toεNFA.εClosure (M.toεNFA.step a (some s)) ↔ x ∈ M.step a s

Tactic:
rw [M.toεNFA_εClosure]

Premises used: NFA.toεNFA_εClosure
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
start S : Set σ
s : α
x a : σ
h : a ∈ S
⊢ x ∈ M.toεNFA.step a (some s) ↔ x ∈ M.step a s

Tactic:
rfl
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
rw : {x : List α | ∃ S ∈ M.toεNFA.accept, S ∈ M.evalFrom M.toεNFA.start x} = M.accepts
⊢ M.toεNFA.accepts = M.accepts

Tactic:
rw [εNFA.accepts, εNFA.eval, toεNFA_evalFrom_match]

Premises used: εNFA.eval, εNFA.accepts, NFA.toεNFA_evalFrom_match
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
⊢ {x : List α | ∃ S ∈ M.toεNFA.accept, S ∈ M.evalFrom M.toεNFA.start x} = M.accepts

Tactic:
rfl
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
s : σ
a : Option α
⊢ step 0 s a = ∅

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
s : σ
a : Option α
⊢ step 1 s a = ∅

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
⊢ Eq.{v + 1} (α := Set σ) (start.{u, v} (α := α) 0) ∅

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
⊢ Eq.{v + 1} (α := Set σ) (start.{u, v} (α := α) 1) univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
⊢ Eq.{v + 1} (α := Set σ) (accept.{u, v} (α := α) 0) ∅

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
⊢ Eq.{v + 1} (α := Set σ) (accept.{u, v} (α := α) 1) univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl