awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
l : List α
a : α
ih : ∀ {s : σ}, s ∈ M.evalFrom S l ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} l
s : σ
append_singleton :
  (∃ (t : σ), (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l) ∧ s ∈ M.εClosure (M.step t (some a))) →
    ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))
append_singleton₁ :
  (∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))) →
    ∃ (t : σ), (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l) ∧ s ∈ M.εClosure (M.step t (some a))
append_singleton₂ append_singleton₃ append_singleton₄ :
  ∀ (w : σ),
    s ∈ M.εClosure (M.step w (some a)) →
      ∀ w_1 ∈ S, w ∈ M.evalFrom {w_1} l → ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))
append_singleton₅ append_singleton₆ append_singleton₇ :
  ∀ w ∈ S,
    ∀ w_1 ∈ M.evalFrom {w} l,
      s ∈ M.εClosure (M.step w_1 (some a)) →
        ∃ (t : σ), (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l) ∧ s ∈ M.εClosure (M.step t (some a))
append_singleton₈ append_singleton₉ append_singleton₁₀ :
  ∀ (w : σ),
    s ∈ M.εClosure (M.step w (some a)) →
      ∀ w_1 ∈ S, w ∈ M.evalFrom {w_1} l → ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))
append_singleton₁₁ append_singleton₁₂ append_singleton₁₃ :
  ∀ w ∈ S,
    ∀ w_1 ∈ M.evalFrom {w} l,
      s ∈ M.εClosure (M.step w_1 (some a)) →
        ∃ (t : σ), (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l) ∧ s ∈ M.εClosure (M.step t (some a))
append_singleton₁₄ append_singleton₁₅ :
  ∀ (w : σ),
    s ∈ M.εClosure (M.step w (some a)) →
      ∀ w_1 ∈ S, w ∈ M.evalFrom {w_1} l → ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))
append_singleton₁₆ :
  ∀ (w : σ),
    s ∈ M.εClosure (M.step w (some a)) →
      ∀ w_1 ∈ S, w ∈ M.evalFrom {w_1} l → w_1 ∈ S ∧ ∃ t ∈ M.evalFrom {w_1} l, s ∈ M.εClosure (M.step t (some a))
⊢ (∃ (t : σ), (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l) ∧ s ∈ M.εClosure (M.step t (some a))) ↔
    ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))
have append_singleton₁₇ : (w : σ) → s ∈ M.εClosure (M.step w (some a)) → (w_1 : σ) → w_1 ∈ S → w ∈ M.evalFrom {w_1} l → σ
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
l : List α
a : α
ih : ∀ {s : σ}, s ∈ M.evalFrom S l ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} l
s : σ
append_singleton :
  (∃ (t : σ), (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l) ∧ s ∈ M.εClosure (M.step t (some a))) →
    ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))
append_singleton₁ :
  (∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))) →
    ∃ (t : σ), (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l) ∧ s ∈ M.εClosure (M.step t (some a))
append_singleton₂ append_singleton₃ append_singleton₄ :
  ∀ (w : σ),
    s ∈ M.εClosure (M.step w (some a)) →
      ∀ w_1 ∈ S, w ∈ M.evalFrom {w_1} l → ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))
append_singleton₅ append_singleton₆ append_singleton₇ :
  ∀ w ∈ S,
    ∀ w_1 ∈ M.evalFrom {w} l,
      s ∈ M.εClosure (M.step w_1 (some a)) →
        ∃ (t : σ), (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l) ∧ s ∈ M.εClosure (M.step t (some a))
append_singleton₈ append_singleton₉ append_singleton₁₀ :
  ∀ (w : σ),
    s ∈ M.εClosure (M.step w (some a)) →
      ∀ w_1 ∈ S, w ∈ M.evalFrom {w_1} l → ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))
append_singleton₁₁ append_singleton₁₂ append_singleton₁₃ :
  ∀ w ∈ S,
    ∀ w_1 ∈ M.evalFrom {w} l,
      s ∈ M.εClosure (M.step w_1 (some a)) →
        ∃ (t : σ), (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l) ∧ s ∈ M.εClosure (M.step t (some a))
append_singleton₁₄ append_singleton₁₅ :
  ∀ (w : σ),
    s ∈ M.εClosure (M.step w (some a)) →
      ∀ w_1 ∈ S, w ∈ M.evalFrom {w_1} l → ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))
