Theorem: EpsilonNFA.eval_from_iff (FOL/Parsing/EpsilonNFA.lean)

State before:
case nil
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
S : List σ
⊢ (∃ s ∈ M.epsilon_closure S, s ∈ M.accepting_state_list) ↔ ∃ s ∈ S, M.toAbstract.eval s []
Tactic:
simp [epsilon_closure_iff]
State after:
case nil
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
S : List σ
⊢ (∃ s, (∃ start_state ∈ S, M.toAbstract.EpsilonClosure start_state s) ∧ s ∈ M.accepting_state_list) ↔
    ∃ s ∈ S, M.toAbstract.eval s []

State before:
case nil
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
S : List σ
⊢ (∃ s, (∃ start_state ∈ S, M.toAbstract.EpsilonClosure start_state s) ∧ s ∈ M.accepting_state_list) ↔
    ∃ s ∈ S, M.toAbstract.eval s []
Tactic:
constructor
State after:
case nil.mp
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
S : List σ
⊢ (∃ s, (∃ start_state ∈ S, M.toAbstract.EpsilonClosure start_state s) ∧ s ∈ M.accepting_state_list) →
    ∃ s ∈ S, M.toAbstract.eval s []

case nil.mpr
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
S : List σ
⊢ (∃ s ∈ S, M.toAbstract.eval s []) →
    ∃ s, (∃ start_state ∈ S, M.toAbstract.EpsilonClosure start_state s) ∧ s ∈ M.accepting_state_list

State before:
case nil.mp
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
S : List σ
⊢ (∃ s, (∃ start_state ∈ S, M.toAbstract.EpsilonClosure start_state s) ∧ s ∈ M.accepting_state_list) →
    ∃ s ∈ S, M.toAbstract.eval s []
Tactic:
intro ⟨s, ⟨s', h1, h2⟩, h3⟩
State after:
case nil.mp
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
S : List σ
s s' : σ
h1 : s' ∈ S
h2 : M.toAbstract.EpsilonClosure s' s
h3 : s ∈ M.accepting_state_list
⊢ ∃ s ∈ S, M.toAbstract.eval s []

State before:
case nil.mp
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
S : List σ
s s' : σ
h1 : s' ∈ S
h2 : M.toAbstract.EpsilonClosure s' s
h3 : s ∈ M.accepting_state_list
⊢ ∃ s ∈ S, M.toAbstract.eval s []
Tactic:
refine ⟨_, h1, ?_⟩
State after:
case nil.mp
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
S : List σ
s s' : σ
h1 : s' ∈ S
h2 : M.toAbstract.EpsilonClosure s' s
h3 : s ∈ M.accepting_state_list
⊢ M.toAbstract.eval s' []

State before:
case nil.mp
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
S : List σ
s s' : σ
h1 : s' ∈ S
h2 : M.toAbstract.EpsilonClosure s' s
h3 : s ∈ M.accepting_state_list
⊢ M.toAbstract.eval s' []
Tactic:
clear h1
State after:
case nil.mp
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
S : List σ
s s' : σ
h2 : M.toAbstract.EpsilonClosure s' s
h3 : s ∈ M.accepting_state_list
⊢ M.toAbstract.eval s' []

State before:
case nil.mp
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
S : List σ
s s' : σ
h2 : M.toAbstract.EpsilonClosure s' s
h3 : s ∈ M.accepting_state_list
⊢ M.toAbstract.eval s' []
Tactic:
induction h2 using Relation.ReflTransGen.head_induction_on with
| refl => exact .accept _ h3
| head h _ ih => exact .eps _ _ _ ih h
State after:
no goals

State before:
case nil.mp.refl
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
S : List σ
s s' : σ
h3 : s ∈ M.accepting_state_list
⊢ M.toAbstract.eval s []
Tactic:
exact .accept _ h3
State after:
no goals

