awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
n : ℕ
h : M.IsPath s₁ s₂ (List.replicate n none)
⊢ ∃ (x' : List (Option α)), x'.reduceOption = [] ∧ M.IsPath s₁ s₂ x'
have h : Eq.{u + 1} (α := List α) (List.reduceOption (List.replicate n none)) [] ∧ M.IsPath s₁ s₂ (List.replicate n none)
Tactic: use List.replicate n none
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
n : ℕ
h : M.IsPath s₁ s₂ (List.replicate n none)
⊢ Eq.{u + 1} (α := List α) (List.reduceOption (List.replicate n none)) [] ∧ M.IsPath s₁ s₂ (List.replicate n none)
have h : Eq.{u + 1} (α := List α) [] [] ∧ M.IsPath s₁ s₂ (List.replicate n none)
Tactic: rw [List.reduceOption_replicate_none]
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
n : ℕ
h : M.IsPath s₁ s₂ (List.replicate n none)
⊢ Eq.{u + 1} (α := List α) [] [] ∧ M.IsPath s₁ s₂ (List.replicate n none)
have h : Eq.{u + 1} (α := List α) [] []
Tactic: trivial
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
⊢ (∃ (x' : List (Option α)), x'.reduceOption = [] ∧ M.IsPath s₁ s₂ x') →
    ∃ (n : ℕ), M.IsPath s₁ s₂ (List.replicate n none)
have nil : (∃ (x' : List (Option α)), (∃ (n : ℕ), x' = List.replicate n none) ∧ M.IsPath s₁ s₂ x') →
  ∃ (n : ℕ), M.IsPath s₁ s₂ (List.replicate n none)
Tactic: simp_rw [List.reduceOption_eq_nil_iff]
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
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₂ : σ
⊢ s₂ ∈ M.evalFrom {s₁} (x ++ [a]) ↔ ∃ (x' : List (Option α)), x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x'
have 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'
Tactic: rw [evalFrom_append_singleton, mem_stepSet_iff]
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
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 ∈ M.evalFrom {s₁} x, s₂ ∈ M.εClosure (M.step t (some a))) ↔
    ∃ (x' : List (Option α)), x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x'
have 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'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
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'
⊢ (∃ 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'
have 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))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
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 α)), x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x'
have 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'
Tactic: obtain ⟨x', _, _⟩ := ih.mp ht
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
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'
⊢ ∃ (x' : List (Option α)), x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x'
have 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'
Tactic: rw [mem_εClosure_iff_exists] at h
Cleared hypotheses: h, x', left, right
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (hypothesis)
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'
⊢ ∃ (x' : List (Option α)), x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x'
have h₁ : ∃ 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
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)
⊢ ∃ (x' : List (Option α)), x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x'
have 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'
Tactic: obtain ⟨u, _, n, _⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
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 : M.IsPath u s₂ (List.replicate n none)
⊢ ∃ (x' : List (Option α)), x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x'
have h : (x' ++ some a :: List.replicate n none).reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ (x' ++ some a :: List.replicate n none)
Tactic: use x' ++ some a :: List.replicate n none
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
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 : M.IsPath u s₂ (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)
have h : x'.reduceOption ++ [a] = x ++ [a] ∧ ∃ (t : σ), M.IsPath s₁ t x' ∧ M.IsPath t s₂ (some a :: List.replicate n none)
Tactic: rw [List.reduceOption_append, List.reduceOption_cons_of_some,
        List.reduceOption_replicate_none, isPath_append]
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
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 : M.IsPath u s₂ (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)
have h : x'.reduceOption ++ [a] = x ++ [a]
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
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]
⊢ x'.reduceOption ++ [a] = x ++ [a] ∧ ∃ (t : σ), M.IsPath s₁ t x' ∧ M.IsPath t s₂ (some a :: List.replicate n none)
have h₁ : ∃ (t : σ), M.IsPath s₁ t x' ∧ M.IsPath t s₂ (some a :: List.replicate n none)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
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)
⊢ x'.reduceOption ++ [a] = x ++ [a] ∧ ∃ (t : σ), M.IsPath s₁ t x' ∧ M.IsPath t s₂ (some a :: List.replicate n none)
have h₁₂ : M.IsPath s₁ t x' ∧ M.IsPath t s₂ (some a :: List.replicate n none)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
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'
⊢ x'.reduceOption ++ [a] = x ++ [a] ∧ ∃ (t : σ), M.IsPath s₁ t x' ∧ M.IsPath t s₂ (some a :: List.replicate n none)
have h₁₇ : M.IsPath t s₂ (some a :: List.replicate n none)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
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 α)), x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x') →
    ∃ t ∈ M.evalFrom {s₁} x, s₂ ∈ M.εClosure (M.step t (some a))
have 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))
Tactic: simp_rw [← List.concat_eq_append, List.reduceOption_eq_concat_iff,
        List.reduceOption_eq_nil_iff]
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (hypothesis)
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.evalFrom {s₁} x, s₂ ∈ M.εClosure (M.step t (some a))
have h₁ : ∃ (t : σ), M.IsPath s₁ t x' ∧ M.IsPath t s₂ (some a :: List.replicate n none)
Tactic: rw [isPath_append] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
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)
⊢ ∃ t ∈ M.evalFrom {s₁} x, s₂ ∈ M.εClosure (M.step t (some a))
have 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))
Tactic: obtain ⟨t, _, _ | u⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
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 : u ∈ M.step t (some a)
h_1 : M.IsPath u s₂ (List.replicate n none)
⊢ ∃ t ∈ M.evalFrom {s₁} x, s₂ ∈ M.εClosure (M.step t (some a))
have h : t ∈ M.evalFrom {s₁} x ∧ s₂ ∈ M.εClosure (M.step t (some a))
Tactic: use t
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
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 : u ∈ M.step t (some a)
h_1 : M.IsPath u s₂ (List.replicate n none)
⊢ t ∈ M.evalFrom {s₁} x ∧ s₂ ∈ M.εClosure (M.step t (some a))
have h : (∃ (x' : List (Option α)), x'.reduceOption = x ∧ M.IsPath s₁ t x') ∧ ∃ t_1 ∈ M.step t (some a), s₂ ∈ M.εClosure {t_1}
Tactic: rw [mem_εClosure_iff_exists, ih]
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
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 : u ∈ M.step t (some a)
h_1 : M.IsPath u 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}
have 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: simp_rw [mem_εClosure_iff_exists_path]
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
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 : u ∈ M.step t (some a)
h_1 : M.IsPath u s₂ (List.replicate n none)
⊢ (∃ (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)
have h : ∃ (x' : List (Option α)), x'.reduceOption = x ∧ M.IsPath s₁ t x'
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
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'
⊢ (∃ (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)
have h₁ : ∃ t_1 ∈ M.step t (some a), ∃ (n : ℕ), M.IsPath t_1 s₂ (List.replicate n none)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
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)
⊢ (∃ (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)
have h₁₂ : u ∈ M.step t (some a) ∧ ∃ (n : ℕ), M.IsPath u s₂ (List.replicate n none)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
x : List α
⊢ s₂ ∈ M.evalFrom {s₁} x ↔ ∃ (x' : List (Option α)), x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
have nil : ∀ {s₂ : σ}, s₂ ∈ M.evalFrom {s₁} [] ↔ ∃ (x' : List (Option α)), x'.reduceOption = [] ∧ 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
Cleared hypotheses: s₂, x
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
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'
⊢ s₂ ∈ M.evalFrom {s₁} x ↔ ∃ (x' : List (Option α)), x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
have 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'
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
Cleared hypotheses: s₂, x
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (hypothesis)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
x : List α
s₂ : σ
left : s₂ ∈ M.accept
h : s₂ ∈ M.eval x
⊢ ∃ (s₁ : σ) (s₂ : σ) (x' : List (Option α)), s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
have h₁ : ∃ t ∈ M.start, s₂ ∈ M.evalFrom {t} x
Tactic: rw [eval, mem_evalFrom_iff_exists] at h
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
h : ∃ t ∈ M.start, s₂ ∈ M.evalFrom {t} x
⊢ ∃ (s₁ : σ) (s₂ : σ) (x' : List (Option α)), s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
have 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'
Tactic: obtain ⟨s₁, _, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (hypothesis)
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
⊢ ∃ (s₁ : σ) (s₂ : σ) (x' : List (Option α)), s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
have h₁ : ∃ (x' : List (Option α)), x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
Tactic: rw [mem_evalFrom_iff_exists_path] at h
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'
⊢ ∃ (s₁ : σ) (s₂ : σ) (x' : List (Option α)), s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
have 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'
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'
⊢ ∃ (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₂ : σ) (x' : List (Option α)), s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
Tactic: tauto
Cleared hypotheses: h