append_singleton₁₆ :
  ∀ (w : σ),
    s ∈ M.εClosure (M.step w (some a)) →
      ∀ w_1 ∈ S, w ∈ M.evalFrom {w_1} l → w_1 ∈ S ∧ ∃ t ∈ M.evalFrom {w_1} l, s ∈ M.εClosure (M.step t (some a))
append_singleton₁₇ : (w : σ) → s ∈ M.εClosure (M.step w (some a)) → (w_1 : σ) → w_1 ∈ S → w ∈ M.evalFrom {w_1} l → σ
append_singleton₁₈ :
  ∀ (w : σ),
    s ∈ M.εClosure (M.step w (some a)) →
      ∀ w_1 ∈ S, w ∈ M.evalFrom {w_1} l → w_1 ∈ S ∧ ∃ t ∈ M.evalFrom {w_1} l, s ∈ M.εClosure (M.step t (some a))
append_singleton₁₉ : (w : σ) → s ∈ M.εClosure (M.step w (some a)) → (w_1 : σ) → w_1 ∈ S → w ∈ M.evalFrom {w_1} l → σ
⊢ (∃ (t : σ), (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l) ∧ s ∈ M.εClosure (M.step t (some a))) ↔
    ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))
have append_singleton₂₀ : ∀ (w : σ), s ∈ M.εClosure (M.step w (some a)) → ∀ w_1 ∈ S, w ∈ M.evalFrom {w_1} l → w_1 ∈ S
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
l : List α
a : α
ih : ∀ {s : σ}, s ∈ M.evalFrom S l ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} l
s : σ
append_singleton :
  (∃ (t : σ), (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l) ∧ s ∈ M.εClosure (M.step t (some a))) →
    ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))
append_singleton₁ :
  (∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))) →
    ∃ (t : σ), (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l) ∧ s ∈ M.εClosure (M.step t (some a))
append_singleton₂ append_singleton₃ append_singleton₄ :
  ∀ (w : σ),
    s ∈ M.εClosure (M.step w (some a)) →
      ∀ w_1 ∈ S, w ∈ M.evalFrom {w_1} l → ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))
append_singleton₅ append_singleton₆ append_singleton₇ :
  ∀ w ∈ S,
    ∀ w_1 ∈ M.evalFrom {w} l,
      s ∈ M.εClosure (M.step w_1 (some a)) →
        ∃ (t : σ), (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l) ∧ s ∈ M.εClosure (M.step t (some a))
append_singleton₈ append_singleton₉ append_singleton₁₀ :
  ∀ (w : σ),
    s ∈ M.εClosure (M.step w (some a)) →
      ∀ w_1 ∈ S, w ∈ M.evalFrom {w_1} l → ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))
append_singleton₁₁ append_singleton₁₂ append_singleton₁₃ :
  ∀ w ∈ S,
    ∀ w_1 ∈ M.evalFrom {w} l,
      s ∈ M.εClosure (M.step w_1 (some a)) →
        ∃ (t : σ), (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l) ∧ s ∈ M.εClosure (M.step t (some a))
append_singleton₁₄ append_singleton₁₅ :
  ∀ (w : σ),
    s ∈ M.εClosure (M.step w (some a)) →
      ∀ w_1 ∈ S, w ∈ M.evalFrom {w_1} l → ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))
append_singleton₁₆ :
  ∀ (w : σ),
    s ∈ M.εClosure (M.step w (some a)) →
      ∀ w_1 ∈ S, w ∈ M.evalFrom {w_1} l → w_1 ∈ S ∧ ∃ t ∈ M.evalFrom {w_1} l, s ∈ M.εClosure (M.step t (some a))
append_singleton₁₇ : (w : σ) → s ∈ M.εClosure (M.step w (some a)) → (w_1 : σ) → w_1 ∈ S → w ∈ M.evalFrom {w_1} l → σ
append_singleton₁₈ :
  ∀ (w : σ),
    s ∈ M.εClosure (M.step w (some a)) →
      ∀ w_1 ∈ S, w ∈ M.evalFrom {w_1} l → w_1 ∈ S ∧ ∃ t ∈ M.evalFrom {w_1} l, s ∈ M.εClosure (M.step t (some a))