State before:
case nil.mp.head
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
S : List σ
s s' : σ
h3 : s ∈ M.accepting_state_list
a✝ c✝ : σ
h : M.toAbstract.epsilon a✝ c✝
h✝ : Relation.ReflTransGen M.toAbstract.epsilon c✝ s
ih : M.toAbstract.eval c✝ []
⊢ M.toAbstract.eval a✝ []
Tactic:
exact .eps _ _ _ ih h
State after:
no goals

State before:
case nil.mpr
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
S : List σ
⊢ (∃ s ∈ S, M.toAbstract.eval s []) →
    ∃ s, (∃ start_state ∈ S, M.toAbstract.EpsilonClosure start_state s) ∧ s ∈ M.accepting_state_list
Tactic:
intro ⟨s, h1, h2⟩
State after:
case nil.mpr
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
S : List σ
s : σ
h1 : s ∈ S
h2 : M.toAbstract.eval s []
⊢ ∃ s, (∃ start_state ∈ S, M.toAbstract.EpsilonClosure start_state s) ∧ s ∈ M.accepting_state_list

State before:
case nil.mpr
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
S : List σ
s : σ
h1 : s ∈ S
h2 : M.toAbstract.eval s []
⊢ ∃ s, (∃ start_state ∈ S, M.toAbstract.EpsilonClosure start_state s) ∧ s ∈ M.accepting_state_list
Tactic:
obtain ⟨s', h3, h4⟩ : ∃ s', M.toAbstract.EpsilonClosure s s' ∧ s' ∈ M.accepting_state_list := by
  clear h1; generalize e : [] = l at h2
  induction h2 with cases e
  | accept _ h' => exact ⟨_, .refl, h'⟩
  | eps _ _ _ _ h2 ih =>
    have ⟨s', h3, h4⟩ := ih rfl
    exact ⟨_, .head h2 h3, h4⟩
State after:
case nil.mpr.intro.intro
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
S : List σ
s : σ
h1 : s ∈ S
h2 : M.toAbstract.eval s []
s' : σ
h3 : M.toAbstract.EpsilonClosure s s'
h4 : s' ∈ M.accepting_state_list
⊢ ∃ s, (∃ start_state ∈ S, M.toAbstract.EpsilonClosure start_state s) ∧ s ∈ M.accepting_state_list

State before:
case nil.mpr.intro.intro
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
S : List σ
s : σ
h1 : s ∈ S
h2 : M.toAbstract.eval s []
s' : σ
h3 : M.toAbstract.EpsilonClosure s s'
h4 : s' ∈ M.accepting_state_list
⊢ ∃ s, (∃ start_state ∈ S, M.toAbstract.EpsilonClosure start_state s) ∧ s ∈ M.accepting_state_list
Tactic:
exact ⟨_, ⟨_, h1, h3⟩, h4⟩
State after:
no goals

State before:
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
S : List σ
s : σ
h1 : s ∈ S
h2 : M.toAbstract.eval s []
⊢ ∃ s', M.toAbstract.EpsilonClosure s s' ∧ s' ∈ M.accepting_state_list
Tactic:
clear h1
State after:
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
S : List σ
s : σ
h2 : M.toAbstract.eval s []
⊢ ∃ s', M.toAbstract.EpsilonClosure s s' ∧ s' ∈ M.accepting_state_list

State before:
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
S : List σ
s : σ
h2 : M.toAbstract.eval s []
⊢ ∃ s', M.toAbstract.EpsilonClosure s s' ∧ s' ∈ M.accepting_state_list
Tactic:
generalize e : [] = l at h2
State after:
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
S : List σ
s : σ
l : List α
e : [] = l
h2 : M.toAbstract.eval s l
⊢ ∃ s', M.toAbstract.EpsilonClosure s s' ∧ s' ∈ M.accepting_state_list

