Theorem: match_epsilon_EpsilonNFA_toAbstract (FOL/Parsing/RegExpToEpsilonNFA.lean)

State before:
α : Type
inst✝ : DecidableEq α
⊢ (match_epsilon_EpsilonNFA α).toAbstract = match_epsilon_AbstractEpsilonNFA α
Tactic:
simp only [match_epsilon_EpsilonNFA]
State after:
α : Type
inst✝ : DecidableEq α
⊢ { symbol_arrow_list := [], epsilon_arrow_list := [{ start_state := 0, stop_state_list := [1] }],
        starting_state_list := [0], accepting_state_list := [1] }.toAbstract =
    match_epsilon_AbstractEpsilonNFA α

State before:
α : Type
inst✝ : DecidableEq α
⊢ { symbol_arrow_list := [], epsilon_arrow_list := [{ start_state := 0, stop_state_list := [1] }],
        starting_state_list := [0], accepting_state_list := [1] }.toAbstract =
    match_epsilon_AbstractEpsilonNFA α
Tactic:
simp only [EpsilonNFA.toAbstract]
State after:
α : Type
inst✝ : DecidableEq α
⊢ {
      symbol := fun start_state symbol stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, symbol := symbol, stop_state_list := stop_state_list } ∈ [] ∧
            stop_state ∈ stop_state_list,
      epsilon := fun start_state stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, stop_state_list := stop_state_list } ∈
              [{ start_state := 0, stop_state_list := [1] }] ∧
            stop_state ∈ stop_state_list,
      start := fun state => state ∈ [0], accepting := fun state => state ∈ [1] } =
    match_epsilon_AbstractEpsilonNFA α

State before:
α : Type
inst✝ : DecidableEq α
⊢ {
      symbol := fun start_state symbol stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, symbol := symbol, stop_state_list := stop_state_list } ∈ [] ∧
            stop_state ∈ stop_state_list,
      epsilon := fun start_state stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, stop_state_list := stop_state_list } ∈
              [{ start_state := 0, stop_state_list := [1] }] ∧
            stop_state ∈ stop_state_list,
      start := fun state => state ∈ [0], accepting := fun state => state ∈ [1] } =
    match_epsilon_AbstractEpsilonNFA α
Tactic:
simp only [match_epsilon_AbstractEpsilonNFA]
State after:
α : Type
inst✝ : DecidableEq α
⊢ {
      symbol := fun start_state symbol stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, symbol := symbol, stop_state_list := stop_state_list } ∈ [] ∧
            stop_state ∈ stop_state_list,
      epsilon := fun start_state stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, stop_state_list := stop_state_list } ∈
              [{ start_state := 0, stop_state_list := [1] }] ∧
            stop_state ∈ stop_state_list,
      start := fun state => state ∈ [0], accepting := fun state => state ∈ [1] } =
    { symbol := fun x x x => False, epsilon := fun p q => p = 0 ∧ q = 1, start := fun p => p = 0,
      accepting := fun p => p = 1 }

State before:
α : Type
inst✝ : DecidableEq α
⊢ {
      symbol := fun start_state symbol stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, symbol := symbol, stop_state_list := stop_state_list } ∈ [] ∧
            stop_state ∈ stop_state_list,
      epsilon := fun start_state stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, stop_state_list := stop_state_list } ∈
              [{ start_state := 0, stop_state_list := [1] }] ∧
            stop_state ∈ stop_state_list,
      start := fun state => state ∈ [0], accepting := fun state => state ∈ [1] } =
    { symbol := fun x x x => False, epsilon := fun p q => p = 0 ∧ q = 1, start := fun p => p = 0,
      accepting := fun p => p = 1 }
Tactic:
simp
State after:
α : Type
inst✝ : DecidableEq α
⊢ (fun start_state stop_state =>
      ∃ stop_state_list, (start_state = 0 ∧ stop_state_list = [1]) ∧ stop_state ∈ stop_state_list) =
    fun p q => p = 0 ∧ q = 1

