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

State before:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
symbol : α
stop_state : σ
⊢ stop_state ∈ e.eval_one_no_eps starting_state_list symbol ↔
    ∃ state ∈ starting_state_list, e.toAbstract.symbol state symbol stop_state
Tactic:
simp only [EpsilonNFA.eval_one_no_eps]
State after:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
symbol : α
stop_state : σ
⊢ stop_state ∈
      (List.map (fun state => symbol_arrow_list_to_fun e.symbol_arrow_list state symbol)
            starting_state_list).join.dedup ↔
    ∃ state ∈ starting_state_list, e.toAbstract.symbol state symbol stop_state

State before:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
symbol : α
stop_state : σ
⊢ stop_state ∈
      (List.map (fun state => symbol_arrow_list_to_fun e.symbol_arrow_list state symbol)
            starting_state_list).join.dedup ↔
    ∃ state ∈ starting_state_list, e.toAbstract.symbol state symbol stop_state
Tactic:
simp only [EpsilonNFA.toAbstract]
State after:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
symbol : α
stop_state : σ
⊢ stop_state ∈
      (List.map (fun state => symbol_arrow_list_to_fun e.symbol_arrow_list state symbol)
            starting_state_list).join.dedup ↔
    ∃ state ∈ starting_state_list,
      ∃ stop_state_list,
        { start_state := state, symbol := symbol, stop_state_list := stop_state_list } ∈ e.symbol_arrow_list ∧
          stop_state ∈ stop_state_list

State before:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
symbol : α
stop_state : σ
⊢ stop_state ∈
      (List.map (fun state => symbol_arrow_list_to_fun e.symbol_arrow_list state symbol)
            starting_state_list).join.dedup ↔
    ∃ state ∈ starting_state_list,
      ∃ stop_state_list,
        { start_state := state, symbol := symbol, stop_state_list := stop_state_list } ∈ e.symbol_arrow_list ∧
          stop_state ∈ stop_state_list
Tactic:
simp only [symbol_arrow_list_to_fun]
State after:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
symbol : α
stop_state : σ
⊢ stop_state ∈
      (List.map
            (fun state =>
              (List.filterMap
                    (fun arrow =>
                      if arrow.start_state = state ∧ arrow.symbol = symbol then some arrow.stop_state_list else none)
                    e.symbol_arrow_list).join.dedup)
            starting_state_list).join.dedup ↔
    ∃ state ∈ starting_state_list,
      ∃ stop_state_list,
        { start_state := state, symbol := symbol, stop_state_list := stop_state_list } ∈ e.symbol_arrow_list ∧
          stop_state ∈ stop_state_list

State before:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
symbol : α
stop_state : σ
⊢ stop_state ∈
      (List.map
            (fun state =>
              (List.filterMap
                    (fun arrow =>
                      if arrow.start_state = state ∧ arrow.symbol = symbol then some arrow.stop_state_list else none)
                    e.symbol_arrow_list).join.dedup)
            starting_state_list).join.dedup ↔
    ∃ state ∈ starting_state_list,
      ∃ stop_state_list,
        { start_state := state, symbol := symbol, stop_state_list := stop_state_list } ∈ e.symbol_arrow_list ∧
          stop_state ∈ stop_state_list
Tactic:
simp
State after:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
symbol : α
stop_state : σ
⊢ (∃ a ∈ starting_state_list,
      ∃ l,
        (∃ a_1 ∈ e.symbol_arrow_list, (a_1.start_state = a ∧ a_1.symbol = symbol) ∧ a_1.stop_state_list = l) ∧
          stop_state ∈ l) ↔
    ∃ state ∈ starting_state_list,
      ∃ stop_state_list,
        { start_state := state, symbol := symbol, stop_state_list := stop_state_list } ∈ e.symbol_arrow_list ∧
          stop_state ∈ stop_state_list

State before:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
symbol : α
stop_state : σ
⊢ (∃ a ∈ starting_state_list,
      ∃ l,
        (∃ a_1 ∈ e.symbol_arrow_list, (a_1.start_state = a ∧ a_1.symbol = symbol) ∧ a_1.stop_state_list = l) ∧
          stop_state ∈ l) ↔
    ∃ state ∈ starting_state_list,
      ∃ stop_state_list,
        { start_state := state, symbol := symbol, stop_state_list := stop_state_list } ∈ e.symbol_arrow_list ∧
          stop_state ∈ stop_state_list
Tactic:
constructor
State after:
case mp
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
symbol : α
stop_state : σ
⊢ (∃ a ∈ starting_state_list,
      ∃ l,
        (∃ a_1 ∈ e.symbol_arrow_list, (a_1.start_state = a ∧ a_1.symbol = symbol) ∧ a_1.stop_state_list = l) ∧
          stop_state ∈ l) →
    ∃ state ∈ starting_state_list,
      ∃ stop_state_list,
        { start_state := state, symbol := symbol, stop_state_list := stop_state_list } ∈ e.symbol_arrow_list ∧
          stop_state ∈ stop_state_list