State before:
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
S : List σ
s : σ
l : List α
e : [] = l
h2 : M.toAbstract.eval s l
⊢ ∃ s', M.toAbstract.EpsilonClosure s s' ∧ s' ∈ M.accepting_state_list
Tactic:
induction h2 with cases e
| accept _ h' => exact ⟨_, .refl, h'⟩
| eps _ _ _ _ h2 ih =>
  have ⟨s', h3, h4⟩ := ih rfl
  exact ⟨_, .head h2 h3, h4⟩
State after:
no goals

State before:
case accept.refl
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
S : List σ
s : σ
l : List α
start_state✝ : σ
h' : M.toAbstract.accepting start_state✝
⊢ ∃ s', M.toAbstract.EpsilonClosure start_state✝ s' ∧ s' ∈ M.accepting_state_list
Tactic:
exact ⟨_, .refl, h'⟩
State after:
no goals

State before:
case eps.refl
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
S : List σ
s : σ
l : List α
start_state✝ stop_state✝ : σ
h2 : M.toAbstract.epsilon start_state✝ stop_state✝
a✝ : M.toAbstract.eval stop_state✝ []
ih : [] = [] → ∃ s', M.toAbstract.EpsilonClosure stop_state✝ s' ∧ s' ∈ M.accepting_state_list
⊢ ∃ s', M.toAbstract.EpsilonClosure start_state✝ s' ∧ s' ∈ M.accepting_state_list
Tactic:
have ⟨s', h3, h4⟩ := ih rfl
State after:
case eps.refl
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
S : List σ
s : σ
l : List α
start_state✝ stop_state✝ : σ
h2 : M.toAbstract.epsilon start_state✝ stop_state✝
a✝ : M.toAbstract.eval stop_state✝ []
ih : [] = [] → ∃ s', M.toAbstract.EpsilonClosure stop_state✝ s' ∧ s' ∈ M.accepting_state_list
s' : σ
h3 : M.toAbstract.EpsilonClosure stop_state✝ s'
h4 : s' ∈ M.accepting_state_list
⊢ ∃ s', M.toAbstract.EpsilonClosure start_state✝ s' ∧ s' ∈ M.accepting_state_list

State before:
case eps.refl
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
S : List σ
s : σ
l : List α
start_state✝ stop_state✝ : σ
h2 : M.toAbstract.epsilon start_state✝ stop_state✝
a✝ : M.toAbstract.eval stop_state✝ []
ih : [] = [] → ∃ s', M.toAbstract.EpsilonClosure stop_state✝ s' ∧ s' ∈ M.accepting_state_list
s' : σ
h3 : M.toAbstract.EpsilonClosure stop_state✝ s'
h4 : s' ∈ M.accepting_state_list
⊢ ∃ s', M.toAbstract.EpsilonClosure start_state✝ s' ∧ s' ∈ M.accepting_state_list
Tactic:
exact ⟨_, .head h2 h3, h4⟩
State after:
no goals

State before:
case cons
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
a : α
as : List α
IH : ∀ (S : List σ), (∃ s ∈ M.eval_from S as, s ∈ M.accepting_state_list) ↔ ∃ s ∈ S, M.toAbstract.eval s as
S : List σ
⊢ (∃ s ∈ M.eval_from (M.eval_one_no_eps (M.epsilon_closure S) a) as, s ∈ M.accepting_state_list) ↔
    ∃ s ∈ S, M.toAbstract.eval s (a :: as)
Tactic:
simp [IH, epsilon_closure_iff, eval_one_no_eps_iff]
State after:
case cons
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
a : α
as : List α
IH : ∀ (S : List σ), (∃ s ∈ M.eval_from S as, s ∈ M.accepting_state_list) ↔ ∃ s ∈ S, M.toAbstract.eval s as
S : List σ
⊢ (∃ s,
      (∃ state, (∃ start_state ∈ S, M.toAbstract.EpsilonClosure start_state state) ∧ M.toAbstract.symbol state a s) ∧
        M.toAbstract.eval s as) ↔
    ∃ s ∈ S, M.toAbstract.eval s (a :: as)