append_singleton₁₉ : (w : σ) → s ∈ M.εClosure (M.step w (some a)) → (w_1 : σ) → w_1 ∈ S → w ∈ M.evalFrom {w_1} l → σ
append_singleton₂₀ : ∀ (w : σ), s ∈ M.εClosure (M.step w (some a)) → ∀ w_1 ∈ S, w ∈ M.evalFrom {w_1} l → w_1 ∈ S
⊢ (∃ (t : σ), (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l) ∧ s ∈ M.εClosure (M.step t (some a))) ↔
    ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))
have append_singleton₂₁ : ∀ (w : σ),
  s ∈ M.εClosure (M.step w (some a)) →
    ∀ w_1 ∈ S, w ∈ M.evalFrom {w_1} l → ∃ t ∈ M.evalFrom {w_1} l, s ∈ M.εClosure (M.step t (some a))
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s : σ
S : Set σ
x : List α
⊢ s ∈ M.evalFrom S x ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} x
have nil : ∀ {s : σ}, s ∈ M.evalFrom S [] ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} []
Tactic: induction x using List.reverseRecOn generalizing s with
  | nil => apply mem_εClosure_iff_exists
  | append_singleton _ _ ih =>
    simp_rw [evalFrom_append_singleton, mem_stepSet_iff, ih]
    tauto
Cleared hypotheses: s, x
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s : σ
S : Set σ
x : List α
nil : ∀ {s : σ}, s ∈ M.evalFrom S [] ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} []
⊢ s ∈ M.evalFrom S x ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} x
have append_singleton : ∀ (l : List α) (a : α) (ih : ∀ {s : σ}, s ∈ M.evalFrom S l ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} l) {s : σ},
  s ∈ M.evalFrom S (l ++ [a]) ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} (l ++ [a])
Tactic: induction x using List.reverseRecOn generalizing s with
  | nil => apply mem_εClosure_iff_exists
  | append_singleton _ _ ih =>
    simp_rw [evalFrom_append_singleton, mem_stepSet_iff, ih]
    tauto
Cleared hypotheses: s, x
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s t : σ
⊢ M.IsPath s t [] ↔ s = t
have rw : (t = s ∧ Eq.{u + 1} (α := List (Option α)) [] [] ∨
    ∃ (t_1 : σ) (a : Option α) (x : List (Option α)), t_1 ∈ M.step s a ∧ M.IsPath t_1 t x ∧ [] = a :: x) ↔
  s = t
Tactic: rw [isPath_iff]
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
u : σ
y : List (Option α)
s : σ
⊢ M.IsPath s u ([] ++ y) → ∃ (t : σ), M.IsPath s t [] ∧ M.IsPath t u y
have nil : M.IsPath s u y → ∃ (t : σ), M.IsPath s t [] ∧ M.IsPath t u y
Tactic: rw [List.nil_append]
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (hypothesis)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
u : σ
y : List (Option α)
x : Option α
a : List (Option α)
ih : ∀ {s : σ}, M.IsPath s u (a ++ y) → ∃ (t : σ), M.IsPath s t a ∧ M.IsPath t u y
s t : σ
h_1 : t ∈ M.step s x
h : M.IsPath t u (a.append y)
⊢ ∃ (t : σ), M.IsPath s t (x :: a) ∧ M.IsPath t u y
have h₁ : ∃ (t_1 : σ), M.IsPath t t_1 a ∧ M.IsPath t_1 u y
Tactic: apply ih at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
u : σ
y : List (Option α)
x : Option α
a : List (Option α)
ih : ∀ {s : σ}, M.IsPath s u (a ++ y) → ∃ (t : σ), M.IsPath s t a ∧ M.IsPath t u y
s t : σ
h_1 : t ∈ M.step s x
h : ∃ (t_1 : σ), M.IsPath t t_1 a ∧ M.IsPath t_1 u y
⊢ ∃ (t : σ), M.IsPath s t (x :: a) ∧ M.IsPath t u y
have cons : ∀ (w : σ), M.IsPath t w a → M.IsPath w u y → ∃ (t : σ), M.IsPath s t (x :: a) ∧ M.IsPath t u y
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
u : σ
y : List (Option α)
x : Option α
a : List (Option α)
ih : ∀ {s : σ}, M.IsPath s u (a ++ y) → ∃ (t : σ), M.IsPath s t a ∧ M.IsPath t u y
s t : σ
h_1 : t ∈ M.step s x
h : ∃ (t_1 : σ), M.IsPath t t_1 a ∧ M.IsPath t_1 u y
cons cons₁ cons₂ cons₃ cons₄ cons₅ cons₆ cons₇ :
  ∀ (w : σ), M.IsPath t w a → M.IsPath w u y → ∃ (t : σ), M.IsPath s t (x :: a) ∧ M.IsPath t u y