State before:
α : Type
inst✝ : DecidableEq α
⊢ (fun start_state stop_state =>
      ∃ stop_state_list, (start_state = 0 ∧ stop_state_list = [1]) ∧ stop_state ∈ stop_state_list) =
    fun p q => p = 0 ∧ q = 1
Tactic:
funext p q
State after:
case h.h
α : Type
inst✝ : DecidableEq α
p q : ℕ
⊢ (∃ stop_state_list, (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list) = (p = 0 ∧ q = 1)

State before:
case h.h
α : Type
inst✝ : DecidableEq α
p q : ℕ
⊢ (∃ stop_state_list, (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list) = (p = 0 ∧ q = 1)
Tactic:
simp
State after:
case h.h
α : Type
inst✝ : DecidableEq α
p q : ℕ
⊢ (∃ stop_state_list, (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list) ↔ p = 0 ∧ q = 1

State before:
case h.h
α : Type
inst✝ : DecidableEq α
p q : ℕ
⊢ (∃ stop_state_list, (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list) ↔ p = 0 ∧ q = 1
Tactic:
constructor
State after:
case h.h.mp
α : Type
inst✝ : DecidableEq α
p q : ℕ
⊢ (∃ stop_state_list, (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list) → p = 0 ∧ q = 1

case h.h.mpr
α : Type
inst✝ : DecidableEq α
p q : ℕ
⊢ p = 0 ∧ q = 1 → ∃ stop_state_list, (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list

State before:
case h.h.mp
α : Type
inst✝ : DecidableEq α
p q : ℕ
⊢ (∃ stop_state_list, (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list) → p = 0 ∧ q = 1
Tactic:
intro a1
State after:
case h.h.mp
α : Type
inst✝ : DecidableEq α
p q : ℕ
a1 : ∃ stop_state_list, (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list
⊢ p = 0 ∧ q = 1

State before:
case h.h.mp
α : Type
inst✝ : DecidableEq α
p q : ℕ
a1 : ∃ stop_state_list, (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list
⊢ p = 0 ∧ q = 1
Tactic:
apply Exists.elim a1
State after:
case h.h.mp
α : Type
inst✝ : DecidableEq α
p q : ℕ
a1 : ∃ stop_state_list, (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list
⊢ ∀ (a : List ℕ), (p = 0 ∧ a = [1]) ∧ q ∈ a → p = 0 ∧ q = 1

State before:
case h.h.mp
α : Type
inst✝ : DecidableEq α
p q : ℕ
a1 : ∃ stop_state_list, (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list
⊢ ∀ (a : List ℕ), (p = 0 ∧ a = [1]) ∧ q ∈ a → p = 0 ∧ q = 1
Tactic:
intro stop_state_list a2
State after:
case h.h.mp
α : Type
inst✝ : DecidableEq α
p q : ℕ
a1 : ∃ stop_state_list, (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list
stop_state_list : List ℕ
a2 : (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list
⊢ p = 0 ∧ q = 1

State before:
case h.h.mp
α : Type
inst✝ : DecidableEq α
p q : ℕ
a1 : ∃ stop_state_list, (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list
stop_state_list : List ℕ
a2 : (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list
⊢ p = 0 ∧ q = 1
Tactic:
clear a1
State after:
case h.h.mp
α : Type
inst✝ : DecidableEq α
p q : ℕ
stop_state_list : List ℕ
a2 : (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list
⊢ p = 0 ∧ q = 1

State before:
case h.h.mp
α : Type
inst✝ : DecidableEq α
p q : ℕ
stop_state_list : List ℕ
a2 : (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list
⊢ p = 0 ∧ q = 1
Tactic:
cases a2
State after:
case h.h.mp.intro
α : Type
inst✝ : DecidableEq α
p q : ℕ
stop_state_list : List ℕ
left✝ : p = 0 ∧ stop_state_list = [1]
right✝ : q ∈ stop_state_list
⊢ p = 0 ∧ q = 1

State before:
α : Type
inst✝ : DecidableEq α
p q : ℕ
stop_state_list : List ℕ
a2_left : p = 0 ∧ stop_state_list = [1]
a2_right : q ∈ stop_state_list
⊢ p = 0 ∧ q = 1
Tactic:
case _ a2_left a2_right =>
  cases a2_left
  case _ a2_left_left a2_left_right =>
    simp only [a2_left_right] at a2_right
    simp at a2_right
    tauto
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
p q : ℕ
stop_state_list : List ℕ
a2_left : p = 0 ∧ stop_state_list = [1]
a2_right : q ∈ stop_state_list
⊢ p = 0 ∧ q = 1
Tactic:
cases a2_left
State after:
case intro
α : Type
inst✝ : DecidableEq α
p q : ℕ
stop_state_list : List ℕ
a2_right : q ∈ stop_state_list
left✝ : p = 0
right✝ : stop_state_list = [1]
⊢ p = 0 ∧ q = 1

State before:
α : Type
inst✝ : DecidableEq α
p q : ℕ
stop_state_list : List ℕ
a2_right : q ∈ stop_state_list
a2_left_left : p = 0
a2_left_right : stop_state_list = [1]
⊢ p = 0 ∧ q = 1
Tactic:
case _ a2_left_left a2_left_right =>
  simp only [a2_left_right] at a2_right
  simp at a2_right
  tauto
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
p q : ℕ
stop_state_list : List ℕ
a2_right : q ∈ stop_state_list
a2_left_left : p = 0
a2_left_right : stop_state_list = [1]
⊢ p = 0 ∧ q = 1
Tactic:
simp only [a2_left_right] at a2_right
State after:
α : Type
inst✝ : DecidableEq α
p q : ℕ
stop_state_list : List ℕ
a2_left_left : p = 0
a2_left_right : stop_state_list = [1]
a2_right : q ∈ [1]
⊢ p = 0 ∧ q = 1

State before:
α : Type
inst✝ : DecidableEq α
p q : ℕ
stop_state_list : List ℕ
a2_left_left : p = 0
a2_left_right : stop_state_list = [1]
a2_right : q ∈ [1]
⊢ p = 0 ∧ q = 1
Tactic:
simp at a2_right
State after:
α : Type
inst✝ : DecidableEq α
p q : ℕ
stop_state_list : List ℕ
a2_left_left : p = 0
a2_left_right : stop_state_list = [1]
a2_right : q = 1
⊢ p = 0 ∧ q = 1

State before:
α : Type
inst✝ : DecidableEq α
p q : ℕ
stop_state_list : List ℕ
a2_left_left : p = 0
a2_left_right : stop_state_list = [1]
a2_right : q = 1
⊢ p = 0 ∧ q = 1
Tactic:
tauto
State after:
no goals

State before:
case h.h.mpr
α : Type
inst✝ : DecidableEq α
p q : ℕ
⊢ p = 0 ∧ q = 1 → ∃ stop_state_list, (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list
Tactic:
intro a1
State after:
case h.h.mpr
α : Type
inst✝ : DecidableEq α
p q : ℕ
a1 : p = 0 ∧ q = 1
⊢ ∃ stop_state_list, (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list

State before:
case h.h.mpr
α : Type
inst✝ : DecidableEq α
p q : ℕ
a1 : p = 0 ∧ q = 1
⊢ ∃ stop_state_list, (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list
Tactic:
apply Exists.intro [1]
State after:
case h.h.mpr
α : Type
inst✝ : DecidableEq α
p q : ℕ
a1 : p = 0 ∧ q = 1
⊢ (p = 0 ∧ [1] = [1]) ∧ q ∈ [1]

State before:
case h.h.mpr
α : Type
inst✝ : DecidableEq α
p q : ℕ
a1 : p = 0 ∧ q = 1
⊢ (p = 0 ∧ [1] = [1]) ∧ q ∈ [1]
Tactic:
simp
State after:
case h.h.mpr
α : Type
inst✝ : DecidableEq α
p q : ℕ
a1 : p = 0 ∧ q = 1
⊢ p = 0 ∧ q = 1

State before:
case h.h.mpr
α : Type
inst✝ : DecidableEq α
p q : ℕ
a1 : p = 0 ∧ q = 1
⊢ p = 0 ∧ q = 1
Tactic:
exact a1
State after:
no goals