State before:
case cons
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
a : α
as : List α
IH : ∀ (S : List σ), (∃ s ∈ M.eval_from S as, s ∈ M.accepting_state_list) ↔ ∃ s ∈ S, M.toAbstract.eval s as
S : List σ
⊢ (∃ s,
      (∃ state, (∃ start_state ∈ S, M.toAbstract.EpsilonClosure start_state state) ∧ M.toAbstract.symbol state a s) ∧
        M.toAbstract.eval s as) ↔
    ∃ s ∈ S, M.toAbstract.eval s (a :: as)
Tactic:
constructor
State after:
case cons.mp
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
a : α
as : List α
IH : ∀ (S : List σ), (∃ s ∈ M.eval_from S as, s ∈ M.accepting_state_list) ↔ ∃ s ∈ S, M.toAbstract.eval s as
S : List σ
⊢ (∃ s,
      (∃ state, (∃ start_state ∈ S, M.toAbstract.EpsilonClosure start_state state) ∧ M.toAbstract.symbol state a s) ∧
        M.toAbstract.eval s as) →
    ∃ s ∈ S, M.toAbstract.eval s (a :: as)

case cons.mpr
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
a : α
as : List α
IH : ∀ (S : List σ), (∃ s ∈ M.eval_from S as, s ∈ M.accepting_state_list) ↔ ∃ s ∈ S, M.toAbstract.eval s as
S : List σ
⊢ (∃ s ∈ S, M.toAbstract.eval s (a :: as)) →
    ∃ s,
      (∃ state, (∃ start_state ∈ S, M.toAbstract.EpsilonClosure start_state state) ∧ M.toAbstract.symbol state a s) ∧
        M.toAbstract.eval s as

State before:
case cons.mp
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
a : α
as : List α
IH : ∀ (S : List σ), (∃ s ∈ M.eval_from S as, s ∈ M.accepting_state_list) ↔ ∃ s ∈ S, M.toAbstract.eval s as
S : List σ
⊢ (∃ s,
      (∃ state, (∃ start_state ∈ S, M.toAbstract.EpsilonClosure start_state state) ∧ M.toAbstract.symbol state a s) ∧
        M.toAbstract.eval s as) →
    ∃ s ∈ S, M.toAbstract.eval s (a :: as)
Tactic:
intro ⟨s₁, ⟨s₂, ⟨s₃, h1, h2⟩, h3⟩, h4⟩
State after:
case cons.mp
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
a : α
as : List α
IH : ∀ (S : List σ), (∃ s ∈ M.eval_from S as, s ∈ M.accepting_state_list) ↔ ∃ s ∈ S, M.toAbstract.eval s as
S : List σ
s₁ s₂ s₃ : σ
h1 : s₃ ∈ S
h2 : M.toAbstract.EpsilonClosure s₃ s₂
h3 : M.toAbstract.symbol s₂ a s₁
h4 : M.toAbstract.eval s₁ as
⊢ ∃ s ∈ S, M.toAbstract.eval s (a :: as)

State before:
case cons.mp
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
a : α
as : List α
IH : ∀ (S : List σ), (∃ s ∈ M.eval_from S as, s ∈ M.accepting_state_list) ↔ ∃ s ∈ S, M.toAbstract.eval s as
S : List σ
s₁ s₂ s₃ : σ
h1 : s₃ ∈ S
h2 : M.toAbstract.EpsilonClosure s₃ s₂
h3 : M.toAbstract.symbol s₂ a s₁
h4 : M.toAbstract.eval s₁ as
⊢ ∃ s ∈ S, M.toAbstract.eval s (a :: as)
Tactic:
refine ⟨_, h1, ?_⟩
State after:
case cons.mp
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
a : α
as : List α
IH : ∀ (S : List σ), (∃ s ∈ M.eval_from S as, s ∈ M.accepting_state_list) ↔ ∃ s ∈ S, M.toAbstract.eval s as
S : List σ
s₁ s₂ s₃ : σ
h1 : s₃ ∈ S
h2 : M.toAbstract.EpsilonClosure s₃ s₂
h3 : M.toAbstract.symbol s₂ a s₁
h4 : M.toAbstract.eval s₁ as
⊢ M.toAbstract.eval s₃ (a :: as)