⊢ ∃ (t : σ), M.IsPath s t (x :: a) ∧ M.IsPath t u y
have cons₈ : ∀ (w : σ), M.IsPath t w a → M.IsPath w u y → M.IsPath s w (x :: a) ∧ M.IsPath w u y
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
u : σ
y : List (Option α)
x : Option α
a : List (Option α)
ih : ∀ {s : σ}, M.IsPath s u (a ++ y) → ∃ (t : σ), M.IsPath s t a ∧ M.IsPath t u y
s t : σ
h_1 : t ∈ M.step s x
h : ∃ (t_1 : σ), M.IsPath t t_1 a ∧ M.IsPath t_1 u y
cons cons₁ cons₂ cons₃ cons₄ cons₅ cons₆ cons₇ :
  ∀ (w : σ), M.IsPath t w a → M.IsPath w u y → ∃ (t : σ), M.IsPath s t (x :: a) ∧ M.IsPath t u y
cons₈ : ∀ (w : σ), M.IsPath t w a → M.IsPath w u y → M.IsPath s w (x :: a) ∧ M.IsPath w u y
⊢ ∃ (t : σ), M.IsPath s t (x :: a) ∧ M.IsPath t u y
have cons₉ : (w : σ) → M.IsPath t w a → M.IsPath w u y → σ
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
u : σ
y : List (Option α)
x : Option α
a : List (Option α)
ih : ∀ {s : σ}, M.IsPath s u (a ++ y) → ∃ (t : σ), M.IsPath s t a ∧ M.IsPath t u y
s t : σ
h_1 : t ∈ M.step s x
h : ∃ (t_1 : σ), M.IsPath t t_1 a ∧ M.IsPath t_1 u y
cons cons₁ cons₂ cons₃ cons₄ cons₅ cons₆ cons₇ :
  ∀ (w : σ), M.IsPath t w a → M.IsPath w u y → ∃ (t : σ), M.IsPath s t (x :: a) ∧ M.IsPath t u y
cons₈ : ∀ (w : σ), M.IsPath t w a → M.IsPath w u y → M.IsPath s w (x :: a) ∧ M.IsPath w u y
cons₉ : (w : σ) → M.IsPath t w a → M.IsPath w u y → σ
cons₁₀ : ∀ (w : σ), M.IsPath t w a → M.IsPath w u y → M.IsPath s w (x :: a) ∧ M.IsPath w u y
cons₁₁ : (w : σ) → M.IsPath t w a → M.IsPath w u y → σ
⊢ ∃ (t : σ), M.IsPath s t (x :: a) ∧ M.IsPath t u y
have cons₁₂ : ∀ (w : σ), M.IsPath t w a → M.IsPath w u y → M.IsPath s w (x :: a)
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
u : σ
y : List (Option α)
x : Option α
a : List (Option α)
ih : ∀ {s : σ}, M.IsPath s u (a ++ y) → ∃ (t : σ), M.IsPath s t a ∧ M.IsPath t u y
s t : σ
h_1 : t ∈ M.step s x
h : ∃ (t_1 : σ), M.IsPath t t_1 a ∧ M.IsPath t_1 u y
cons cons₁ cons₂ cons₃ cons₄ cons₅ cons₆ cons₇ :
  ∀ (w : σ), M.IsPath t w a → M.IsPath w u y → ∃ (t : σ), M.IsPath s t (x :: a) ∧ M.IsPath t u y
