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

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0
q_0 : σ_1
⊢ (∃ stop_state_list,
      ((∃ a ∈ M_0.epsilon_arrow_list,
            a.start_state = p_0 ∧ List.map (Sum.inr ∘ Sum.inl) a.stop_state_list = stop_state_list) ∨
          ∃ a ∈ M_0.accepting_state_list,
            a = p_0 ∧ List.map (Sum.inr ∘ Sum.inr) M_1.starting_state_list = stop_state_list) ∧
        Sum.inr (Sum.inr q_0) ∈ stop_state_list) ↔
    p_0 ∈ M_0.accepting_state_list ∧ q_0 ∈ M_1.starting_state_list
Tactic:
sorry
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
q : ℕ ⊕ σ_0 ⊕ σ_1
p_0 : σ_1
⊢ (∃ stop_state_list,
      { start_state := Sum.inr (Sum.inr p_0), stop_state_list := stop_state_list } ∈
          List.map
                (fun arrow =>
                  { start_state := Sum.inr arrow.start_state,
                    stop_state_list := List.map Sum.inr arrow.stop_state_list })
                (List.map
                  (fun arrow =>
                    { start_state := Sum.inl arrow.start_state,
                      stop_state_list := List.map Sum.inl arrow.stop_state_list })
                  M_0.epsilon_arrow_list) ++
              List.map
                (fun arrow =>
                  { start_state := Sum.inr arrow.start_state,
                    stop_state_list := List.map Sum.inr arrow.stop_state_list })
                (List.map
                  (fun arrow =>
                    { start_state := Sum.inr arrow.start_state,
                      stop_state_list := List.map Sum.inr arrow.stop_state_list })
                  M_1.epsilon_arrow_list) ++
            List.map
              (fun accepting_state =>
                { start_state := accepting_state,
                  stop_state_list := List.map Sum.inr (List.map Sum.inr M_1.starting_state_list) })
              (List.map Sum.inr (List.map Sum.inl M_0.accepting_state_list)) ∧
        q ∈ stop_state_list) =
    match (Sum.inr (Sum.inr p_0), q) with
    | (Sum.inr (Sum.inl p'), Sum.inr (Sum.inl q')) =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_0.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | (Sum.inr (Sum.inr p'), Sum.inr (Sum.inr q')) =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | (Sum.inr (Sum.inl p'), Sum.inr (Sum.inr q')) => p' ∈ M_0.accepting_state_list ∧ q' ∈ M_1.starting_state_list
    | x => False
Tactic:
cases q
State after:
case inl
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_1
val✝ : ℕ
⊢ (∃ stop_state_list,
      { start_state := Sum.inr (Sum.inr p_0), stop_state_list := stop_state_list } ∈
          List.map
                (fun arrow =>
                  { start_state := Sum.inr arrow.start_state,
                    stop_state_list := List.map Sum.inr arrow.stop_state_list })
                (List.map
                  (fun arrow =>
                    { start_state := Sum.inl arrow.start_state,
                      stop_state_list := List.map Sum.inl arrow.stop_state_list })
                  M_0.epsilon_arrow_list) ++
              List.map
                (fun arrow =>
                  { start_state := Sum.inr arrow.start_state,
                    stop_state_list := List.map Sum.inr arrow.stop_state_list })
                (List.map
                  (fun arrow =>
                    { start_state := Sum.inr arrow.start_state,
                      stop_state_list := List.map Sum.inr arrow.stop_state_list })
                  M_1.epsilon_arrow_list) ++
            List.map
              (fun accepting_state =>
                { start_state := accepting_state,
                  stop_state_list := List.map Sum.inr (List.map Sum.inr M_1.starting_state_list) })
              (List.map Sum.inr (List.map Sum.inl M_0.accepting_state_list)) ∧
        Sum.inl val✝ ∈ stop_state_list) =
    match (Sum.inr (Sum.inr p_0), Sum.inl val✝) with
    | (Sum.inr (Sum.inl p'), Sum.inr (Sum.inl q')) =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_0.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | (Sum.inr (Sum.inr p'), Sum.inr (Sum.inr q')) =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | (Sum.inr (Sum.inl p'), Sum.inr (Sum.inr q')) => p' ∈ M_0.accepting_state_list ∧ q' ∈ M_1.starting_state_list
    | x => False