case mpr
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
symbol : α
stop_state : σ
⊢ (∃ state ∈ starting_state_list,
      ∃ stop_state_list,
        { start_state := state, symbol := symbol, stop_state_list := stop_state_list } ∈ e.symbol_arrow_list ∧
          stop_state ∈ stop_state_list) →
    ∃ a ∈ starting_state_list,
      ∃ l,
        (∃ a_1 ∈ e.symbol_arrow_list, (a_1.start_state = a ∧ a_1.symbol = symbol) ∧ a_1.stop_state_list = l) ∧
          stop_state ∈ l

State before:
case mp
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
symbol : α
stop_state : σ
⊢ (∃ a ∈ starting_state_list,
      ∃ l,
        (∃ a_1 ∈ e.symbol_arrow_list, (a_1.start_state = a ∧ a_1.symbol = symbol) ∧ a_1.stop_state_list = l) ∧
          stop_state ∈ l) →
    ∃ state ∈ starting_state_list,
      ∃ stop_state_list,
        { start_state := state, symbol := symbol, stop_state_list := stop_state_list } ∈ e.symbol_arrow_list ∧
          stop_state ∈ stop_state_list
Tactic:
rintro ⟨_, h1, _, ⟨⟨⟩, h2, ⟨rfl, rfl⟩, rfl⟩, h3⟩
State after:
case mp.intro.intro.intro.intro.intro.mk.intro.intro.intro
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
stop_state start_state✝ : σ
symbol✝ : α
stop_state_list✝ : List σ
h2 : { start_state := start_state✝, symbol := symbol✝, stop_state_list := stop_state_list✝ } ∈ e.symbol_arrow_list
h1 :
  { start_state := start_state✝, symbol := symbol✝, stop_state_list := stop_state_list✝ }.start_state ∈
    starting_state_list
h3 :
  stop_state ∈ { start_state := start_state✝, symbol := symbol✝, stop_state_list := stop_state_list✝ }.stop_state_list
⊢ ∃ state ∈ starting_state_list,
    ∃ stop_state_list,
      { start_state := state,
            symbol := { start_state := start_state✝, symbol := symbol✝, stop_state_list := stop_state_list✝ }.symbol,
            stop_state_list := stop_state_list } ∈
          e.symbol_arrow_list ∧
        stop_state ∈ stop_state_list

State before:
case mp.intro.intro.intro.intro.intro.mk.intro.intro.intro
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
stop_state start_state✝ : σ
symbol✝ : α
stop_state_list✝ : List σ
h2 : { start_state := start_state✝, symbol := symbol✝, stop_state_list := stop_state_list✝ } ∈ e.symbol_arrow_list
h1 :
  { start_state := start_state✝, symbol := symbol✝, stop_state_list := stop_state_list✝ }.start_state ∈
    starting_state_list
h3 :
  stop_state ∈ { start_state := start_state✝, symbol := symbol✝, stop_state_list := stop_state_list✝ }.stop_state_list
⊢ ∃ state ∈ starting_state_list,
    ∃ stop_state_list,
      { start_state := state,
            symbol := { start_state := start_state✝, symbol := symbol✝, stop_state_list := stop_state_list✝ }.symbol,
            stop_state_list := stop_state_list } ∈
          e.symbol_arrow_list ∧
        stop_state ∈ stop_state_list
Tactic:
exact ⟨_, h1, _, h2, h3⟩
State after:
no goals

State before:
case mpr
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
symbol : α
stop_state : σ
⊢ (∃ state ∈ starting_state_list,
      ∃ stop_state_list,
        { start_state := state, symbol := symbol, stop_state_list := stop_state_list } ∈ e.symbol_arrow_list ∧
          stop_state ∈ stop_state_list) →
    ∃ a ∈ starting_state_list,
      ∃ l,
        (∃ a_1 ∈ e.symbol_arrow_list, (a_1.start_state = a ∧ a_1.symbol = symbol) ∧ a_1.stop_state_list = l) ∧
          stop_state ∈ l
Tactic:
rintro ⟨_, h1, _, h2, h3⟩
State after:
case mpr.intro.intro.intro.intro
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
symbol : α
stop_state w✝¹ : σ
h1 : w✝¹ ∈ starting_state_list
w✝ : List σ
h2 : { start_state := w✝¹, symbol := symbol, stop_state_list := w✝ } ∈ e.symbol_arrow_list
h3 : stop_state ∈ w✝
⊢ ∃ a ∈ starting_state_list,
    ∃ l,
      (∃ a_1 ∈ e.symbol_arrow_list, (a_1.start_state = a ∧ a_1.symbol = symbol) ∧ a_1.stop_state_list = l) ∧
        stop_state ∈ l

State before:
case mpr.intro.intro.intro.intro
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
symbol : α
stop_state w✝¹ : σ
h1 : w✝¹ ∈ starting_state_list
w✝ : List σ
h2 : { start_state := w✝¹, symbol := symbol, stop_state_list := w✝ } ∈ e.symbol_arrow_list
h3 : stop_state ∈ w✝
⊢ ∃ a ∈ starting_state_list,
    ∃ l,
      (∃ a_1 ∈ e.symbol_arrow_list, (a_1.start_state = a ∧ a_1.symbol = symbol) ∧ a_1.stop_state_list = l) ∧
        stop_state ∈ l
Tactic:
exact ⟨_, h1, _, ⟨_, h2, ⟨rfl, rfl⟩, rfl⟩, h3⟩
State after:
no goals