cons₈ : ∀ (w : σ), M.IsPath t w a → M.IsPath w u y → M.IsPath s w (x :: a) ∧ M.IsPath w u y
cons₉ : (w : σ) → M.IsPath t w a → M.IsPath w u y → σ
cons₁₀ : ∀ (w : σ), M.IsPath t w a → M.IsPath w u y → M.IsPath s w (x :: a) ∧ M.IsPath w u y
cons₁₁ : (w : σ) → M.IsPath t w a → M.IsPath w u y → σ
cons₁₂ : ∀ (w : σ), M.IsPath t w a → M.IsPath w u y → M.IsPath s w (x :: a)
⊢ ∃ (t : σ), M.IsPath s t (x :: a) ∧ M.IsPath t u y
have cons₁₃ : ∀ (w : σ), M.IsPath t w a → M.IsPath w u y → M.IsPath w u y
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s u : σ
x y : List (Option α)
⊢ M.IsPath s u (x ++ y) → ∃ (t : σ), M.IsPath s t x ∧ M.IsPath t u y
have nil : ∀ {s : σ}, M.IsPath s u ([] ++ y) → ∃ (t : σ), M.IsPath s t [] ∧ M.IsPath t u y
Tactic: induction x generalizing s with
    | nil =>
      rw [List.nil_append]
      tauto
    | cons x a ih =>
      rintro (_ | ⟨t, _, _, _, _, _, h⟩)
      apply ih at h
      tauto
Cleared hypotheses: s, x
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s u : σ
x y : List (Option α)
nil : ∀ {s : σ}, M.IsPath s u ([] ++ y) → ∃ (t : σ), M.IsPath s t [] ∧ M.IsPath t u y
⊢ M.IsPath s u (x ++ y) → ∃ (t : σ), M.IsPath s t x ∧ M.IsPath t u y
have cons : ∀ (x : Option α) (a : List (Option α))
  (ih : ∀ {s : σ}, M.IsPath s u (a ++ y) → ∃ (t : σ), M.IsPath s t a ∧ M.IsPath t u y) {s : σ},
  M.IsPath s u (x :: a ++ y) → ∃ (t : σ), M.IsPath s t (x :: a) ∧ M.IsPath t u y
Tactic: induction x generalizing s with
    | nil =>
      rw [List.nil_append]
      tauto
    | cons x a ih =>
      rintro (_ | ⟨t, _, _, _, _, _, h⟩)
      apply ih at h
      tauto
Cleared hypotheses: s, x
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s u : σ
x y : List (Option α)
t : σ
hx : M.IsPath s t x
right : M.IsPath t u y
⊢ M.IsPath s u (x ++ y)
have nil : ∀ {s : σ} (hx : M.IsPath s t []), M.IsPath s u ([] ++ y)
Tactic: induction x generalizing s
Cleared hypotheses: s, x, hx
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s u : σ
x y : List (Option α)
t : σ
hx : M.IsPath s t x
right : M.IsPath t u y
nil : ∀ {s : σ} (hx : M.IsPath s t []), M.IsPath s u ([] ++ y)
⊢ M.IsPath s u (x ++ y)
have cons : ∀ (head : Option α) (tail : List (Option α)),
  (∀ {s : σ} (hx : M.IsPath s t tail), M.IsPath s u (tail ++ y)) →
    ∀ {s : σ} (hx : M.IsPath s t (head :: tail)), M.IsPath s u (head :: tail ++ y)