case inr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_1
val✝ : σ_0 ⊕ σ_1
⊢ (∃ stop_state_list,
      { start_state := Sum.inr (Sum.inr p_0), stop_state_list := stop_state_list } ∈
          List.map
                (fun arrow =>
                  { start_state := Sum.inr arrow.start_state,
                    stop_state_list := List.map Sum.inr arrow.stop_state_list })
                (List.map
                  (fun arrow =>
                    { start_state := Sum.inl arrow.start_state,
                      stop_state_list := List.map Sum.inl arrow.stop_state_list })
                  M_0.epsilon_arrow_list) ++
              List.map
                (fun arrow =>
                  { start_state := Sum.inr arrow.start_state,
                    stop_state_list := List.map Sum.inr arrow.stop_state_list })
                (List.map
                  (fun arrow =>
                    { start_state := Sum.inr arrow.start_state,
                      stop_state_list := List.map Sum.inr arrow.stop_state_list })
                  M_1.epsilon_arrow_list) ++
            List.map
              (fun accepting_state =>
                { start_state := accepting_state,
                  stop_state_list := List.map Sum.inr (List.map Sum.inr M_1.starting_state_list) })
              (List.map Sum.inr (List.map Sum.inl M_0.accepting_state_list)) ∧
        Sum.inr val✝ ∈ stop_state_list) =
    match (Sum.inr (Sum.inr p_0), Sum.inr val✝) with
    | (Sum.inr (Sum.inl p'), Sum.inr (Sum.inl q')) =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_0.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | (Sum.inr (Sum.inr p'), Sum.inr (Sum.inr q')) =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | (Sum.inr (Sum.inl p'), Sum.inr (Sum.inr q')) => p' ∈ M_0.accepting_state_list ∧ q' ∈ M_1.starting_state_list
    | x => False

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_1
q_0 : ℕ
⊢ (∃ stop_state_list,
      { start_state := Sum.inr (Sum.inr p_0), stop_state_list := stop_state_list } ∈
          List.map
                (fun arrow =>
                  { start_state := Sum.inr arrow.start_state,
                    stop_state_list := List.map Sum.inr arrow.stop_state_list })
                (List.map
                  (fun arrow =>
                    { start_state := Sum.inl arrow.start_state,
                      stop_state_list := List.map Sum.inl arrow.stop_state_list })
                  M_0.epsilon_arrow_list) ++
              List.map
                (fun arrow =>
                  { start_state := Sum.inr arrow.start_state,
                    stop_state_list := List.map Sum.inr arrow.stop_state_list })
                (List.map
                  (fun arrow =>
                    { start_state := Sum.inr arrow.start_state,
                      stop_state_list := List.map Sum.inr arrow.stop_state_list })
                  M_1.epsilon_arrow_list) ++
            List.map
              (fun accepting_state =>
                { start_state := accepting_state,
                  stop_state_list := List.map Sum.inr (List.map Sum.inr M_1.starting_state_list) })
              (List.map Sum.inr (List.map Sum.inl M_0.accepting_state_list)) ∧
        Sum.inl q_0 ∈ stop_state_list) =
    match (Sum.inr (Sum.inr p_0), Sum.inl q_0) with
    | (Sum.inr (Sum.inl p'), Sum.inr (Sum.inl q')) =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_0.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | (Sum.inr (Sum.inr p'), Sum.inr (Sum.inr q')) =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | (Sum.inr (Sum.inl p'), Sum.inr (Sum.inr q')) => p' ∈ M_0.accepting_state_list ∧ q' ∈ M_1.starting_state_list
    | x => False
Tactic:
case _ q_0 =>
  simp
  intro xs x a1 a2 a3
  simp only [← a3]
  simp
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_1
q_0 : σ_0 ⊕ σ_1
⊢ (∃ stop_state_list,
      { start_state := Sum.inr (Sum.inr p_0), stop_state_list := stop_state_list } ∈
          List.map
                (fun arrow =>
                  { start_state := Sum.inr arrow.start_state,
                    stop_state_list := List.map Sum.inr arrow.stop_state_list })
                (List.map
                  (fun arrow =>
                    { start_state := Sum.inl arrow.start_state,
                      stop_state_list := List.map Sum.inl arrow.stop_state_list })
                  M_0.epsilon_arrow_list) ++
              List.map
                (fun arrow =>
                  { start_state := Sum.inr arrow.start_state,
                    stop_state_list := List.map Sum.inr arrow.stop_state_list })
                (List.map
                  (fun arrow =>
                    { start_state := Sum.inr arrow.start_state,
                      stop_state_list := List.map Sum.inr arrow.stop_state_list })
                  M_1.epsilon_arrow_list) ++
            List.map
              (fun accepting_state =>
                { start_state := accepting_state,
                  stop_state_list := List.map Sum.inr (List.map Sum.inr M_1.starting_state_list) })
              (List.map Sum.inr (List.map Sum.inl M_0.accepting_state_list)) ∧
        Sum.inr q_0 ∈ stop_state_list) =
    match (Sum.inr (Sum.inr p_0), Sum.inr q_0) with
    | (Sum.inr (Sum.inl p'), Sum.inr (Sum.inl q')) =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_0.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | (Sum.inr (Sum.inr p'), Sum.inr (Sum.inr q')) =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | (Sum.inr (Sum.inl p'), Sum.inr (Sum.inr q')) => p' ∈ M_0.accepting_state_list ∧ q' ∈ M_1.starting_state_list
    | x => False