State before:
case cons.mp
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
a : α
as : List α
IH : ∀ (S : List σ), (∃ s ∈ M.eval_from S as, s ∈ M.accepting_state_list) ↔ ∃ s ∈ S, M.toAbstract.eval s as
S : List σ
s₁ s₂ s₃ : σ
h1 : s₃ ∈ S
h2 : M.toAbstract.EpsilonClosure s₃ s₂
h3 : M.toAbstract.symbol s₂ a s₁
h4 : M.toAbstract.eval s₁ as
⊢ M.toAbstract.eval s₃ (a :: as)
Tactic:
clear h1
State after:
case cons.mp
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
a : α
as : List α
IH : ∀ (S : List σ), (∃ s ∈ M.eval_from S as, s ∈ M.accepting_state_list) ↔ ∃ s ∈ S, M.toAbstract.eval s as
S : List σ
s₁ s₂ s₃ : σ
h2 : M.toAbstract.EpsilonClosure s₃ s₂
h3 : M.toAbstract.symbol s₂ a s₁
h4 : M.toAbstract.eval s₁ as
⊢ M.toAbstract.eval s₃ (a :: as)

State before:
case cons.mp
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
a : α
as : List α
IH : ∀ (S : List σ), (∃ s ∈ M.eval_from S as, s ∈ M.accepting_state_list) ↔ ∃ s ∈ S, M.toAbstract.eval s as
S : List σ
s₁ s₂ s₃ : σ
h2 : M.toAbstract.EpsilonClosure s₃ s₂
h3 : M.toAbstract.symbol s₂ a s₁
h4 : M.toAbstract.eval s₁ as
⊢ M.toAbstract.eval s₃ (a :: as)
Tactic:
induction h2 using Relation.ReflTransGen.head_induction_on with
| refl => {apply AbstractEpsilonNFA.eval.sym _ _ _ _ h4 h3;  }
| head h _ ih => exact .eps _ _ _ ih h
State after:
no goals

State before:
case cons.mp.refl
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
a : α
as : List α
IH : ∀ (S : List σ), (∃ s ∈ M.eval_from S as, s ∈ M.accepting_state_list) ↔ ∃ s ∈ S, M.toAbstract.eval s as
S : List σ
s₁ s₂ s₃ : σ
h3 : M.toAbstract.symbol s₂ a s₁
h4 : M.toAbstract.eval s₁ as
⊢ M.toAbstract.eval s₂ (a :: as)
Tactic:
apply AbstractEpsilonNFA.eval.sym _ _ _ _ h4 h3
State after:
no goals

State before:
case cons.mp.head
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
a : α
as : List α
IH : ∀ (S : List σ), (∃ s ∈ M.eval_from S as, s ∈ M.accepting_state_list) ↔ ∃ s ∈ S, M.toAbstract.eval s as
S : List σ
s₁ s₂ s₃ : σ
h3 : M.toAbstract.symbol s₂ a s₁
h4 : M.toAbstract.eval s₁ as
a✝ c✝ : σ
h : M.toAbstract.epsilon a✝ c✝
h✝ : Relation.ReflTransGen M.toAbstract.epsilon c✝ s₂
ih : M.toAbstract.eval c✝ (a :: as)
⊢ M.toAbstract.eval a✝ (a :: as)
Tactic:
exact .eps _ _ _ ih h
State after:
no goals