Tactic: induction x generalizing s
Cleared hypotheses: s, x, hx
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
u : σ
y : List (Option α)
t : σ
right : M.IsPath t u y
s : σ
hx : M.IsPath s t []
⊢ M.IsPath s u ([] ++ y)
have nil : M.IsPath t u ([] ++ y)
Tactic: cases hx
Cleared hypotheses: s, hx
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
u : σ
y : List (Option α)
t : σ
right : M.IsPath t u y
head : Option α
tail : List (Option α)
tail_ih : ∀ {s : σ} (hx : M.IsPath s t tail), M.IsPath s u (tail ++ y)
s : σ
hx : M.IsPath s t (head :: tail)
⊢ M.IsPath s u (head :: tail ++ y)
have cons : ∀ t_1 ∈ M.step s head, M.IsPath t_1 t tail → M.IsPath s u (head :: tail ++ y)
Tactic: cases hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ t : σ
h : Membership.mem (γ := Set σ) {s₁} t
⊢ ∃ (n : ℕ), M.IsPath s₁ t (List.replicate n none)
have h : M.IsPath s₁ t (List.replicate 0 none)
Tactic: use 0
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ t : σ
h : Membership.mem (γ := Set σ) {s₁} t
⊢ M.IsPath s₁ t (List.replicate 0 none)
have h : M.IsPath s₁ s₁ (List.replicate 0 none)
Tactic: subst t
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ s t : σ
h : t ∈ M.step s none
h_1 : M.εClosure {s₁} s
ih : ∃ (n : ℕ), M.IsPath s₁ s (List.replicate n none)
⊢ ∃ (n : ℕ), M.IsPath s₁ t (List.replicate n none)
have step : ∀ (n : ℕ), M.IsPath s₁ s (List.replicate n none) → ∃ (n : ℕ), M.IsPath s₁ t (List.replicate n none)
Tactic: obtain ⟨n, _⟩ := ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ s t : σ
h : t ∈ M.step s none
h_1 : M.εClosure {s₁} s
n : ℕ
h_2 : M.IsPath s₁ s (List.replicate n none)
⊢ ∃ (n : ℕ), M.IsPath s₁ t (List.replicate n none)
have h : M.IsPath s₁ t (List.replicate (n + 1) none)
Tactic: use n + 1
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ s t : σ
h : t ∈ M.step s none
h_1 : M.εClosure {s₁} s
n : ℕ
h_2 : M.IsPath s₁ s (List.replicate n none)
⊢ M.IsPath s₁ t (List.replicate (n + 1) none)
have h : ∃ (t_1 : σ), M.IsPath s₁ t_1 (List.replicate n none) ∧ M.IsPath t_1 t (List.replicate 1 none)
Tactic: rw [List.replicate_add, isPath_append]
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ s t : σ
h : t ∈ M.step s none
h_1 : M.εClosure {s₁} s
n : ℕ
h_2 : M.IsPath s₁ s (List.replicate n none)
⊢ ∃ (t_1 : σ), M.IsPath s₁ t_1 (List.replicate n none) ∧ M.IsPath t_1 t (List.replicate 1 none)
have h : M.IsPath s₁ s (List.replicate n none) ∧ M.IsPath s t (List.replicate 1 none)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ s t : σ
h_1 : t ∈ M.step s none
h_2 : M.εClosure {s₁} s
n : ℕ
h_3 : M.IsPath s₁ s (List.replicate n none)
h : M.IsPath s₁ s (List.replicate n none) ∧ M.IsPath s t (List.replicate 1 none)
h₁ : σ
h₂ : M.IsPath s₁ s (List.replicate n none) ∧ M.IsPath s t (List.replicate 1 none)
h₃ : σ
h₄ : M.IsPath s₁ s (List.replicate n none)
⊢ ∃ (t_1 : σ), M.IsPath s₁ t_1 (List.replicate n none) ∧ M.IsPath t_1 t (List.replicate 1 none)
have h₅ : M.IsPath s t (List.replicate 1 none)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
h : s₂ ∈ M.εClosure {s₁}
⊢ ∃ (n : ℕ), M.IsPath s₁ s₂ (List.replicate n none)
have base : ∀ (t : σ), Membership.mem (γ := Set σ) {s₁} t → ∃ (n : ℕ), M.IsPath s₁ t (List.replicate n none)
Tactic: induction h with
    | base t =>
      use 0
      subst t
      apply IsPath.nil
    | step _ _ _ _ ih =>
      obtain ⟨n, _⟩ := ih
      use n + 1
      rw [List.replicate_add, isPath_append]
      tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
h : s₂ ∈ M.εClosure {s₁}
base : ∀ (t : σ), Membership.mem (γ := Set σ) {s₁} t → ∃ (n : ℕ), M.IsPath s₁ t (List.replicate n none)
⊢ ∃ (n : ℕ), M.IsPath s₁ s₂ (List.replicate n none)
have step : ∀ (s t : σ),
  t ∈ M.step s none →
    M.εClosure {s₁} s →
      ∀ (ih : ∃ (n : ℕ), M.IsPath s₁ s (List.replicate n none)), ∃ (n : ℕ), M.IsPath s₁ t (List.replicate n none)