Tactic:
case _ q_0 =>
  cases q_0
  case _ q_0 =>
    simp
    intro xs x a1 a2 a3
    simp only [← a3]
    simp
  case _ q_0 =>
    simp
    sorry
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_1
q_0 : ℕ
⊢ (∃ stop_state_list,
      { start_state := Sum.inr (Sum.inr p_0), stop_state_list := stop_state_list } ∈
          List.map
                (fun arrow =>
                  { start_state := Sum.inr arrow.start_state,
                    stop_state_list := List.map Sum.inr arrow.stop_state_list })
                (List.map
                  (fun arrow =>
                    { start_state := Sum.inl arrow.start_state,
                      stop_state_list := List.map Sum.inl arrow.stop_state_list })
                  M_0.epsilon_arrow_list) ++
              List.map
                (fun arrow =>
                  { start_state := Sum.inr arrow.start_state,
                    stop_state_list := List.map Sum.inr arrow.stop_state_list })
                (List.map
                  (fun arrow =>
                    { start_state := Sum.inr arrow.start_state,
                      stop_state_list := List.map Sum.inr arrow.stop_state_list })
                  M_1.epsilon_arrow_list) ++
            List.map
              (fun accepting_state =>
                { start_state := accepting_state,
                  stop_state_list := List.map Sum.inr (List.map Sum.inr M_1.starting_state_list) })
              (List.map Sum.inr (List.map Sum.inl M_0.accepting_state_list)) ∧
        Sum.inl q_0 ∈ stop_state_list) =
    match (Sum.inr (Sum.inr p_0), Sum.inl q_0) with
    | (Sum.inr (Sum.inl p'), Sum.inr (Sum.inl q')) =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_0.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | (Sum.inr (Sum.inr p'), Sum.inr (Sum.inr q')) =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | (Sum.inr (Sum.inl p'), Sum.inr (Sum.inr q')) => p' ∈ M_0.accepting_state_list ∧ q' ∈ M_1.starting_state_list
    | x => False
Tactic:
simp
State after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_1
q_0 : ℕ
⊢ ∀ (x : List (ℕ ⊕ σ_0 ⊕ σ_1)),
    ∀ x_1 ∈ M_1.epsilon_arrow_list,
      x_1.start_state = p_0 → List.map (Sum.inr ∘ Sum.inr) x_1.stop_state_list = x → Sum.inl q_0 ∉ x

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_1
q_0 : ℕ
⊢ ∀ (x : List (ℕ ⊕ σ_0 ⊕ σ_1)),
    ∀ x_1 ∈ M_1.epsilon_arrow_list,
      x_1.start_state = p_0 → List.map (Sum.inr ∘ Sum.inr) x_1.stop_state_list = x → Sum.inl q_0 ∉ x