State before:
case cons.mpr
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
a : α
as : List α
IH : ∀ (S : List σ), (∃ s ∈ M.eval_from S as, s ∈ M.accepting_state_list) ↔ ∃ s ∈ S, M.toAbstract.eval s as
S : List σ
⊢ (∃ s ∈ S, M.toAbstract.eval s (a :: as)) →
    ∃ s,
      (∃ state, (∃ start_state ∈ S, M.toAbstract.EpsilonClosure start_state state) ∧ M.toAbstract.symbol state a s) ∧
        M.toAbstract.eval s as
Tactic:
intro ⟨s, h1, h2⟩
State after:
case cons.mpr
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
a : α
as : List α
IH : ∀ (S : List σ), (∃ s ∈ M.eval_from S as, s ∈ M.accepting_state_list) ↔ ∃ s ∈ S, M.toAbstract.eval s as
S : List σ
s : σ
h1 : s ∈ S
h2 : M.toAbstract.eval s (a :: as)
⊢ ∃ s,
    (∃ state, (∃ start_state ∈ S, M.toAbstract.EpsilonClosure start_state state) ∧ M.toAbstract.symbol state a s) ∧
      M.toAbstract.eval s as

State before:
case cons.mpr
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
a : α
as : List α
IH : ∀ (S : List σ), (∃ s ∈ M.eval_from S as, s ∈ M.accepting_state_list) ↔ ∃ s ∈ S, M.toAbstract.eval s as
S : List σ
s : σ
h1 : s ∈ S
h2 : M.toAbstract.eval s (a :: as)
⊢ ∃ s,
    (∃ state, (∃ start_state ∈ S, M.toAbstract.EpsilonClosure start_state state) ∧ M.toAbstract.symbol state a s) ∧
      M.toAbstract.eval s as
Tactic:
obtain ⟨s₁, s₂, h3, h4, h5⟩ :
    ∃ s₁ s₂, M.toAbstract.EpsilonClosure s s₂ ∧
      M.toAbstract.symbol s₂ a s₁ ∧ M.toAbstract.eval s₁ as := by
  clear h1; generalize e : a::as = l at h2
  induction h2 with cases e
  | sym _ _ _ _ h1 h2 => exact ⟨_, _, .refl, h2, h1⟩
  | eps _ _ _ h1 h2 ih =>
    have ⟨s₁, s₂, h3, h4, h5⟩ := ih rfl
    exact ⟨_, _, .head h2 h3, h4, h5⟩
State after:
case cons.mpr.intro.intro.intro.intro
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
a : α
as : List α
IH : ∀ (S : List σ), (∃ s ∈ M.eval_from S as, s ∈ M.accepting_state_list) ↔ ∃ s ∈ S, M.toAbstract.eval s as
S : List σ
s : σ
h1 : s ∈ S
h2 : M.toAbstract.eval s (a :: as)
s₁ s₂ : σ
h3 : M.toAbstract.EpsilonClosure s s₂
h4 : M.toAbstract.symbol s₂ a s₁
h5 : M.toAbstract.eval s₁ as
⊢ ∃ s,
    (∃ state, (∃ start_state ∈ S, M.toAbstract.EpsilonClosure start_state state) ∧ M.toAbstract.symbol state a s) ∧
      M.toAbstract.eval s as

State before:
case cons.mpr.intro.intro.intro.intro
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
a : α
as : List α
IH : ∀ (S : List σ), (∃ s ∈ M.eval_from S as, s ∈ M.accepting_state_list) ↔ ∃ s ∈ S, M.toAbstract.eval s as
S : List σ
s : σ
h1 : s ∈ S
h2 : M.toAbstract.eval s (a :: as)
s₁ s₂ : σ
h3 : M.toAbstract.EpsilonClosure s s₂
h4 : M.toAbstract.symbol s₂ a s₁
h5 : M.toAbstract.eval s₁ as
⊢ ∃ s,
    (∃ state, (∃ start_state ∈ S, M.toAbstract.EpsilonClosure start_state state) ∧ M.toAbstract.symbol state a s) ∧
      M.toAbstract.eval s as