Tactic: induction h with
    | base t =>
      use 0
      subst t
      apply IsPath.nil
    | step _ _ _ _ ih =>
      obtain ⟨n, _⟩ := ih
      use n + 1
      rw [List.replicate_add, isPath_append]
      tauto
Cleared hypotheses: h
-- 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)
⊢ s₂ ∈ M.εClosure {s₁}
have zero : ∀ {s₂ : σ} (h : M.IsPath s₁ s₂ (List.replicate 0 none)), s₂ ∈ M.εClosure {s₁}
Tactic: induction n generalizing s₂
Cleared hypotheses: s₂, n, h
-- 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)
zero : ∀ {s₂ : σ} (h : M.IsPath s₁ s₂ (List.replicate 0 none)), s₂ ∈ M.εClosure {s₁}
⊢ s₂ ∈ M.εClosure {s₁}
have succ : ∀ (n : ℕ),
  (∀ {s₂ : σ} (h : M.IsPath s₁ s₂ (List.replicate n none)), s₂ ∈ M.εClosure {s₁}) →
    ∀ {s₂ : σ} (h : M.IsPath s₁ s₂ (List.replicate (n + 1) none)), s₂ ∈ M.εClosure {s₁}
Tactic: induction n generalizing s₂
Cleared hypotheses: s₂, n, h
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (hypothesis)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
h : M.IsPath s₁ s₂ (List.replicate 0 none)
⊢ s₂ ∈ M.εClosure {s₁}
have h₁ : M.IsPath s₁ s₂ []
Tactic: rw [List.replicate_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (hypothesis)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
h : M.IsPath s₁ s₂ []
⊢ s₂ ∈ M.εClosure {s₁}
have h₁ : s₁ = s₂
Tactic: apply IsPath.eq_of_nil at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (hypothesis)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
n : ℕ
h_1 : ∀ {s₂ : σ} (h : M.IsPath s₁ s₂ (List.replicate n none)), s₂ ∈ M.εClosure {s₁}
s₂ : σ
h : M.IsPath s₁ s₂ (List.replicate (n + 1) none)
⊢ s₂ ∈ M.εClosure {s₁}
have h₁ : ∃ (t : σ), M.IsPath s₁ t (List.replicate n none) ∧ s₂ ∈ M.step t none
Tactic: simp_rw [List.replicate_add, isPath_append, List.replicate_one, isPath_singleton] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
n : ℕ
h_1 : ∀ {s₂ : σ} (h : M.IsPath s₁ s₂ (List.replicate n none)), s₂ ∈ M.εClosure {s₁}
s₂ : σ
h : ∃ (t : σ), M.IsPath s₁ t (List.replicate n none) ∧ s₂ ∈ M.step t none
⊢ s₂ ∈ M.εClosure {s₁}
have succ : ∀ (t : σ), M.IsPath s₁ t (List.replicate n none) → s₂ ∈ M.step t none → s₂ ∈ M.εClosure {s₁}
Tactic: obtain ⟨t, _, _⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
⊢ s₂ ∈ M.evalFrom {s₁} [] ↔ ∃ (x' : List (Option α)), x'.reduceOption = [] ∧ M.IsPath s₁ s₂ x'
have nil : (∃ (n : ℕ), M.IsPath s₁ s₂ (List.replicate n none)) ↔ ∃ (x' : List (Option α)), x'.reduceOption = [] ∧ M.IsPath s₁ s₂ x'
Tactic: rw [evalFrom_nil, mem_εClosure_iff_exists_path]
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
⊢ (∃ (n : ℕ), M.IsPath s₁ s₂ (List.replicate n none)) ↔
    ∃ (x' : List (Option α)), x'.reduceOption = [] ∧ M.IsPath s₁ s₂ x'
have nil : (∃ (n : ℕ), M.IsPath s₁ s₂ (List.replicate n none)) → ∃ (x' : List (Option α)), x'.reduceOption = [] ∧ M.IsPath s₁ s₂ x'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
nil :
  (∃ (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)) ↔
    ∃ (x' : List (Option α)), x'.reduceOption = [] ∧ M.IsPath s₁ s₂ x'
have nil₁ : (∃ (x' : List (Option α)), x'.reduceOption = [] ∧ M.IsPath s₁ s₂ x') → ∃ (n : ℕ), M.IsPath s₁ s₂ (List.replicate n none)
Tactic: constructor