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

State before:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
state : σ
⊢ state ∈ e.epsilon_closure starting_state_list ↔
    ∃ start_state ∈ starting_state_list, e.toAbstract.EpsilonClosure start_state state
Tactic:
simp only [epsilon_closure]
State after:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
state : σ
⊢ state ∈ dft (epsilon_arrow_list_to_graph e.epsilon_arrow_list) starting_state_list ↔
    ∃ start_state ∈ starting_state_list, e.toAbstract.EpsilonClosure start_state state

State before:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
state : σ
⊢ state ∈ dft (epsilon_arrow_list_to_graph e.epsilon_arrow_list) starting_state_list ↔
    ∃ start_state ∈ starting_state_list, e.toAbstract.EpsilonClosure start_state state
Tactic:
simp only [dft_iff]
State after:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
state : σ
⊢ (∃ s ∈ starting_state_list,
      Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ epsilon_arrow_list_to_graph e.epsilon_arrow_list ∧ b ∈ l) s
        state) ↔
    ∃ start_state ∈ starting_state_list, e.toAbstract.EpsilonClosure start_state state

State before:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
state : σ
⊢ (∃ s ∈ starting_state_list,
      Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ epsilon_arrow_list_to_graph e.epsilon_arrow_list ∧ b ∈ l) s
        state) ↔
    ∃ start_state ∈ starting_state_list, e.toAbstract.EpsilonClosure start_state state
Tactic:
congr! with a b c
State after:
case a.h.e'_2.h.h.e'_2.h.e.h.e'_2.h.h.a
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
state a b c : σ
⊢ (∃ l, (b, l) ∈ epsilon_arrow_list_to_graph e.epsilon_arrow_list ∧ c ∈ l) ↔ e.toAbstract.epsilon b c

State before:
case a.h.e'_2.h.h.e'_2.h.e.h.e'_2.h.h.a
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
state a b c : σ
⊢ (∃ l, (b, l) ∈ epsilon_arrow_list_to_graph e.epsilon_arrow_list ∧ c ∈ l) ↔ e.toAbstract.epsilon b c
Tactic:
simp [toAbstract]
State after:
case a.h.e'_2.h.h.e'_2.h.e.h.e'_2.h.h.a
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
state a b c : σ
⊢ (∃ l, (b, l) ∈ epsilon_arrow_list_to_graph e.epsilon_arrow_list ∧ c ∈ l) ↔
    ∃ stop_state_list,
      { start_state := b, stop_state_list := stop_state_list } ∈ e.epsilon_arrow_list ∧ c ∈ stop_state_list

State before:
case a.h.e'_2.h.h.e'_2.h.e.h.e'_2.h.h.a
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
state a b c : σ
⊢ (∃ l, (b, l) ∈ epsilon_arrow_list_to_graph e.epsilon_arrow_list ∧ c ∈ l) ↔
    ∃ stop_state_list,
      { start_state := b, stop_state_list := stop_state_list } ∈ e.epsilon_arrow_list ∧ c ∈ stop_state_list
Tactic:
induction e.epsilon_arrow_list <;> simp [*, epsilon_arrow_list_to_graph, or_and_right, exists_or]
State after:
case a.h.e'_2.h.h.e'_2.h.e.h.e'_2.h.h.a.cons
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
state a b c : σ
head✝ : EpsilonArrow σ
tail✝ : List (EpsilonArrow σ)
tail_ih✝ :
  (∃ l, (b, l) ∈ epsilon_arrow_list_to_graph tail✝ ∧ c ∈ l) ↔
    ∃ stop_state_list, { start_state := b, stop_state_list := stop_state_list } ∈ tail✝ ∧ c ∈ stop_state_list
⊢ ((∃ x, (b = head✝.start_state ∧ x = head✝.stop_state_list) ∧ c ∈ x) ∨
      ∃ stop_state_list, { start_state := b, stop_state_list := stop_state_list } ∈ tail✝ ∧ c ∈ stop_state_list) ↔
    (∃ x, { start_state := b, stop_state_list := x } = head✝ ∧ c ∈ x) ∨
      ∃ stop_state_list, { start_state := b, stop_state_list := stop_state_list } ∈ tail✝ ∧ c ∈ stop_state_list

State before:
case a.h.e'_2.h.h.e'_2.h.e.h.e'_2.h.h.a.cons
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
state a b c : σ
head✝ : EpsilonArrow σ
tail✝ : List (EpsilonArrow σ)
tail_ih✝ :
  (∃ l, (b, l) ∈ epsilon_arrow_list_to_graph tail✝ ∧ c ∈ l) ↔
    ∃ stop_state_list, { start_state := b, stop_state_list := stop_state_list } ∈ tail✝ ∧ c ∈ stop_state_list
⊢ ((∃ x, (b = head✝.start_state ∧ x = head✝.stop_state_list) ∧ c ∈ x) ∨
      ∃ stop_state_list, { start_state := b, stop_state_list := stop_state_list } ∈ tail✝ ∧ c ∈ stop_state_list) ↔
    (∃ x, { start_state := b, stop_state_list := x } = head✝ ∧ c ∈ x) ∨
      ∃ stop_state_list, { start_state := b, stop_state_list := stop_state_list } ∈ tail✝ ∧ c ∈ stop_state_list
Tactic:
apply or_congr_left <| exists_congr fun a => and_congr_left fun _ => ?_
State after:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
state a✝ b c : σ
head✝ : EpsilonArrow σ
tail✝ : List (EpsilonArrow σ)
tail_ih✝ :
  (∃ l, (b, l) ∈ epsilon_arrow_list_to_graph tail✝ ∧ c ∈ l) ↔
    ∃ stop_state_list, { start_state := b, stop_state_list := stop_state_list } ∈ tail✝ ∧ c ∈ stop_state_list
a : List σ
x✝ : c ∈ a
⊢ b = head✝.start_state ∧ a = head✝.stop_state_list ↔ { start_state := b, stop_state_list := a } = head✝

State before:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
state a✝ b c : σ
head✝ : EpsilonArrow σ
tail✝ : List (EpsilonArrow σ)
tail_ih✝ :
  (∃ l, (b, l) ∈ epsilon_arrow_list_to_graph tail✝ ∧ c ∈ l) ↔
    ∃ stop_state_list, { start_state := b, stop_state_list := stop_state_list } ∈ tail✝ ∧ c ∈ stop_state_list
a : List σ
x✝ : c ∈ a
⊢ b = head✝.start_state ∧ a = head✝.stop_state_list ↔ { start_state := b, stop_state_list := a } = head✝
Tactic:
constructor <;> [rintro ⟨rfl, rfl⟩; rintro rfl] <;> [rfl; constructor <;> rfl]
State after:
no goals