Tactic:
intro xs x a1 a2 a3
State after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_1
q_0 : ℕ
xs : List (ℕ ⊕ σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a1 : x ∈ M_1.epsilon_arrow_list
a2 : x.start_state = p_0
a3 : List.map (Sum.inr ∘ Sum.inr) x.stop_state_list = xs
⊢ Sum.inl q_0 ∉ xs

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_1
q_0 : ℕ
xs : List (ℕ ⊕ σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a1 : x ∈ M_1.epsilon_arrow_list
a2 : x.start_state = p_0
a3 : List.map (Sum.inr ∘ Sum.inr) x.stop_state_list = xs
⊢ Sum.inl q_0 ∉ xs
Tactic:
simp only [← a3]
State after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_1
q_0 : ℕ
xs : List (ℕ ⊕ σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a1 : x ∈ M_1.epsilon_arrow_list
a2 : x.start_state = p_0
a3 : List.map (Sum.inr ∘ Sum.inr) x.stop_state_list = xs
⊢ Sum.inl q_0 ∉ List.map (Sum.inr ∘ Sum.inr) x.stop_state_list

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_1
q_0 : ℕ
xs : List (ℕ ⊕ σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a1 : x ∈ M_1.epsilon_arrow_list
a2 : x.start_state = p_0
a3 : List.map (Sum.inr ∘ Sum.inr) x.stop_state_list = xs
⊢ Sum.inl q_0 ∉ List.map (Sum.inr ∘ Sum.inr) x.stop_state_list
Tactic:
simp
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_1
q_0 : σ_0 ⊕ σ_1
⊢ (∃ stop_state_list,
      { start_state := Sum.inr (Sum.inr p_0), stop_state_list := stop_state_list } ∈
          List.map
                (fun arrow =>
                  { start_state := Sum.inr arrow.start_state,
                    stop_state_list := List.map Sum.inr arrow.stop_state_list })
                (List.map
                  (fun arrow =>
                    { start_state := Sum.inl arrow.start_state,
                      stop_state_list := List.map Sum.inl arrow.stop_state_list })
                  M_0.epsilon_arrow_list) ++
              List.map
                (fun arrow =>
                  { start_state := Sum.inr arrow.start_state,
                    stop_state_list := List.map Sum.inr arrow.stop_state_list })
                (List.map
                  (fun arrow =>
                    { start_state := Sum.inr arrow.start_state,
                      stop_state_list := List.map Sum.inr arrow.stop_state_list })
                  M_1.epsilon_arrow_list) ++
            List.map
              (fun accepting_state =>
                { start_state := accepting_state,
                  stop_state_list := List.map Sum.inr (List.map Sum.inr M_1.starting_state_list) })
              (List.map Sum.inr (List.map Sum.inl M_0.accepting_state_list)) ∧
        Sum.inr q_0 ∈ stop_state_list) =
    match (Sum.inr (Sum.inr p_0), Sum.inr q_0) with
    | (Sum.inr (Sum.inl p'), Sum.inr (Sum.inl q')) =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_0.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | (Sum.inr (Sum.inr p'), Sum.inr (Sum.inr q')) =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | (Sum.inr (Sum.inl p'), Sum.inr (Sum.inr q')) => p' ∈ M_0.accepting_state_list ∧ q' ∈ M_1.starting_state_list
    | x => False
Tactic:
cases q_0
State after:
case inl
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_1
val✝ : σ_0
⊢ (∃ stop_state_list,
      { start_state := Sum.inr (Sum.inr p_0), stop_state_list := stop_state_list } ∈
          List.map
                (fun arrow =>
                  { start_state := Sum.inr arrow.start_state,
                    stop_state_list := List.map Sum.inr arrow.stop_state_list })
                (List.map
                  (fun arrow =>
                    { start_state := Sum.inl arrow.start_state,
                      stop_state_list := List.map Sum.inl arrow.stop_state_list })
                  M_0.epsilon_arrow_list) ++
              List.map
                (fun arrow =>
                  { start_state := Sum.inr arrow.start_state,
                    stop_state_list := List.map Sum.inr arrow.stop_state_list })
                (List.map
                  (fun arrow =>
                    { start_state := Sum.inr arrow.start_state,
                      stop_state_list := List.map Sum.inr arrow.stop_state_list })
                  M_1.epsilon_arrow_list) ++
            List.map
              (fun accepting_state =>
                { start_state := accepting_state,
                  stop_state_list := List.map Sum.inr (List.map Sum.inr M_1.starting_state_list) })
              (List.map Sum.inr (List.map Sum.inl M_0.accepting_state_list)) ∧
        Sum.inr (Sum.inl val✝) ∈ stop_state_list) =
    match (Sum.inr (Sum.inr p_0), Sum.inr (Sum.inl val✝)) with
    | (Sum.inr (Sum.inl p'), Sum.inr (Sum.inl q')) =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_0.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | (Sum.inr (Sum.inr p'), Sum.inr (Sum.inr q')) =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | (Sum.inr (Sum.inl p'), Sum.inr (Sum.inr q')) => p' ∈ M_0.accepting_state_list ∧ q' ∈ M_1.starting_state_list
    | x => False

case inr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 val✝ : σ_1
⊢ (∃ stop_state_list,
      { start_state := Sum.inr (Sum.inr p_0), stop_state_list := stop_state_list } ∈
          List.map
                (fun arrow =>
                  { start_state := Sum.inr arrow.start_state,
                    stop_state_list := List.map Sum.inr arrow.stop_state_list })
                (List.map
                  (fun arrow =>
                    { start_state := Sum.inl arrow.start_state,
                      stop_state_list := List.map Sum.inl arrow.stop_state_list })
                  M_0.epsilon_arrow_list) ++
              List.map
                (fun arrow =>
                  { start_state := Sum.inr arrow.start_state,
                    stop_state_list := List.map Sum.inr arrow.stop_state_list })
                (List.map
                  (fun arrow =>
                    { start_state := Sum.inr arrow.start_state,
                      stop_state_list := List.map Sum.inr arrow.stop_state_list })
                  M_1.epsilon_arrow_list) ++
            List.map
              (fun accepting_state =>
                { start_state := accepting_state,
                  stop_state_list := List.map Sum.inr (List.map Sum.inr M_1.starting_state_list) })
              (List.map Sum.inr (List.map Sum.inl M_0.accepting_state_list)) ∧
        Sum.inr (Sum.inr val✝) ∈ stop_state_list) =
    match (Sum.inr (Sum.inr p_0), Sum.inr (Sum.inr val✝)) with
    | (Sum.inr (Sum.inl p'), Sum.inr (Sum.inl q')) =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_0.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | (Sum.inr (Sum.inr p'), Sum.inr (Sum.inr q')) =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | (Sum.inr (Sum.inl p'), Sum.inr (Sum.inr q')) => p' ∈ M_0.accepting_state_list ∧ q' ∈ M_1.starting_state_list
    | x => False

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_1
q_0 : σ_0
⊢ (∃ stop_state_list,
      { start_state := Sum.inr (Sum.inr p_0), stop_state_list := stop_state_list } ∈
          List.map
                (fun arrow =>
                  { start_state := Sum.inr arrow.start_state,
                    stop_state_list := List.map Sum.inr arrow.stop_state_list })
                (List.map
                  (fun arrow =>
                    { start_state := Sum.inl arrow.start_state,
                      stop_state_list := List.map Sum.inl arrow.stop_state_list })
                  M_0.epsilon_arrow_list) ++
              List.map
                (fun arrow =>
                  { start_state := Sum.inr arrow.start_state,
                    stop_state_list := List.map Sum.inr arrow.stop_state_list })
                (List.map
                  (fun arrow =>
                    { start_state := Sum.inr arrow.start_state,
                      stop_state_list := List.map Sum.inr arrow.stop_state_list })
                  M_1.epsilon_arrow_list) ++
            List.map
              (fun accepting_state =>
                { start_state := accepting_state,
                  stop_state_list := List.map Sum.inr (List.map Sum.inr M_1.starting_state_list) })
              (List.map Sum.inr (List.map Sum.inl M_0.accepting_state_list)) ∧
        Sum.inr (Sum.inl q_0) ∈ stop_state_list) =
    match (Sum.inr (Sum.inr p_0), Sum.inr (Sum.inl q_0)) with
    | (Sum.inr (Sum.inl p'), Sum.inr (Sum.inl q')) =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_0.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | (Sum.inr (Sum.inr p'), Sum.inr (Sum.inr q')) =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | (Sum.inr (Sum.inl p'), Sum.inr (Sum.inr q')) => p' ∈ M_0.accepting_state_list ∧ q' ∈ M_1.starting_state_list
    | x => False
Tactic:
case _ q_0 =>
  simp
  intro xs x a1 a2 a3
  simp only [← a3]
  simp
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
⊢ (∃ stop_state_list,
      { start_state := Sum.inr (Sum.inr p_0), stop_state_list := stop_state_list } ∈
          List.map
                (fun arrow =>
                  { start_state := Sum.inr arrow.start_state,
                    stop_state_list := List.map Sum.inr arrow.stop_state_list })
                (List.map
                  (fun arrow =>
                    { start_state := Sum.inl arrow.start_state,
                      stop_state_list := List.map Sum.inl arrow.stop_state_list })
                  M_0.epsilon_arrow_list) ++
              List.map
                (fun arrow =>
                  { start_state := Sum.inr arrow.start_state,
                    stop_state_list := List.map Sum.inr arrow.stop_state_list })
                (List.map
                  (fun arrow =>
                    { start_state := Sum.inr arrow.start_state,
                      stop_state_list := List.map Sum.inr arrow.stop_state_list })
                  M_1.epsilon_arrow_list) ++
            List.map
              (fun accepting_state =>
                { start_state := accepting_state,
                  stop_state_list := List.map Sum.inr (List.map Sum.inr M_1.starting_state_list) })
              (List.map Sum.inr (List.map Sum.inl M_0.accepting_state_list)) ∧
        Sum.inr (Sum.inr q_0) ∈ stop_state_list) =
    match (Sum.inr (Sum.inr p_0), Sum.inr (Sum.inr q_0)) with
    | (Sum.inr (Sum.inl p'), Sum.inr (Sum.inl q')) =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_0.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | (Sum.inr (Sum.inr p'), Sum.inr (Sum.inr q')) =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | (Sum.inr (Sum.inl p'), Sum.inr (Sum.inr q')) => p' ∈ M_0.accepting_state_list ∧ q' ∈ M_1.starting_state_list
    | x => False
Tactic:
case _ q_0 =>
  simp
  sorry
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_1
q_0 : σ_0
⊢ (∃ stop_state_list,
      { start_state := Sum.inr (Sum.inr p_0), stop_state_list := stop_state_list } ∈
          List.map
                (fun arrow =>
                  { start_state := Sum.inr arrow.start_state,
                    stop_state_list := List.map Sum.inr arrow.stop_state_list })
                (List.map
                  (fun arrow =>
                    { start_state := Sum.inl arrow.start_state,
                      stop_state_list := List.map Sum.inl arrow.stop_state_list })
                  M_0.epsilon_arrow_list) ++
              List.map
                (fun arrow =>
                  { start_state := Sum.inr arrow.start_state,
                    stop_state_list := List.map Sum.inr arrow.stop_state_list })
                (List.map
                  (fun arrow =>
                    { start_state := Sum.inr arrow.start_state,
                      stop_state_list := List.map Sum.inr arrow.stop_state_list })
                  M_1.epsilon_arrow_list) ++
            List.map
              (fun accepting_state =>
                { start_state := accepting_state,
                  stop_state_list := List.map Sum.inr (List.map Sum.inr M_1.starting_state_list) })
              (List.map Sum.inr (List.map Sum.inl M_0.accepting_state_list)) ∧
        Sum.inr (Sum.inl q_0) ∈ stop_state_list) =
    match (Sum.inr (Sum.inr p_0), Sum.inr (Sum.inl q_0)) with
    | (Sum.inr (Sum.inl p'), Sum.inr (Sum.inl q')) =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_0.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | (Sum.inr (Sum.inr p'), Sum.inr (Sum.inr q')) =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | (Sum.inr (Sum.inl p'), Sum.inr (Sum.inr q')) => p' ∈ M_0.accepting_state_list ∧ q' ∈ M_1.starting_state_list
    | x => False
Tactic:
simp
State after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_1
q_0 : σ_0
⊢ ∀ (x : List (ℕ ⊕ σ_0 ⊕ σ_1)),
    ∀ x_1 ∈ M_1.epsilon_arrow_list,
      x_1.start_state = p_0 → List.map (Sum.inr ∘ Sum.inr) x_1.stop_state_list = x → Sum.inr (Sum.inl q_0) ∉ x

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_1
q_0 : σ_0
⊢ ∀ (x : List (ℕ ⊕ σ_0 ⊕ σ_1)),
    ∀ x_1 ∈ M_1.epsilon_arrow_list,
      x_1.start_state = p_0 → List.map (Sum.inr ∘ Sum.inr) x_1.stop_state_list = x → Sum.inr (Sum.inl q_0) ∉ x
Tactic:
intro xs x a1 a2 a3
State after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_1
q_0 : σ_0
xs : List (ℕ ⊕ σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a1 : x ∈ M_1.epsilon_arrow_list
a2 : x.start_state = p_0
a3 : List.map (Sum.inr ∘ Sum.inr) x.stop_state_list = xs
⊢ Sum.inr (Sum.inl q_0) ∉ xs

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_1
q_0 : σ_0
xs : List (ℕ ⊕ σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a1 : x ∈ M_1.epsilon_arrow_list
a2 : x.start_state = p_0
a3 : List.map (Sum.inr ∘ Sum.inr) x.stop_state_list = xs
⊢ Sum.inr (Sum.inl q_0) ∉ xs
Tactic:
simp only [← a3]
State after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_1
q_0 : σ_0
xs : List (ℕ ⊕ σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a1 : x ∈ M_1.epsilon_arrow_list
a2 : x.start_state = p_0
a3 : List.map (Sum.inr ∘ Sum.inr) x.stop_state_list = xs
⊢ Sum.inr (Sum.inl q_0) ∉ List.map (Sum.inr ∘ Sum.inr) x.stop_state_list

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_1
q_0 : σ_0
xs : List (ℕ ⊕ σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a1 : x ∈ M_1.epsilon_arrow_list
a2 : x.start_state = p_0
a3 : List.map (Sum.inr ∘ Sum.inr) x.stop_state_list = xs
⊢ Sum.inr (Sum.inl q_0) ∉ List.map (Sum.inr ∘ Sum.inr) x.stop_state_list
Tactic:
simp
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
⊢ (∃ stop_state_list,
      { start_state := Sum.inr (Sum.inr p_0), stop_state_list := stop_state_list } ∈
          List.map
                (fun arrow =>
                  { start_state := Sum.inr arrow.start_state,
                    stop_state_list := List.map Sum.inr arrow.stop_state_list })
                (List.map
                  (fun arrow =>
                    { start_state := Sum.inl arrow.start_state,
                      stop_state_list := List.map Sum.inl arrow.stop_state_list })
                  M_0.epsilon_arrow_list) ++
              List.map
                (fun arrow =>
                  { start_state := Sum.inr arrow.start_state,
                    stop_state_list := List.map Sum.inr arrow.stop_state_list })
                (List.map
                  (fun arrow =>
                    { start_state := Sum.inr arrow.start_state,
                      stop_state_list := List.map Sum.inr arrow.stop_state_list })
                  M_1.epsilon_arrow_list) ++
            List.map
              (fun accepting_state =>
                { start_state := accepting_state,
                  stop_state_list := List.map Sum.inr (List.map Sum.inr M_1.starting_state_list) })
              (List.map Sum.inr (List.map Sum.inl M_0.accepting_state_list)) ∧
        Sum.inr (Sum.inr q_0) ∈ stop_state_list) =
    match (Sum.inr (Sum.inr p_0), Sum.inr (Sum.inr q_0)) with
    | (Sum.inr (Sum.inl p'), Sum.inr (Sum.inl q')) =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_0.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | (Sum.inr (Sum.inr p'), Sum.inr (Sum.inr q')) =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | (Sum.inr (Sum.inl p'), Sum.inr (Sum.inr q')) => p' ∈ M_0.accepting_state_list ∧ q' ∈ M_1.starting_state_list
    | x => False
Tactic:
simp
State after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
⊢ (∃ stop_state_list,
      (∃ a ∈ M_1.epsilon_arrow_list,
          a.start_state = p_0 ∧ List.map (Sum.inr ∘ Sum.inr) a.stop_state_list = stop_state_list) ∧
        Sum.inr (Sum.inr q_0) ∈ stop_state_list) ↔
    ∃ stop_state_list,
      { start_state := p_0, stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q_0 ∈ stop_state_list

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
⊢ (∃ stop_state_list,
      (∃ a ∈ M_1.epsilon_arrow_list,
          a.start_state = p_0 ∧ List.map (Sum.inr ∘ Sum.inr) a.stop_state_list = stop_state_list) ∧
        Sum.inr (Sum.inr q_0) ∈ stop_state_list) ↔
    ∃ stop_state_list,
      { start_state := p_0, stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q_0 ∈ stop_state_list
Tactic:
sorry
State after:
no goals

State before:
case right.right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
⊢ ((fun state => state ∈ List.map Sum.inr (List.map Sum.inl M_0.starting_state_list)) = fun p =>
      match p with
      | Sum.inr (Sum.inl p') => p' ∈ M_0.starting_state_list
      | x => False) ∧
    (fun state => state ∈ List.map Sum.inr (List.map Sum.inr M_1.accepting_state_list)) = fun p =>
      match p with
      | Sum.inr (Sum.inr p') => p' ∈ M_1.accepting_state_list
      | x => False
Tactic:
constructor
State after:
case right.right.left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
⊢ (fun state => state ∈ List.map Sum.inr (List.map Sum.inl M_0.starting_state_list)) = fun p =>
    match p with
    | Sum.inr (Sum.inl p') => p' ∈ M_0.starting_state_list
    | x => False

case right.right.right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
⊢ (fun state => state ∈ List.map Sum.inr (List.map Sum.inr M_1.accepting_state_list)) = fun p =>
    match p with
    | Sum.inr (Sum.inr p') => p' ∈ M_1.accepting_state_list
    | x => False

State before:
case right.right.left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
⊢ (fun state => state ∈ List.map Sum.inr (List.map Sum.inl M_0.starting_state_list)) = fun p =>
    match p with
    | Sum.inr (Sum.inl p') => p' ∈ M_0.starting_state_list
    | x => False
Tactic:
funext p
State after:
case right.right.left.h
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p : ℕ ⊕ σ_0 ⊕ σ_1
⊢ (p ∈ List.map Sum.inr (List.map Sum.inl M_0.starting_state_list)) =
    match p with
    | Sum.inr (Sum.inl p') => p' ∈ M_0.starting_state_list
    | x => False

State before:
case right.right.left.h
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p : ℕ ⊕ σ_0 ⊕ σ_1
⊢ (p ∈ List.map Sum.inr (List.map Sum.inl M_0.starting_state_list)) =
    match p with
    | Sum.inr (Sum.inl p') => p' ∈ M_0.starting_state_list
    | x => False
Tactic:
cases p
State after:
case right.right.left.h.inl
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
val✝ : ℕ
⊢ (Sum.inl val✝ ∈ List.map Sum.inr (List.map Sum.inl M_0.starting_state_list)) =
    match Sum.inl val✝ with
    | Sum.inr (Sum.inl p') => p' ∈ M_0.starting_state_list
    | x => False

case right.right.left.h.inr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
val✝ : σ_0 ⊕ σ_1
⊢ (Sum.inr val✝ ∈ List.map Sum.inr (List.map Sum.inl M_0.starting_state_list)) =
    match Sum.inr val✝ with
    | Sum.inr (Sum.inl p') => p' ∈ M_0.starting_state_list
    | x => False

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : ℕ
⊢ (Sum.inl p_0 ∈ List.map Sum.inr (List.map Sum.inl M_0.starting_state_list)) =
    match Sum.inl p_0 with
    | Sum.inr (Sum.inl p') => p' ∈ M_0.starting_state_list
    | x => False
Tactic:
case _ p_0 =>
  simp
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0 ⊕ σ_1
⊢ (Sum.inr p_0 ∈ List.map Sum.inr (List.map Sum.inl M_0.starting_state_list)) =
    match Sum.inr p_0 with
    | Sum.inr (Sum.inl p') => p' ∈ M_0.starting_state_list
    | x => False
Tactic:
case _ p_0 =>
  cases p_0
  case _ p_0 =>
    simp
  case _ p_0 =>
    simp
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : ℕ
⊢ (Sum.inl p_0 ∈ List.map Sum.inr (List.map Sum.inl M_0.starting_state_list)) =
    match Sum.inl p_0 with
    | Sum.inr (Sum.inl p') => p' ∈ M_0.starting_state_list
    | x => False
Tactic:
simp
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0 ⊕ σ_1
⊢ (Sum.inr p_0 ∈ List.map Sum.inr (List.map Sum.inl M_0.starting_state_list)) =
    match Sum.inr p_0 with
    | Sum.inr (Sum.inl p') => p' ∈ M_0.starting_state_list
    | x => False
Tactic:
cases p_0
State after:
case inl
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
val✝ : σ_0
⊢ (Sum.inr (Sum.inl val✝) ∈ List.map Sum.inr (List.map Sum.inl M_0.starting_state_list)) =
    match Sum.inr (Sum.inl val✝) with
    | Sum.inr (Sum.inl p') => p' ∈ M_0.starting_state_list
    | x => False

case inr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
val✝ : σ_1
⊢ (Sum.inr (Sum.inr val✝) ∈ List.map Sum.inr (List.map Sum.inl M_0.starting_state_list)) =
    match Sum.inr (Sum.inr val✝) with
    | Sum.inr (Sum.inl p') => p' ∈ M_0.starting_state_list
    | x => False

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0
⊢ (Sum.inr (Sum.inl p_0) ∈ List.map Sum.inr (List.map Sum.inl M_0.starting_state_list)) =
    match Sum.inr (Sum.inl p_0) with
    | Sum.inr (Sum.inl p') => p' ∈ M_0.starting_state_list
    | x => False
Tactic:
case _ p_0 =>
  simp
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_1
⊢ (Sum.inr (Sum.inr p_0) ∈ List.map Sum.inr (List.map Sum.inl M_0.starting_state_list)) =
    match Sum.inr (Sum.inr p_0) with
    | Sum.inr (Sum.inl p') => p' ∈ M_0.starting_state_list
    | x => False
Tactic:
case _ p_0 =>
  simp
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0
⊢ (Sum.inr (Sum.inl p_0) ∈ List.map Sum.inr (List.map Sum.inl M_0.starting_state_list)) =
    match Sum.inr (Sum.inl p_0) with
    | Sum.inr (Sum.inl p') => p' ∈ M_0.starting_state_list
    | x => False
Tactic:
simp
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_1
⊢ (Sum.inr (Sum.inr p_0) ∈ List.map Sum.inr (List.map Sum.inl M_0.starting_state_list)) =
    match Sum.inr (Sum.inr p_0) with
    | Sum.inr (Sum.inl p') => p' ∈ M_0.starting_state_list
    | x => False
Tactic:
simp
State after:
no goals

State before:
case right.right.right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
⊢ (fun state => state ∈ List.map Sum.inr (List.map Sum.inr M_1.accepting_state_list)) = fun p =>
    match p with
    | Sum.inr (Sum.inr p') => p' ∈ M_1.accepting_state_list
    | x => False
Tactic:
funext p
State after:
case right.right.right.h
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p : ℕ ⊕ σ_0 ⊕ σ_1
⊢ (p ∈ List.map Sum.inr (List.map Sum.inr M_1.accepting_state_list)) =
    match p with
    | Sum.inr (Sum.inr p') => p' ∈ M_1.accepting_state_list
    | x => False

State before:
case right.right.right.h
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p : ℕ ⊕ σ_0 ⊕ σ_1
⊢ (p ∈ List.map Sum.inr (List.map Sum.inr M_1.accepting_state_list)) =
    match p with
    | Sum.inr (Sum.inr p') => p' ∈ M_1.accepting_state_list
    | x => False
Tactic:
cases p
State after:
case right.right.right.h.inl
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
val✝ : ℕ
⊢ (Sum.inl val✝ ∈ List.map Sum.inr (List.map Sum.inr M_1.accepting_state_list)) =
    match Sum.inl val✝ with
    | Sum.inr (Sum.inr p') => p' ∈ M_1.accepting_state_list
    | x => False

case right.right.right.h.inr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
val✝ : σ_0 ⊕ σ_1
⊢ (Sum.inr val✝ ∈ List.map Sum.inr (List.map Sum.inr M_1.accepting_state_list)) =
    match Sum.inr val✝ with
    | Sum.inr (Sum.inr p') => p' ∈ M_1.accepting_state_list
    | x => False

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : ℕ
⊢ (Sum.inl p_0 ∈ List.map Sum.inr (List.map Sum.inr M_1.accepting_state_list)) =
    match Sum.inl p_0 with
    | Sum.inr (Sum.inr p') => p' ∈ M_1.accepting_state_list
    | x => False
Tactic:
case _ p_0 =>
  simp
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0 ⊕ σ_1
⊢ (Sum.inr p_0 ∈ List.map Sum.inr (List.map Sum.inr M_1.accepting_state_list)) =
    match Sum.inr p_0 with
    | Sum.inr (Sum.inr p') => p' ∈ M_1.accepting_state_list
    | x => False
Tactic:
case _ p_0 =>
  cases p_0
  case _ p_0 =>
    simp
  case _ p_0 =>
    simp
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : ℕ
⊢ (Sum.inl p_0 ∈ List.map Sum.inr (List.map Sum.inr M_1.accepting_state_list)) =
    match Sum.inl p_0 with
    | Sum.inr (Sum.inr p') => p' ∈ M_1.accepting_state_list
    | x => False
Tactic:
simp
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0 ⊕ σ_1
⊢ (Sum.inr p_0 ∈ List.map Sum.inr (List.map Sum.inr M_1.accepting_state_list)) =
    match Sum.inr p_0 with
    | Sum.inr (Sum.inr p') => p' ∈ M_1.accepting_state_list
    | x => False
Tactic:
cases p_0
State after:
case inl
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
val✝ : σ_0
⊢ (Sum.inr (Sum.inl val✝) ∈ List.map Sum.inr (List.map Sum.inr M_1.accepting_state_list)) =
    match Sum.inr (Sum.inl val✝) with
    | Sum.inr (Sum.inr p') => p' ∈ M_1.accepting_state_list
    | x => False

case inr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
val✝ : σ_1
⊢ (Sum.inr (Sum.inr val✝) ∈ List.map Sum.inr (List.map Sum.inr M_1.accepting_state_list)) =
    match Sum.inr (Sum.inr val✝) with
    | Sum.inr (Sum.inr p') => p' ∈ M_1.accepting_state_list
    | x => False

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0
⊢ (Sum.inr (Sum.inl p_0) ∈ List.map Sum.inr (List.map Sum.inr M_1.accepting_state_list)) =
    match Sum.inr (Sum.inl p_0) with
    | Sum.inr (Sum.inr p') => p' ∈ M_1.accepting_state_list
    | x => False
Tactic:
case _ p_0 =>
  simp
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_1
⊢ (Sum.inr (Sum.inr p_0) ∈ List.map Sum.inr (List.map Sum.inr M_1.accepting_state_list)) =
    match Sum.inr (Sum.inr p_0) with
    | Sum.inr (Sum.inr p') => p' ∈ M_1.accepting_state_list
    | x => False
Tactic:
case _ p_0 =>
  simp
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0
⊢ (Sum.inr (Sum.inl p_0) ∈ List.map Sum.inr (List.map Sum.inr M_1.accepting_state_list)) =
    match Sum.inr (Sum.inl p_0) with
    | Sum.inr (Sum.inr p') => p' ∈ M_1.accepting_state_list
    | x => False
Tactic:
simp
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_1
⊢ (Sum.inr (Sum.inr p_0) ∈ List.map Sum.inr (List.map Sum.inr M_1.accepting_state_list)) =
    match Sum.inr (Sum.inr p_0) with
    | Sum.inr (Sum.inr p') => p' ∈ M_1.accepting_state_list
    | x => False
Tactic:
simp
State after:
no goals