Theorem: match_union_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
⊢ {
        symbol_arrow_list :=
          (EpsilonNFA.wrapLeft σ_1 M_0).symbol_arrow_list ++ (EpsilonNFA.wrapRight σ_0 M_1).symbol_arrow_list,
        epsilon_arrow_list :=
          (EpsilonNFA.wrapLeft σ_1 M_0).epsilon_arrow_list ++ (EpsilonNFA.wrapRight σ_0 M_1).epsilon_arrow_list,
        starting_state_list :=
          (EpsilonNFA.wrapLeft σ_1 M_0).starting_state_list ++ (EpsilonNFA.wrapRight σ_0 M_1).starting_state_list,
        accepting_state_list :=
          (EpsilonNFA.wrapLeft σ_1 M_0).accepting_state_list ++
            (EpsilonNFA.wrapRight σ_0 M_1).accepting_state_list }.toAbstract =
    match_union_AbstractEpsilonNFA α σ_0 σ_1 M_0.toAbstract M_1.toAbstract
Tactic:
simp only [EpsilonNFA.toAbstract]
Proof state after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
⊢ {
      symbol := fun start_state symbol stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, symbol := symbol, stop_state_list := stop_state_list } ∈
              (EpsilonNFA.wrapLeft σ_1 M_0).symbol_arrow_list ++ (EpsilonNFA.wrapRight σ_0 M_1).symbol_arrow_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 } ∈
              (EpsilonNFA.wrapLeft σ_1 M_0).epsilon_arrow_list ++ (EpsilonNFA.wrapRight σ_0 M_1).epsilon_arrow_list ∧
            stop_state ∈ stop_state_list,
      start := fun state =>
        state ∈ (EpsilonNFA.wrapLeft σ_1 M_0).starting_state_list ++ (EpsilonNFA.wrapRight σ_0 M_1).starting_state_list,
      accepting := fun state =>
        state ∈
          (EpsilonNFA.wrapLeft σ_1 M_0).accepting_state_list ++ (EpsilonNFA.wrapRight σ_0 M_1).accepting_state_list } =
    match_union_AbstractEpsilonNFA α σ_0 σ_1
      {
        symbol := fun start_state symbol stop_state =>
          ∃ stop_state_list,
            { start_state := start_state, symbol := symbol, stop_state_list := stop_state_list } ∈
                M_0.symbol_arrow_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 } ∈ M_0.epsilon_arrow_list ∧
              stop_state ∈ stop_state_list,
        start := fun state => state ∈ M_0.starting_state_list,
        accepting := fun state => state ∈ M_0.accepting_state_list }
      {
        symbol := fun start_state symbol stop_state =>
          ∃ stop_state_list,
            { start_state := start_state, symbol := symbol, stop_state_list := stop_state_list } ∈
                M_1.symbol_arrow_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 } ∈ M_1.epsilon_arrow_list ∧
              stop_state ∈ stop_state_list,
        start := fun state => state ∈ M_1.starting_state_list,
        accepting := fun state => state ∈ M_1.accepting_state_list }