Tactic:
exact ⟨_, ⟨_, ⟨_, h1, h3⟩, h4⟩, h5⟩
State after:
no goals

State before:
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
a : α
as : List α
IH : ∀ (S : List σ), (∃ s ∈ M.eval_from S as, s ∈ M.accepting_state_list) ↔ ∃ s ∈ S, M.toAbstract.eval s as
S : List σ
s : σ
h1 : s ∈ S
h2 : M.toAbstract.eval s (a :: as)
⊢ ∃ s₁ s₂, M.toAbstract.EpsilonClosure s s₂ ∧ M.toAbstract.symbol s₂ a s₁ ∧ M.toAbstract.eval s₁ as
Tactic:
clear h1
State after:
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
a : α
as : List α
IH : ∀ (S : List σ), (∃ s ∈ M.eval_from S as, s ∈ M.accepting_state_list) ↔ ∃ s ∈ S, M.toAbstract.eval s as
S : List σ
s : σ
h2 : M.toAbstract.eval s (a :: as)
⊢ ∃ s₁ s₂, M.toAbstract.EpsilonClosure s s₂ ∧ M.toAbstract.symbol s₂ a s₁ ∧ M.toAbstract.eval s₁ as

State before:
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
a : α
as : List α
IH : ∀ (S : List σ), (∃ s ∈ M.eval_from S as, s ∈ M.accepting_state_list) ↔ ∃ s ∈ S, M.toAbstract.eval s as
S : List σ
s : σ
h2 : M.toAbstract.eval s (a :: as)
⊢ ∃ s₁ s₂, M.toAbstract.EpsilonClosure s s₂ ∧ M.toAbstract.symbol s₂ a s₁ ∧ M.toAbstract.eval s₁ as
Tactic:
generalize e : a::as = l at h2
State after:
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
a : α
as : List α
IH : ∀ (S : List σ), (∃ s ∈ M.eval_from S as, s ∈ M.accepting_state_list) ↔ ∃ s ∈ S, M.toAbstract.eval s as
S : List σ
s : σ
l : List α
e : a :: as = l
h2 : M.toAbstract.eval s l
⊢ ∃ s₁ s₂, M.toAbstract.EpsilonClosure s s₂ ∧ M.toAbstract.symbol s₂ a s₁ ∧ M.toAbstract.eval s₁ as

State before:
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
a : α
as : List α
IH : ∀ (S : List σ), (∃ s ∈ M.eval_from S as, s ∈ M.accepting_state_list) ↔ ∃ s ∈ S, M.toAbstract.eval s as
S : List σ
s : σ
l : List α
e : a :: as = l
h2 : M.toAbstract.eval s l
⊢ ∃ s₁ s₂, M.toAbstract.EpsilonClosure s s₂ ∧ M.toAbstract.symbol s₂ a s₁ ∧ M.toAbstract.eval s₁ as
Tactic:
induction h2 with cases e
| sym _ _ _ _ h1 h2 => exact ⟨_, _, .refl, h2, h1⟩
| eps _ _ _ h1 h2 ih =>
  have ⟨s₁, s₂, h3, h4, h5⟩ := ih rfl
  exact ⟨_, _, .head h2 h3, h4, h5⟩
State after:
no goals

State before:
case sym.refl
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
a : α
as : List α
IH : ∀ (S : List σ), (∃ s ∈ M.eval_from S as, s ∈ M.accepting_state_list) ↔ ∃ s ∈ S, M.toAbstract.eval s as
S : List σ
s : σ
l : List α
start_state✝ stop_state✝ : σ
h2 : M.toAbstract.symbol start_state✝ a stop_state✝
h1 : M.toAbstract.eval stop_state✝ as
a_ih✝ :
  a :: as = as →
    ∃ s₁ s₂, M.toAbstract.EpsilonClosure stop_state✝ s₂ ∧ M.toAbstract.symbol s₂ a s₁ ∧ M.toAbstract.eval s₁ as
⊢ ∃ s₁ s₂, M.toAbstract.EpsilonClosure start_state✝ s₂ ∧ M.toAbstract.symbol s₂ a s₁ ∧ M.toAbstract.eval s₁ as
Tactic:
exact ⟨_, _, .refl, h2, h1⟩
State after:
no goals

State before:
case eps.refl
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
a : α
as : List α
IH : ∀ (S : List σ), (∃ s ∈ M.eval_from S as, s ∈ M.accepting_state_list) ↔ ∃ s ∈ S, M.toAbstract.eval s as
S : List σ
s : σ
l : List α
start_state✝ stop_state✝ : σ
h2 : M.toAbstract.epsilon start_state✝ stop_state✝
h1 : M.toAbstract.eval stop_state✝ (a :: as)
ih :
  a :: as = a :: as →
    ∃ s₁ s₂, M.toAbstract.EpsilonClosure stop_state✝ s₂ ∧ M.toAbstract.symbol s₂ a s₁ ∧ M.toAbstract.eval s₁ as
⊢ ∃ s₁ s₂, M.toAbstract.EpsilonClosure start_state✝ s₂ ∧ M.toAbstract.symbol s₂ a s₁ ∧ M.toAbstract.eval s₁ as
Tactic:
have ⟨s₁, s₂, h3, h4, h5⟩ := ih rfl
State after:
case eps.refl
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
a : α
as : List α
IH : ∀ (S : List σ), (∃ s ∈ M.eval_from S as, s ∈ M.accepting_state_list) ↔ ∃ s ∈ S, M.toAbstract.eval s as
S : List σ
s : σ
l : List α
start_state✝ stop_state✝ : σ
h2 : M.toAbstract.epsilon start_state✝ stop_state✝
h1 : M.toAbstract.eval stop_state✝ (a :: as)
ih :
  a :: as = a :: as →
    ∃ s₁ s₂, M.toAbstract.EpsilonClosure stop_state✝ s₂ ∧ M.toAbstract.symbol s₂ a s₁ ∧ M.toAbstract.eval s₁ as
s₁ s₂ : σ
h3 : M.toAbstract.EpsilonClosure stop_state✝ s₂
h4 : M.toAbstract.symbol s₂ a s₁
h5 : M.toAbstract.eval s₁ as
⊢ ∃ s₁ s₂, M.toAbstract.EpsilonClosure start_state✝ s₂ ∧ M.toAbstract.symbol s₂ a s₁ ∧ M.toAbstract.eval s₁ as

State before:
case eps.refl
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
a : α
as : List α
IH : ∀ (S : List σ), (∃ s ∈ M.eval_from S as, s ∈ M.accepting_state_list) ↔ ∃ s ∈ S, M.toAbstract.eval s as
S : List σ
s : σ
l : List α
start_state✝ stop_state✝ : σ
h2 : M.toAbstract.epsilon start_state✝ stop_state✝
h1 : M.toAbstract.eval stop_state✝ (a :: as)
ih :
  a :: as = a :: as →
    ∃ s₁ s₂, M.toAbstract.EpsilonClosure stop_state✝ s₂ ∧ M.toAbstract.symbol s₂ a s₁ ∧ M.toAbstract.eval s₁ as
s₁ s₂ : σ
h3 : M.toAbstract.EpsilonClosure stop_state✝ s₂
h4 : M.toAbstract.symbol s₂ a s₁
h5 : M.toAbstract.eval s₁ as
⊢ ∃ s₁ s₂, M.toAbstract.EpsilonClosure start_state✝ s₂ ∧ M.toAbstract.symbol s₂ a s₁ ∧ M.toAbstract.eval s₁ as
Tactic:
exact ⟨_, _, .head h2 h3, h4, h5⟩
State after:
no goals