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

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
⊢ (match_union_EpsilonNFA α σ_0 σ_1 M_0 M_1).toAbstract =
    match_union_AbstractEpsilonNFA α σ_0 σ_1 M_0.toAbstract M_1.toAbstract
Tactic:
simp only [match_union_EpsilonNFA]
State after:
α : 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

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]
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 }

State before:
α : 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 }
Tactic:
simp only [match_union_AbstractEpsilonNFA]
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 } =
    {
      symbol := fun p c q =>
        match (p, q) with
        | (Sum.inl p', Sum.inl q') =>
          ∃ stop_state_list,
            { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
              q' ∈ stop_state_list
        | (Sum.inr p', Sum.inr q') =>
          ∃ stop_state_list,
            { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
              q' ∈ stop_state_list
        | x => False,
      epsilon := fun p q =>
        match (p, q) with
        | (Sum.inl p', 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 p', Sum.inr q') =>
          ∃ stop_state_list,
            { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
        | x => False,
      start := fun p =>
        match p with
        | Sum.inl p' => p' ∈ M_0.starting_state_list
        | Sum.inr p' => p' ∈ M_1.starting_state_list,
      accepting := fun p =>
        match p with
        | Sum.inl p' => p' ∈ M_0.accepting_state_list
        | Sum.inr p' => p' ∈ M_1.accepting_state_list }

State before:
α : 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 } =
    {
      symbol := fun p c q =>
        match (p, q) with
        | (Sum.inl p', Sum.inl q') =>
          ∃ stop_state_list,
            { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
              q' ∈ stop_state_list
        | (Sum.inr p', Sum.inr q') =>
          ∃ stop_state_list,
            { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
              q' ∈ stop_state_list
        | x => False,
      epsilon := fun p q =>
        match (p, q) with
        | (Sum.inl p', 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 p', Sum.inr q') =>
          ∃ stop_state_list,
            { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
        | x => False,
      start := fun p =>
        match p with
        | Sum.inl p' => p' ∈ M_0.starting_state_list
        | Sum.inr p' => p' ∈ M_1.starting_state_list,
      accepting := fun p =>
        match p with
        | Sum.inl p' => p' ∈ M_0.accepting_state_list
        | Sum.inr p' => p' ∈ M_1.accepting_state_list }
Tactic:
simp only [AbstractEpsilonNFA.mk.injEq]
State after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
⊢ ((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) =
      fun p c q =>
      match (p, q) with
      | (Sum.inl p', Sum.inl q') =>
        ∃ stop_state_list,
          { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
            q' ∈ stop_state_list
      | (Sum.inr p', Sum.inr q') =>
        ∃ stop_state_list,
          { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
            q' ∈ stop_state_list
      | x => False) ∧
    ((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) =
        fun p q =>
        match (p, q) with
        | (Sum.inl p', 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 p', Sum.inr q') =>
          ∃ stop_state_list,
            { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
        | x => False) ∧
      ((fun state =>
            state ∈
              (EpsilonNFA.wrapLeft σ_1 M_0).starting_state_list ++ (EpsilonNFA.wrapRight σ_0 M_1).starting_state_list) =
          fun p =>
          match p with
          | Sum.inl p' => p' ∈ M_0.starting_state_list
          | Sum.inr p' => p' ∈ M_1.starting_state_list) ∧
        (fun state =>
            state ∈
              (EpsilonNFA.wrapLeft σ_1 M_0).accepting_state_list ++
                (EpsilonNFA.wrapRight σ_0 M_1).accepting_state_list) =
          fun p =>
          match p with
          | Sum.inl p' => p' ∈ M_0.accepting_state_list
          | Sum.inr p' => p' ∈ M_1.accepting_state_list

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
⊢ ((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) =
      fun p c q =>
      match (p, q) with
      | (Sum.inl p', Sum.inl q') =>
        ∃ stop_state_list,
          { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
            q' ∈ stop_state_list
      | (Sum.inr p', Sum.inr q') =>
        ∃ stop_state_list,
          { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
            q' ∈ stop_state_list
      | x => False) ∧
    ((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) =
        fun p q =>
        match (p, q) with
        | (Sum.inl p', 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 p', Sum.inr q') =>
          ∃ stop_state_list,
            { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
        | x => False) ∧
      ((fun state =>
            state ∈
              (EpsilonNFA.wrapLeft σ_1 M_0).starting_state_list ++ (EpsilonNFA.wrapRight σ_0 M_1).starting_state_list) =
          fun p =>
          match p with
          | Sum.inl p' => p' ∈ M_0.starting_state_list
          | Sum.inr p' => p' ∈ M_1.starting_state_list) ∧
        (fun state =>
            state ∈
              (EpsilonNFA.wrapLeft σ_1 M_0).accepting_state_list ++
                (EpsilonNFA.wrapRight σ_0 M_1).accepting_state_list) =
          fun p =>
          match p with
          | Sum.inl p' => p' ∈ M_0.accepting_state_list
          | Sum.inr p' => p' ∈ M_1.accepting_state_list
Tactic:
simp only [EpsilonNFA.wrapLeft]
State after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
⊢ ((fun start_state symbol stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, symbol := symbol, stop_state_list := stop_state_list } ∈
              (EpsilonNFA.map Sum.inl M_0).symbol_arrow_list ++ (EpsilonNFA.wrapRight σ_0 M_1).symbol_arrow_list ∧
            stop_state ∈ stop_state_list) =
      fun p c q =>
      match (p, q) with
      | (Sum.inl p', Sum.inl q') =>
        ∃ stop_state_list,
          { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
            q' ∈ stop_state_list
      | (Sum.inr p', Sum.inr q') =>
        ∃ stop_state_list,
          { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
            q' ∈ stop_state_list
      | x => False) ∧
    ((fun start_state stop_state =>
          ∃ stop_state_list,
            { start_state := start_state, stop_state_list := stop_state_list } ∈
                (EpsilonNFA.map Sum.inl M_0).epsilon_arrow_list ++ (EpsilonNFA.wrapRight σ_0 M_1).epsilon_arrow_list ∧
              stop_state ∈ stop_state_list) =
        fun p q =>
        match (p, q) with
        | (Sum.inl p', 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 p', Sum.inr q') =>
          ∃ stop_state_list,
            { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
        | x => False) ∧
      ((fun state =>
            state ∈
              (EpsilonNFA.map Sum.inl M_0).starting_state_list ++ (EpsilonNFA.wrapRight σ_0 M_1).starting_state_list) =
          fun p =>
          match p with
          | Sum.inl p' => p' ∈ M_0.starting_state_list
          | Sum.inr p' => p' ∈ M_1.starting_state_list) ∧
        (fun state =>
            state ∈
              (EpsilonNFA.map Sum.inl M_0).accepting_state_list ++
                (EpsilonNFA.wrapRight σ_0 M_1).accepting_state_list) =
          fun p =>
          match p with
          | Sum.inl p' => p' ∈ M_0.accepting_state_list
          | Sum.inr p' => p' ∈ M_1.accepting_state_list

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
⊢ ((fun start_state symbol stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, symbol := symbol, stop_state_list := stop_state_list } ∈
              (EpsilonNFA.map Sum.inl M_0).symbol_arrow_list ++ (EpsilonNFA.wrapRight σ_0 M_1).symbol_arrow_list ∧
            stop_state ∈ stop_state_list) =
      fun p c q =>
      match (p, q) with
      | (Sum.inl p', Sum.inl q') =>
        ∃ stop_state_list,
          { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
            q' ∈ stop_state_list
      | (Sum.inr p', Sum.inr q') =>
        ∃ stop_state_list,
          { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
            q' ∈ stop_state_list
      | x => False) ∧
    ((fun start_state stop_state =>
          ∃ stop_state_list,
            { start_state := start_state, stop_state_list := stop_state_list } ∈
                (EpsilonNFA.map Sum.inl M_0).epsilon_arrow_list ++ (EpsilonNFA.wrapRight σ_0 M_1).epsilon_arrow_list ∧
              stop_state ∈ stop_state_list) =
        fun p q =>
        match (p, q) with
        | (Sum.inl p', 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 p', Sum.inr q') =>
          ∃ stop_state_list,
            { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
        | x => False) ∧
      ((fun state =>
            state ∈
              (EpsilonNFA.map Sum.inl M_0).starting_state_list ++ (EpsilonNFA.wrapRight σ_0 M_1).starting_state_list) =
          fun p =>
          match p with
          | Sum.inl p' => p' ∈ M_0.starting_state_list
          | Sum.inr p' => p' ∈ M_1.starting_state_list) ∧
        (fun state =>
            state ∈
              (EpsilonNFA.map Sum.inl M_0).accepting_state_list ++
                (EpsilonNFA.wrapRight σ_0 M_1).accepting_state_list) =
          fun p =>
          match p with
          | Sum.inl p' => p' ∈ M_0.accepting_state_list
          | Sum.inr p' => p' ∈ M_1.accepting_state_list
Tactic:
simp only [EpsilonNFA.wrapRight]
State after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
⊢ ((fun start_state symbol stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, symbol := symbol, stop_state_list := stop_state_list } ∈
              (EpsilonNFA.map Sum.inl M_0).symbol_arrow_list ++ (EpsilonNFA.map Sum.inr M_1).symbol_arrow_list ∧
            stop_state ∈ stop_state_list) =
      fun p c q =>
      match (p, q) with
      | (Sum.inl p', Sum.inl q') =>
        ∃ stop_state_list,
          { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
            q' ∈ stop_state_list
      | (Sum.inr p', Sum.inr q') =>
        ∃ stop_state_list,
          { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
            q' ∈ stop_state_list
      | x => False) ∧
    ((fun start_state stop_state =>
          ∃ stop_state_list,
            { start_state := start_state, stop_state_list := stop_state_list } ∈
                (EpsilonNFA.map Sum.inl M_0).epsilon_arrow_list ++ (EpsilonNFA.map Sum.inr M_1).epsilon_arrow_list ∧
              stop_state ∈ stop_state_list) =
        fun p q =>
        match (p, q) with
        | (Sum.inl p', 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 p', Sum.inr q') =>
          ∃ stop_state_list,
            { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
        | x => False) ∧
      ((fun state =>
            state ∈
              (EpsilonNFA.map Sum.inl M_0).starting_state_list ++ (EpsilonNFA.map Sum.inr M_1).starting_state_list) =
          fun p =>
          match p with
          | Sum.inl p' => p' ∈ M_0.starting_state_list
          | Sum.inr p' => p' ∈ M_1.starting_state_list) ∧
        (fun state =>
            state ∈
              (EpsilonNFA.map Sum.inl M_0).accepting_state_list ++ (EpsilonNFA.map Sum.inr M_1).accepting_state_list) =
          fun p =>
          match p with
          | Sum.inl p' => p' ∈ M_0.accepting_state_list
          | Sum.inr p' => p' ∈ M_1.accepting_state_list

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
⊢ ((fun start_state symbol stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, symbol := symbol, stop_state_list := stop_state_list } ∈
              (EpsilonNFA.map Sum.inl M_0).symbol_arrow_list ++ (EpsilonNFA.map Sum.inr M_1).symbol_arrow_list ∧
            stop_state ∈ stop_state_list) =
      fun p c q =>
      match (p, q) with
      | (Sum.inl p', Sum.inl q') =>
        ∃ stop_state_list,
          { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
            q' ∈ stop_state_list
      | (Sum.inr p', Sum.inr q') =>
        ∃ stop_state_list,
          { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
            q' ∈ stop_state_list
      | x => False) ∧
    ((fun start_state stop_state =>
          ∃ stop_state_list,
            { start_state := start_state, stop_state_list := stop_state_list } ∈
                (EpsilonNFA.map Sum.inl M_0).epsilon_arrow_list ++ (EpsilonNFA.map Sum.inr M_1).epsilon_arrow_list ∧
              stop_state ∈ stop_state_list) =
        fun p q =>
        match (p, q) with
        | (Sum.inl p', 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 p', Sum.inr q') =>
          ∃ stop_state_list,
            { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
        | x => False) ∧
      ((fun state =>
            state ∈
              (EpsilonNFA.map Sum.inl M_0).starting_state_list ++ (EpsilonNFA.map Sum.inr M_1).starting_state_list) =
          fun p =>
          match p with
          | Sum.inl p' => p' ∈ M_0.starting_state_list
          | Sum.inr p' => p' ∈ M_1.starting_state_list) ∧
        (fun state =>
            state ∈
              (EpsilonNFA.map Sum.inl M_0).accepting_state_list ++ (EpsilonNFA.map Sum.inr M_1).accepting_state_list) =
          fun p =>
          match p with
          | Sum.inl p' => p' ∈ M_0.accepting_state_list
          | Sum.inr p' => p' ∈ M_1.accepting_state_list
Tactic:
simp only [EpsilonNFA.map]
State after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
⊢ ((fun start_state symbol stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, symbol := symbol, stop_state_list := stop_state_list } ∈
              List.map
                  (fun arrow =>
                    { start_state := Sum.inl arrow.start_state, symbol := arrow.symbol,
                      stop_state_list := List.map Sum.inl arrow.stop_state_list })
                  M_0.symbol_arrow_list ++
                List.map
                  (fun arrow =>
                    { start_state := Sum.inr arrow.start_state, symbol := arrow.symbol,
                      stop_state_list := List.map Sum.inr arrow.stop_state_list })
                  M_1.symbol_arrow_list ∧
            stop_state ∈ stop_state_list) =
      fun p c q =>
      match (p, q) with
      | (Sum.inl p', Sum.inl q') =>
        ∃ stop_state_list,
          { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
            q' ∈ stop_state_list
      | (Sum.inr p', Sum.inr q') =>
        ∃ stop_state_list,
          { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
            q' ∈ stop_state_list
      | x => False) ∧
    ((fun start_state stop_state =>
          ∃ stop_state_list,
            { start_state := start_state, stop_state_list := 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 })
                    M_1.epsilon_arrow_list ∧
              stop_state ∈ stop_state_list) =
        fun p q =>
        match (p, q) with
        | (Sum.inl p', 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 p', Sum.inr q') =>
          ∃ stop_state_list,
            { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
        | x => False) ∧
      ((fun state => state ∈ List.map Sum.inl M_0.starting_state_list ++ List.map Sum.inr M_1.starting_state_list) =
          fun p =>
          match p with
          | Sum.inl p' => p' ∈ M_0.starting_state_list
          | Sum.inr p' => p' ∈ M_1.starting_state_list) ∧
        (fun state => state ∈ List.map Sum.inl M_0.accepting_state_list ++ List.map Sum.inr M_1.accepting_state_list) =
          fun p =>
          match p with
          | Sum.inl p' => p' ∈ M_0.accepting_state_list
          | Sum.inr p' => p' ∈ M_1.accepting_state_list

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
⊢ ((fun start_state symbol stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, symbol := symbol, stop_state_list := stop_state_list } ∈
              List.map
                  (fun arrow =>
                    { start_state := Sum.inl arrow.start_state, symbol := arrow.symbol,
                      stop_state_list := List.map Sum.inl arrow.stop_state_list })
                  M_0.symbol_arrow_list ++
                List.map
                  (fun arrow =>
                    { start_state := Sum.inr arrow.start_state, symbol := arrow.symbol,
                      stop_state_list := List.map Sum.inr arrow.stop_state_list })
                  M_1.symbol_arrow_list ∧
            stop_state ∈ stop_state_list) =
      fun p c q =>
      match (p, q) with
      | (Sum.inl p', Sum.inl q') =>
        ∃ stop_state_list,
          { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
            q' ∈ stop_state_list
      | (Sum.inr p', Sum.inr q') =>
        ∃ stop_state_list,
          { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
            q' ∈ stop_state_list
      | x => False) ∧
    ((fun start_state stop_state =>
          ∃ stop_state_list,
            { start_state := start_state, stop_state_list := 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 })
                    M_1.epsilon_arrow_list ∧
              stop_state ∈ stop_state_list) =
        fun p q =>
        match (p, q) with
        | (Sum.inl p', 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 p', Sum.inr q') =>
          ∃ stop_state_list,
            { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
        | x => False) ∧
      ((fun state => state ∈ List.map Sum.inl M_0.starting_state_list ++ List.map Sum.inr M_1.starting_state_list) =
          fun p =>
          match p with
          | Sum.inl p' => p' ∈ M_0.starting_state_list
          | Sum.inr p' => p' ∈ M_1.starting_state_list) ∧
        (fun state => state ∈ List.map Sum.inl M_0.accepting_state_list ++ List.map Sum.inr M_1.accepting_state_list) =
          fun p =>
          match p with
          | Sum.inl p' => p' ∈ M_0.accepting_state_list
          | Sum.inr p' => p' ∈ M_1.accepting_state_list
Tactic:
constructor
State after:
case left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
⊢ (fun start_state symbol stop_state =>
      ∃ stop_state_list,
        { start_state := start_state, symbol := symbol, stop_state_list := stop_state_list } ∈
            List.map
                (fun arrow =>
                  { start_state := Sum.inl arrow.start_state, symbol := arrow.symbol,
                    stop_state_list := List.map Sum.inl arrow.stop_state_list })
                M_0.symbol_arrow_list ++
              List.map
                (fun arrow =>
                  { start_state := Sum.inr arrow.start_state, symbol := arrow.symbol,
                    stop_state_list := List.map Sum.inr arrow.stop_state_list })
                M_1.symbol_arrow_list ∧
          stop_state ∈ stop_state_list) =
    fun p c q =>
    match (p, q) with
    | (Sum.inl p', Sum.inl q') =>
      ∃ stop_state_list,
        { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
          q' ∈ stop_state_list
    | (Sum.inr p', Sum.inr q') =>
      ∃ stop_state_list,
        { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
          q' ∈ stop_state_list
    | x => False

case right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
⊢ ((fun start_state stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, stop_state_list := 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 })
                  M_1.epsilon_arrow_list ∧
            stop_state ∈ stop_state_list) =
      fun p q =>
      match (p, q) with
      | (Sum.inl p', 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 p', Sum.inr q') =>
        ∃ stop_state_list,
          { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
      | x => False) ∧
    ((fun state => state ∈ List.map Sum.inl M_0.starting_state_list ++ List.map Sum.inr M_1.starting_state_list) =
        fun p =>
        match p with
        | Sum.inl p' => p' ∈ M_0.starting_state_list
        | Sum.inr p' => p' ∈ M_1.starting_state_list) ∧
      (fun state => state ∈ List.map Sum.inl M_0.accepting_state_list ++ List.map Sum.inr M_1.accepting_state_list) =
        fun p =>
        match p with
        | Sum.inl p' => p' ∈ M_0.accepting_state_list
        | Sum.inr p' => p' ∈ M_1.accepting_state_list

State before:
case left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
⊢ (fun start_state symbol stop_state =>
      ∃ stop_state_list,
        { start_state := start_state, symbol := symbol, stop_state_list := stop_state_list } ∈
            List.map
                (fun arrow =>
                  { start_state := Sum.inl arrow.start_state, symbol := arrow.symbol,
                    stop_state_list := List.map Sum.inl arrow.stop_state_list })
                M_0.symbol_arrow_list ++
              List.map
                (fun arrow =>
                  { start_state := Sum.inr arrow.start_state, symbol := arrow.symbol,
                    stop_state_list := List.map Sum.inr arrow.stop_state_list })
                M_1.symbol_arrow_list ∧
          stop_state ∈ stop_state_list) =
    fun p c q =>
    match (p, q) with
    | (Sum.inl p', Sum.inl q') =>
      ∃ stop_state_list,
        { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
          q' ∈ stop_state_list
    | (Sum.inr p', Sum.inr q') =>
      ∃ stop_state_list,
        { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
          q' ∈ stop_state_list
    | x => False
Tactic:
funext p c q
State after:
case left.h.h.h
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p : σ_0 ⊕ σ_1
c : α
q : σ_0 ⊕ σ_1
⊢ (∃ stop_state_list,
      { start_state := p, symbol := c, stop_state_list := stop_state_list } ∈
          List.map
              (fun arrow =>
                { start_state := Sum.inl arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inl arrow.stop_state_list })
              M_0.symbol_arrow_list ++
            List.map
              (fun arrow =>
                { start_state := Sum.inr arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inr arrow.stop_state_list })
              M_1.symbol_arrow_list ∧
        q ∈ stop_state_list) =
    match (p, q) with
    | (Sum.inl p', Sum.inl q') =>
      ∃ stop_state_list,
        { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
          q' ∈ stop_state_list
    | (Sum.inr p', Sum.inr q') =>
      ∃ stop_state_list,
        { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
          q' ∈ stop_state_list
    | x => False

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

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

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
q : σ_0 ⊕ σ_1
p_0 : σ_0
⊢ (∃ stop_state_list,
      { start_state := Sum.inl p_0, symbol := c, stop_state_list := stop_state_list } ∈
          List.map
              (fun arrow =>
                { start_state := Sum.inl arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inl arrow.stop_state_list })
              M_0.symbol_arrow_list ++
            List.map
              (fun arrow =>
                { start_state := Sum.inr arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inr arrow.stop_state_list })
              M_1.symbol_arrow_list ∧
        q ∈ stop_state_list) =
    match (Sum.inl p_0, q) with
    | (Sum.inl p', Sum.inl q') =>
      ∃ stop_state_list,
        { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
          q' ∈ stop_state_list
    | (Sum.inr p', Sum.inr q') =>
      ∃ stop_state_list,
        { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
          q' ∈ stop_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
c : α
p_0 val✝ : σ_0
⊢ (∃ stop_state_list,
      { start_state := Sum.inl p_0, symbol := c, stop_state_list := stop_state_list } ∈
          List.map
              (fun arrow =>
                { start_state := Sum.inl arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inl arrow.stop_state_list })
              M_0.symbol_arrow_list ++
            List.map
              (fun arrow =>
                { start_state := Sum.inr arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inr arrow.stop_state_list })
              M_1.symbol_arrow_list ∧
        Sum.inl val✝ ∈ stop_state_list) =
    match (Sum.inl p_0, Sum.inl val✝) with
    | (Sum.inl p', Sum.inl q') =>
      ∃ stop_state_list,
        { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
          q' ∈ stop_state_list
    | (Sum.inr p', Sum.inr q') =>
      ∃ stop_state_list,
        { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
          q' ∈ stop_state_list
    | x => False

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

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

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
⊢ (∃ stop_state_list,
      { start_state := Sum.inl p_0, symbol := c, stop_state_list := stop_state_list } ∈
          List.map
              (fun arrow =>
                { start_state := Sum.inl arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inl arrow.stop_state_list })
              M_0.symbol_arrow_list ++
            List.map
              (fun arrow =>
                { start_state := Sum.inr arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inr arrow.stop_state_list })
              M_1.symbol_arrow_list ∧
        Sum.inl q_0 ∈ stop_state_list) =
    match (Sum.inl p_0, Sum.inl q_0) with
    | (Sum.inl p', Sum.inl q') =>
      ∃ stop_state_list,
        { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
          q' ∈ stop_state_list
    | (Sum.inr p', Sum.inr q') =>
      ∃ stop_state_list,
        { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
          q' ∈ stop_state_list
    | x => False
Tactic:
simp only [eq_iff_iff]
State after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
⊢ (∃ stop_state_list,
      { start_state := Sum.inl p_0, symbol := c, stop_state_list := stop_state_list } ∈
          List.map
              (fun arrow =>
                { start_state := Sum.inl arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inl arrow.stop_state_list })
              M_0.symbol_arrow_list ++
            List.map
              (fun arrow =>
                { start_state := Sum.inr arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inr arrow.stop_state_list })
              M_1.symbol_arrow_list ∧
        Sum.inl q_0 ∈ stop_state_list) ↔
    ∃ stop_state_list,
      { start_state := p_0, symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
        q_0 ∈ stop_state_list

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
⊢ (∃ stop_state_list,
      { start_state := Sum.inl p_0, symbol := c, stop_state_list := stop_state_list } ∈
          List.map
              (fun arrow =>
                { start_state := Sum.inl arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inl arrow.stop_state_list })
              M_0.symbol_arrow_list ++
            List.map
              (fun arrow =>
                { start_state := Sum.inr arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inr arrow.stop_state_list })
              M_1.symbol_arrow_list ∧
        Sum.inl q_0 ∈ stop_state_list) ↔
    ∃ stop_state_list,
      { start_state := p_0, symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
        q_0 ∈ stop_state_list
Tactic:
constructor
State after:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
⊢ (∃ stop_state_list,
      { start_state := Sum.inl p_0, symbol := c, stop_state_list := stop_state_list } ∈
          List.map
              (fun arrow =>
                { start_state := Sum.inl arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inl arrow.stop_state_list })
              M_0.symbol_arrow_list ++
            List.map
              (fun arrow =>
                { start_state := Sum.inr arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inr arrow.stop_state_list })
              M_1.symbol_arrow_list ∧
        Sum.inl q_0 ∈ stop_state_list) →
    ∃ stop_state_list,
      { start_state := p_0, symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
        q_0 ∈ stop_state_list

case mpr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
⊢ (∃ stop_state_list,
      { start_state := p_0, symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
        q_0 ∈ stop_state_list) →
    ∃ stop_state_list,
      { start_state := Sum.inl p_0, symbol := c, stop_state_list := stop_state_list } ∈
          List.map
              (fun arrow =>
                { start_state := Sum.inl arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inl arrow.stop_state_list })
              M_0.symbol_arrow_list ++
            List.map
              (fun arrow =>
                { start_state := Sum.inr arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inr arrow.stop_state_list })
              M_1.symbol_arrow_list ∧
        Sum.inl q_0 ∈ stop_state_list

State before:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
⊢ (∃ stop_state_list,
      { start_state := Sum.inl p_0, symbol := c, stop_state_list := stop_state_list } ∈
          List.map
              (fun arrow =>
                { start_state := Sum.inl arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inl arrow.stop_state_list })
              M_0.symbol_arrow_list ++
            List.map
              (fun arrow =>
                { start_state := Sum.inr arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inr arrow.stop_state_list })
              M_1.symbol_arrow_list ∧
        Sum.inl q_0 ∈ stop_state_list) →
    ∃ stop_state_list,
      { start_state := p_0, symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
        q_0 ∈ stop_state_list
Tactic:
simp
State after:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
⊢ ∀ (x : List (σ_0 ⊕ σ_1)),
    ∀ x_1 ∈ M_0.symbol_arrow_list,
      x_1.start_state = p_0 →
        x_1.symbol = c →
          List.map Sum.inl x_1.stop_state_list = x →
            Sum.inl q_0 ∈ x →
              ∃ stop_state_list,
                { start_state := p_0, symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
                  q_0 ∈ stop_state_list

State before:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
⊢ ∀ (x : List (σ_0 ⊕ σ_1)),
    ∀ x_1 ∈ M_0.symbol_arrow_list,
      x_1.start_state = p_0 →
        x_1.symbol = c →
          List.map Sum.inl x_1.stop_state_list = x →
            Sum.inl q_0 ∈ x →
              ∃ stop_state_list,
                { start_state := p_0, symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
                  q_0 ∈ stop_state_list
Tactic:
intro xs x a1 a2 a3 a4 a5
State after:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a1 : x ∈ M_0.symbol_arrow_list
a2 : x.start_state = p_0
a3 : x.symbol = c
a4 : List.map Sum.inl x.stop_state_list = xs
a5 : Sum.inl q_0 ∈ xs
⊢ ∃ stop_state_list,
    { start_state := p_0, symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
      q_0 ∈ stop_state_list

State before:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a1 : x ∈ M_0.symbol_arrow_list
a2 : x.start_state = p_0
a3 : x.symbol = c
a4 : List.map Sum.inl x.stop_state_list = xs
a5 : Sum.inl q_0 ∈ xs
⊢ ∃ stop_state_list,
    { start_state := p_0, symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
      q_0 ∈ stop_state_list
Tactic:
simp only [← a4] at a5
State after:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a1 : x ∈ M_0.symbol_arrow_list
a2 : x.start_state = p_0
a3 : x.symbol = c
a4 : List.map Sum.inl x.stop_state_list = xs
a5 : Sum.inl q_0 ∈ List.map Sum.inl x.stop_state_list
⊢ ∃ stop_state_list,
    { start_state := p_0, symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
      q_0 ∈ stop_state_list

State before:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a1 : x ∈ M_0.symbol_arrow_list
a2 : x.start_state = p_0
a3 : x.symbol = c
a4 : List.map Sum.inl x.stop_state_list = xs
a5 : Sum.inl q_0 ∈ List.map Sum.inl x.stop_state_list
⊢ ∃ stop_state_list,
    { start_state := p_0, symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
      q_0 ∈ stop_state_list
Tactic:
clear a4
State after:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a1 : x ∈ M_0.symbol_arrow_list
a2 : x.start_state = p_0
a3 : x.symbol = c
a5 : Sum.inl q_0 ∈ List.map Sum.inl x.stop_state_list
⊢ ∃ stop_state_list,
    { start_state := p_0, symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
      q_0 ∈ stop_state_list

State before:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a1 : x ∈ M_0.symbol_arrow_list
a2 : x.start_state = p_0
a3 : x.symbol = c
a5 : Sum.inl q_0 ∈ List.map Sum.inl x.stop_state_list
⊢ ∃ stop_state_list,
    { start_state := p_0, symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
      q_0 ∈ stop_state_list
Tactic:
simp only [← a2]
State after:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a1 : x ∈ M_0.symbol_arrow_list
a2 : x.start_state = p_0
a3 : x.symbol = c
a5 : Sum.inl q_0 ∈ List.map Sum.inl x.stop_state_list
⊢ ∃ stop_state_list,
    { start_state := x.start_state, symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
      q_0 ∈ stop_state_list

State before:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a1 : x ∈ M_0.symbol_arrow_list
a2 : x.start_state = p_0
a3 : x.symbol = c
a5 : Sum.inl q_0 ∈ List.map Sum.inl x.stop_state_list
⊢ ∃ stop_state_list,
    { start_state := x.start_state, symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
      q_0 ∈ stop_state_list
Tactic:
simp only [← a3]
State after:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a1 : x ∈ M_0.symbol_arrow_list
a2 : x.start_state = p_0
a3 : x.symbol = c
a5 : Sum.inl q_0 ∈ List.map Sum.inl x.stop_state_list
⊢ ∃ stop_state_list,
    { start_state := x.start_state, symbol := x.symbol, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
      q_0 ∈ stop_state_list

State before:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a1 : x ∈ M_0.symbol_arrow_list
a2 : x.start_state = p_0
a3 : x.symbol = c
a5 : Sum.inl q_0 ∈ List.map Sum.inl x.stop_state_list
⊢ ∃ stop_state_list,
    { start_state := x.start_state, symbol := x.symbol, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
      q_0 ∈ stop_state_list
Tactic:
apply Exists.intro x.stop_state_list
State after:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a1 : x ∈ M_0.symbol_arrow_list
a2 : x.start_state = p_0
a3 : x.symbol = c
a5 : Sum.inl q_0 ∈ List.map Sum.inl x.stop_state_list
⊢ { start_state := x.start_state, symbol := x.symbol, stop_state_list := x.stop_state_list } ∈ M_0.symbol_arrow_list ∧
    q_0 ∈ x.stop_state_list

State before:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a1 : x ∈ M_0.symbol_arrow_list
a2 : x.start_state = p_0
a3 : x.symbol = c
a5 : Sum.inl q_0 ∈ List.map Sum.inl x.stop_state_list
⊢ { start_state := x.start_state, symbol := x.symbol, stop_state_list := x.stop_state_list } ∈ M_0.symbol_arrow_list ∧
    q_0 ∈ x.stop_state_list
Tactic:
constructor
State after:
case mp.left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a1 : x ∈ M_0.symbol_arrow_list
a2 : x.start_state = p_0
a3 : x.symbol = c
a5 : Sum.inl q_0 ∈ List.map Sum.inl x.stop_state_list
⊢ { start_state := x.start_state, symbol := x.symbol, stop_state_list := x.stop_state_list } ∈ M_0.symbol_arrow_list

case mp.right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a1 : x ∈ M_0.symbol_arrow_list
a2 : x.start_state = p_0
a3 : x.symbol = c
a5 : Sum.inl q_0 ∈ List.map Sum.inl x.stop_state_list
⊢ q_0 ∈ x.stop_state_list

State before:
case mp.left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a1 : x ∈ M_0.symbol_arrow_list
a2 : x.start_state = p_0
a3 : x.symbol = c
a5 : Sum.inl q_0 ∈ List.map Sum.inl x.stop_state_list
⊢ { start_state := x.start_state, symbol := x.symbol, stop_state_list := x.stop_state_list } ∈ M_0.symbol_arrow_list
Tactic:
exact a1
State after:
no goals

State before:
case mp.right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a1 : x ∈ M_0.symbol_arrow_list
a2 : x.start_state = p_0
a3 : x.symbol = c
a5 : Sum.inl q_0 ∈ List.map Sum.inl x.stop_state_list
⊢ q_0 ∈ x.stop_state_list
Tactic:
simp at a5
State after:
case mp.right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a1 : x ∈ M_0.symbol_arrow_list
a2 : x.start_state = p_0
a3 : x.symbol = c
a5 : q_0 ∈ x.stop_state_list
⊢ q_0 ∈ x.stop_state_list

State before:
case mp.right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a1 : x ∈ M_0.symbol_arrow_list
a2 : x.start_state = p_0
a3 : x.symbol = c
a5 : q_0 ∈ x.stop_state_list
⊢ q_0 ∈ x.stop_state_list
Tactic:
exact a5
State after:
no goals

State before:
case mpr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
⊢ (∃ stop_state_list,
      { start_state := p_0, symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
        q_0 ∈ stop_state_list) →
    ∃ stop_state_list,
      { start_state := Sum.inl p_0, symbol := c, stop_state_list := stop_state_list } ∈
          List.map
              (fun arrow =>
                { start_state := Sum.inl arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inl arrow.stop_state_list })
              M_0.symbol_arrow_list ++
            List.map
              (fun arrow =>
                { start_state := Sum.inr arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inr arrow.stop_state_list })
              M_1.symbol_arrow_list ∧
        Sum.inl q_0 ∈ stop_state_list
Tactic:
simp
State after:
case mpr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
⊢ ∀ (x : List σ_0),
    { start_state := p_0, symbol := c, stop_state_list := x } ∈ M_0.symbol_arrow_list →
      q_0 ∈ x →
        ∃ stop_state_list,
          (∃ a ∈ M_0.symbol_arrow_list,
              a.start_state = p_0 ∧ a.symbol = c ∧ List.map Sum.inl a.stop_state_list = stop_state_list) ∧
            Sum.inl q_0 ∈ stop_state_list

State before:
case mpr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
⊢ ∀ (x : List σ_0),
    { start_state := p_0, symbol := c, stop_state_list := x } ∈ M_0.symbol_arrow_list →
      q_0 ∈ x →
        ∃ stop_state_list,
          (∃ a ∈ M_0.symbol_arrow_list,
              a.start_state = p_0 ∧ a.symbol = c ∧ List.map Sum.inl a.stop_state_list = stop_state_list) ∧
            Sum.inl q_0 ∈ stop_state_list
Tactic:
intro xs x a1
State after:
case mpr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List σ_0
x : { start_state := p_0, symbol := c, stop_state_list := xs } ∈ M_0.symbol_arrow_list
a1 : q_0 ∈ xs
⊢ ∃ stop_state_list,
    (∃ a ∈ M_0.symbol_arrow_list,
        a.start_state = p_0 ∧ a.symbol = c ∧ List.map Sum.inl a.stop_state_list = stop_state_list) ∧
      Sum.inl q_0 ∈ stop_state_list

State before:
case mpr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List σ_0
x : { start_state := p_0, symbol := c, stop_state_list := xs } ∈ M_0.symbol_arrow_list
a1 : q_0 ∈ xs
⊢ ∃ stop_state_list,
    (∃ a ∈ M_0.symbol_arrow_list,
        a.start_state = p_0 ∧ a.symbol = c ∧ List.map Sum.inl a.stop_state_list = stop_state_list) ∧
      Sum.inl q_0 ∈ stop_state_list
Tactic:
apply Exists.intro (xs.map Sum.inl)
State after:
case mpr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List σ_0
x : { start_state := p_0, symbol := c, stop_state_list := xs } ∈ M_0.symbol_arrow_list
a1 : q_0 ∈ xs
⊢ (∃ a ∈ M_0.symbol_arrow_list,
      a.start_state = p_0 ∧ a.symbol = c ∧ List.map Sum.inl a.stop_state_list = List.map Sum.inl xs) ∧
    Sum.inl q_0 ∈ List.map Sum.inl xs

State before:
case mpr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List σ_0
x : { start_state := p_0, symbol := c, stop_state_list := xs } ∈ M_0.symbol_arrow_list
a1 : q_0 ∈ xs
⊢ (∃ a ∈ M_0.symbol_arrow_list,
      a.start_state = p_0 ∧ a.symbol = c ∧ List.map Sum.inl a.stop_state_list = List.map Sum.inl xs) ∧
    Sum.inl q_0 ∈ List.map Sum.inl xs
Tactic:
constructor
State after:
case mpr.left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List σ_0
x : { start_state := p_0, symbol := c, stop_state_list := xs } ∈ M_0.symbol_arrow_list
a1 : q_0 ∈ xs
⊢ ∃ a ∈ M_0.symbol_arrow_list,
    a.start_state = p_0 ∧ a.symbol = c ∧ List.map Sum.inl a.stop_state_list = List.map Sum.inl xs

case mpr.right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List σ_0
x : { start_state := p_0, symbol := c, stop_state_list := xs } ∈ M_0.symbol_arrow_list
a1 : q_0 ∈ xs
⊢ Sum.inl q_0 ∈ List.map Sum.inl xs

State before:
case mpr.left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List σ_0
x : { start_state := p_0, symbol := c, stop_state_list := xs } ∈ M_0.symbol_arrow_list
a1 : q_0 ∈ xs
⊢ ∃ a ∈ M_0.symbol_arrow_list,
    a.start_state = p_0 ∧ a.symbol = c ∧ List.map Sum.inl a.stop_state_list = List.map Sum.inl xs
Tactic:
apply Exists.intro { start_state := p_0, symbol := c, stop_state_list := xs }
State after:
case mpr.left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List σ_0
x : { start_state := p_0, symbol := c, stop_state_list := xs } ∈ M_0.symbol_arrow_list
a1 : q_0 ∈ xs
⊢ { start_state := p_0, symbol := c, stop_state_list := xs } ∈ M_0.symbol_arrow_list ∧
    { start_state := p_0, symbol := c, stop_state_list := xs }.start_state = p_0 ∧
      { start_state := p_0, symbol := c, stop_state_list := xs }.symbol = c ∧
        List.map Sum.inl { start_state := p_0, symbol := c, stop_state_list := xs }.stop_state_list =
          List.map Sum.inl xs

State before:
case mpr.left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List σ_0
x : { start_state := p_0, symbol := c, stop_state_list := xs } ∈ M_0.symbol_arrow_list
a1 : q_0 ∈ xs
⊢ { start_state := p_0, symbol := c, stop_state_list := xs } ∈ M_0.symbol_arrow_list ∧
    { start_state := p_0, symbol := c, stop_state_list := xs }.start_state = p_0 ∧
      { start_state := p_0, symbol := c, stop_state_list := xs }.symbol = c ∧
        List.map Sum.inl { start_state := p_0, symbol := c, stop_state_list := xs }.stop_state_list =
          List.map Sum.inl xs
Tactic:
simp
State after:
case mpr.left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List σ_0
x : { start_state := p_0, symbol := c, stop_state_list := xs } ∈ M_0.symbol_arrow_list
a1 : q_0 ∈ xs
⊢ { start_state := p_0, symbol := c, stop_state_list := xs } ∈ M_0.symbol_arrow_list

State before:
case mpr.left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List σ_0
x : { start_state := p_0, symbol := c, stop_state_list := xs } ∈ M_0.symbol_arrow_list
a1 : q_0 ∈ xs
⊢ { start_state := p_0, symbol := c, stop_state_list := xs } ∈ M_0.symbol_arrow_list
Tactic:
exact x
State after:
no goals

State before:
case mpr.right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List σ_0
x : { start_state := p_0, symbol := c, stop_state_list := xs } ∈ M_0.symbol_arrow_list
a1 : q_0 ∈ xs
⊢ Sum.inl q_0 ∈ List.map Sum.inl xs
Tactic:
simp
State after:
case mpr.right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List σ_0
x : { start_state := p_0, symbol := c, stop_state_list := xs } ∈ M_0.symbol_arrow_list
a1 : q_0 ∈ xs
⊢ q_0 ∈ xs

State before:
case mpr.right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List σ_0
x : { start_state := p_0, symbol := c, stop_state_list := xs } ∈ M_0.symbol_arrow_list
a1 : q_0 ∈ xs
⊢ q_0 ∈ xs
Tactic:
exact a1
State after:
no goals

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

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 : σ_0
q0 : σ_1
⊢ ∀ (x : List (σ_0 ⊕ σ_1)),
    ∀ x_1 ∈ M_0.symbol_arrow_list,
      x_1.start_state = p_0 → x_1.symbol = c → List.map Sum.inl x_1.stop_state_list = x → Sum.inr q0 ∉ x
Tactic:
intro xs x _ _ _ a4
State after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 : σ_0
q0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a✝² : x ∈ M_0.symbol_arrow_list
a✝¹ : x.start_state = p_0
a✝ : x.symbol = c
a4 : List.map Sum.inl x.stop_state_list = xs
⊢ Sum.inr q0 ∉ xs

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 : σ_0
q0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a✝² : x ∈ M_0.symbol_arrow_list
a✝¹ : x.start_state = p_0
a✝ : x.symbol = c
a4 : List.map Sum.inl x.stop_state_list = xs
⊢ Sum.inr q0 ∉ xs
Tactic:
simp only [← a4]
State after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 : σ_0
q0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a✝² : x ∈ M_0.symbol_arrow_list
a✝¹ : x.start_state = p_0
a✝ : x.symbol = c
a4 : List.map Sum.inl x.stop_state_list = xs
⊢ Sum.inr q0 ∉ List.map Sum.inl x.stop_state_list

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 : σ_0
q0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a✝² : x ∈ M_0.symbol_arrow_list
a✝¹ : x.start_state = p_0
a✝ : x.symbol = c
a4 : List.map Sum.inl x.stop_state_list = xs
⊢ Sum.inr q0 ∉ List.map Sum.inl 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
c : α
q : σ_0 ⊕ σ_1
p0 : σ_1
⊢ (∃ stop_state_list,
      { start_state := Sum.inr p0, symbol := c, stop_state_list := stop_state_list } ∈
          List.map
              (fun arrow =>
                { start_state := Sum.inl arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inl arrow.stop_state_list })
              M_0.symbol_arrow_list ++
            List.map
              (fun arrow =>
                { start_state := Sum.inr arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inr arrow.stop_state_list })
              M_1.symbol_arrow_list ∧
        q ∈ stop_state_list) =
    match (Sum.inr p0, q) with
    | (Sum.inl p', Sum.inl q') =>
      ∃ stop_state_list,
        { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
          q' ∈ stop_state_list
    | (Sum.inr p', Sum.inr q') =>
      ∃ stop_state_list,
        { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
          q' ∈ stop_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
c : α
p0 : σ_1
val✝ : σ_0
⊢ (∃ stop_state_list,
      { start_state := Sum.inr p0, symbol := c, stop_state_list := stop_state_list } ∈
          List.map
              (fun arrow =>
                { start_state := Sum.inl arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inl arrow.stop_state_list })
              M_0.symbol_arrow_list ++
            List.map
              (fun arrow =>
                { start_state := Sum.inr arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inr arrow.stop_state_list })
              M_1.symbol_arrow_list ∧
        Sum.inl val✝ ∈ stop_state_list) =
    match (Sum.inr p0, Sum.inl val✝) with
    | (Sum.inl p', Sum.inl q') =>
      ∃ stop_state_list,
        { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
          q' ∈ stop_state_list
    | (Sum.inr p', Sum.inr q') =>
      ∃ stop_state_list,
        { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
          q' ∈ stop_state_list
    | x => False

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

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 : σ_1
q_0 : σ_0
⊢ (∃ stop_state_list,
      { start_state := Sum.inr p0, symbol := c, stop_state_list := stop_state_list } ∈
          List.map
              (fun arrow =>
                { start_state := Sum.inl arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inl arrow.stop_state_list })
              M_0.symbol_arrow_list ++
            List.map
              (fun arrow =>
                { start_state := Sum.inr arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inr arrow.stop_state_list })
              M_1.symbol_arrow_list ∧
        Sum.inl q_0 ∈ stop_state_list) =
    match (Sum.inr p0, Sum.inl q_0) with
    | (Sum.inl p', Sum.inl q') =>
      ∃ stop_state_list,
        { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
          q' ∈ stop_state_list
    | (Sum.inr p', Sum.inr q') =>
      ∃ stop_state_list,
        { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
          q' ∈ stop_state_list
    | x => False
Tactic:
simp only [eq_iff_iff]
State after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 : σ_1
q_0 : σ_0
⊢ (∃ stop_state_list,
      { start_state := Sum.inr p0, symbol := c, stop_state_list := stop_state_list } ∈
          List.map
              (fun arrow =>
                { start_state := Sum.inl arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inl arrow.stop_state_list })
              M_0.symbol_arrow_list ++
            List.map
              (fun arrow =>
                { start_state := Sum.inr arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inr arrow.stop_state_list })
              M_1.symbol_arrow_list ∧
        Sum.inl q_0 ∈ stop_state_list) ↔
    False

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 : σ_1
q_0 : σ_0
⊢ (∃ stop_state_list,
      { start_state := Sum.inr p0, symbol := c, stop_state_list := stop_state_list } ∈
          List.map
              (fun arrow =>
                { start_state := Sum.inl arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inl arrow.stop_state_list })
              M_0.symbol_arrow_list ++
            List.map
              (fun arrow =>
                { start_state := Sum.inr arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inr arrow.stop_state_list })
              M_1.symbol_arrow_list ∧
        Sum.inl q_0 ∈ stop_state_list) ↔
    False
Tactic:
constructor
State after:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 : σ_1
q_0 : σ_0
⊢ (∃ stop_state_list,
      { start_state := Sum.inr p0, symbol := c, stop_state_list := stop_state_list } ∈
          List.map
              (fun arrow =>
                { start_state := Sum.inl arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inl arrow.stop_state_list })
              M_0.symbol_arrow_list ++
            List.map
              (fun arrow =>
                { start_state := Sum.inr arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inr arrow.stop_state_list })
              M_1.symbol_arrow_list ∧
        Sum.inl q_0 ∈ stop_state_list) →
    False

case mpr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 : σ_1
q_0 : σ_0
⊢ False →
    ∃ stop_state_list,
      { start_state := Sum.inr p0, symbol := c, stop_state_list := stop_state_list } ∈
          List.map
              (fun arrow =>
                { start_state := Sum.inl arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inl arrow.stop_state_list })
              M_0.symbol_arrow_list ++
            List.map
              (fun arrow =>
                { start_state := Sum.inr arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inr arrow.stop_state_list })
              M_1.symbol_arrow_list ∧
        Sum.inl q_0 ∈ stop_state_list

State before:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 : σ_1
q_0 : σ_0
⊢ (∃ stop_state_list,
      { start_state := Sum.inr p0, symbol := c, stop_state_list := stop_state_list } ∈
          List.map
              (fun arrow =>
                { start_state := Sum.inl arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inl arrow.stop_state_list })
              M_0.symbol_arrow_list ++
            List.map
              (fun arrow =>
                { start_state := Sum.inr arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inr arrow.stop_state_list })
              M_1.symbol_arrow_list ∧
        Sum.inl q_0 ∈ stop_state_list) →
    False
Tactic:
simp
State after:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 : σ_1
q_0 : σ_0
⊢ ∀ (x : List (σ_0 ⊕ σ_1)),
    ∀ x_1 ∈ M_1.symbol_arrow_list,
      x_1.start_state = p0 → x_1.symbol = c → List.map Sum.inr x_1.stop_state_list = x → Sum.inl q_0 ∉ x

State before:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 : σ_1
q_0 : σ_0
⊢ ∀ (x : List (σ_0 ⊕ σ_1)),
    ∀ x_1 ∈ M_1.symbol_arrow_list,
      x_1.start_state = p0 → x_1.symbol = c → List.map Sum.inr x_1.stop_state_list = x → Sum.inl q_0 ∉ x
Tactic:
intro xs x _ _ _ a4
State after:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 : σ_1
q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_1
a✝² : x ∈ M_1.symbol_arrow_list
a✝¹ : x.start_state = p0
a✝ : x.symbol = c
a4 : List.map Sum.inr x.stop_state_list = xs
⊢ Sum.inl q_0 ∉ xs

State before:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 : σ_1
q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_1
a✝² : x ∈ M_1.symbol_arrow_list
a✝¹ : x.start_state = p0
a✝ : x.symbol = c
a4 : List.map Sum.inr x.stop_state_list = xs
⊢ Sum.inl q_0 ∉ xs
Tactic:
simp only [← a4]
State after:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 : σ_1
q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_1
a✝² : x ∈ M_1.symbol_arrow_list
a✝¹ : x.start_state = p0
a✝ : x.symbol = c
a4 : List.map Sum.inr x.stop_state_list = xs
⊢ Sum.inl q_0 ∉ List.map Sum.inr x.stop_state_list

State before:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 : σ_1
q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_1
a✝² : x ∈ M_1.symbol_arrow_list
a✝¹ : x.start_state = p0
a✝ : x.symbol = c
a4 : List.map Sum.inr x.stop_state_list = xs
⊢ Sum.inl q_0 ∉ List.map Sum.inr x.stop_state_list
Tactic:
simp
State after:
no goals

State before:
case mpr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 : σ_1
q_0 : σ_0
⊢ False →
    ∃ stop_state_list,
      { start_state := Sum.inr p0, symbol := c, stop_state_list := stop_state_list } ∈
          List.map
              (fun arrow =>
                { start_state := Sum.inl arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inl arrow.stop_state_list })
              M_0.symbol_arrow_list ++
            List.map
              (fun arrow =>
                { start_state := Sum.inr arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inr arrow.stop_state_list })
              M_1.symbol_arrow_list ∧
        Sum.inl q_0 ∈ 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
c : α
p0 q0 : σ_1
⊢ (∃ stop_state_list,
      { start_state := Sum.inr p0, symbol := c, stop_state_list := stop_state_list } ∈
          List.map
              (fun arrow =>
                { start_state := Sum.inl arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inl arrow.stop_state_list })
              M_0.symbol_arrow_list ++
            List.map
              (fun arrow =>
                { start_state := Sum.inr arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inr arrow.stop_state_list })
              M_1.symbol_arrow_list ∧
        Sum.inr q0 ∈ stop_state_list) =
    match (Sum.inr p0, Sum.inr q0) with
    | (Sum.inl p', Sum.inl q') =>
      ∃ stop_state_list,
        { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
          q' ∈ stop_state_list
    | (Sum.inr p', Sum.inr q') =>
      ∃ stop_state_list,
        { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
          q' ∈ stop_state_list
    | x => False
Tactic:
simp
State after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
⊢ (∃ stop_state_list,
      (∃ a ∈ M_1.symbol_arrow_list,
          a.start_state = p0 ∧ a.symbol = c ∧ List.map Sum.inr a.stop_state_list = stop_state_list) ∧
        Sum.inr q0 ∈ stop_state_list) ↔
    ∃ stop_state_list,
      { start_state := p0, symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
        q0 ∈ stop_state_list

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
⊢ (∃ stop_state_list,
      (∃ a ∈ M_1.symbol_arrow_list,
          a.start_state = p0 ∧ a.symbol = c ∧ List.map Sum.inr a.stop_state_list = stop_state_list) ∧
        Sum.inr q0 ∈ stop_state_list) ↔
    ∃ stop_state_list,
      { start_state := p0, symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
        q0 ∈ stop_state_list
Tactic:
constructor
State after:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
⊢ (∃ stop_state_list,
      (∃ a ∈ M_1.symbol_arrow_list,
          a.start_state = p0 ∧ a.symbol = c ∧ List.map Sum.inr a.stop_state_list = stop_state_list) ∧
        Sum.inr q0 ∈ stop_state_list) →
    ∃ stop_state_list,
      { start_state := p0, symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
        q0 ∈ stop_state_list

case mpr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
⊢ (∃ stop_state_list,
      { start_state := p0, symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
        q0 ∈ stop_state_list) →
    ∃ stop_state_list,
      (∃ a ∈ M_1.symbol_arrow_list,
          a.start_state = p0 ∧ a.symbol = c ∧ List.map Sum.inr a.stop_state_list = stop_state_list) ∧
        Sum.inr q0 ∈ stop_state_list

State before:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
⊢ (∃ stop_state_list,
      (∃ a ∈ M_1.symbol_arrow_list,
          a.start_state = p0 ∧ a.symbol = c ∧ List.map Sum.inr a.stop_state_list = stop_state_list) ∧
        Sum.inr q0 ∈ stop_state_list) →
    ∃ stop_state_list,
      { start_state := p0, symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
        q0 ∈ stop_state_list
Tactic:
intro a1
State after:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
a1 :
  ∃ stop_state_list,
    (∃ a ∈ M_1.symbol_arrow_list,
        a.start_state = p0 ∧ a.symbol = c ∧ List.map Sum.inr a.stop_state_list = stop_state_list) ∧
      Sum.inr q0 ∈ stop_state_list
⊢ ∃ stop_state_list,
    { start_state := p0, symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
      q0 ∈ stop_state_list

State before:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
a1 :
  ∃ stop_state_list,
    (∃ a ∈ M_1.symbol_arrow_list,
        a.start_state = p0 ∧ a.symbol = c ∧ List.map Sum.inr a.stop_state_list = stop_state_list) ∧
      Sum.inr q0 ∈ stop_state_list
⊢ ∃ stop_state_list,
    { start_state := p0, symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
      q0 ∈ stop_state_list
Tactic:
cases a1
State after:
case mp.intro
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
w✝ : List (σ_0 ⊕ σ_1)
h✝ :
  (∃ a ∈ M_1.symbol_arrow_list, a.start_state = p0 ∧ a.symbol = c ∧ List.map Sum.inr a.stop_state_list = w✝) ∧
    Sum.inr q0 ∈ w✝
⊢ ∃ stop_state_list,
    { start_state := p0, symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
      q0 ∈ stop_state_list

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List (σ_0 ⊕ σ_1)
a2 :
  (∃ a ∈ M_1.symbol_arrow_list, a.start_state = p0 ∧ a.symbol = c ∧ List.map Sum.inr a.stop_state_list = xs) ∧
    Sum.inr q0 ∈ xs
⊢ ∃ stop_state_list,
    { start_state := p0, symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
      q0 ∈ stop_state_list
Tactic:
cases a2
State after:
case intro
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List (σ_0 ⊕ σ_1)
left✝ : ∃ a ∈ M_1.symbol_arrow_list, a.start_state = p0 ∧ a.symbol = c ∧ List.map Sum.inr a.stop_state_list = xs
right✝ : Sum.inr q0 ∈ xs
⊢ ∃ stop_state_list,
    { start_state := p0, symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
      q0 ∈ stop_state_list

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List (σ_0 ⊕ σ_1)
a2_left : ∃ a ∈ M_1.symbol_arrow_list, a.start_state = p0 ∧ a.symbol = c ∧ List.map Sum.inr a.stop_state_list = xs
a2_right : Sum.inr q0 ∈ xs
⊢ ∃ stop_state_list,
    { start_state := p0, symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
      q0 ∈ stop_state_list
Tactic:
cases a2_left
State after:
case intro
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List (σ_0 ⊕ σ_1)
a2_right : Sum.inr q0 ∈ xs
w✝ : SymbolArrow α σ_1
h✝ : w✝ ∈ M_1.symbol_arrow_list ∧ w✝.start_state = p0 ∧ w✝.symbol = c ∧ List.map Sum.inr w✝.stop_state_list = xs
⊢ ∃ stop_state_list,
    { start_state := p0, symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
      q0 ∈ stop_state_list

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List (σ_0 ⊕ σ_1)
a2_right : Sum.inr q0 ∈ xs
x : SymbolArrow α σ_1
a3 : x ∈ M_1.symbol_arrow_list ∧ x.start_state = p0 ∧ x.symbol = c ∧ List.map Sum.inr x.stop_state_list = xs
⊢ ∃ stop_state_list,
    { start_state := p0, symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
      q0 ∈ stop_state_list
Tactic:
cases a3
State after:
case intro
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List (σ_0 ⊕ σ_1)
a2_right : Sum.inr q0 ∈ xs
x : SymbolArrow α σ_1
left✝ : x ∈ M_1.symbol_arrow_list
right✝ : x.start_state = p0 ∧ x.symbol = c ∧ List.map Sum.inr x.stop_state_list = xs
⊢ ∃ stop_state_list,
    { start_state := p0, symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
      q0 ∈ stop_state_list

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List (σ_0 ⊕ σ_1)
a2_right : Sum.inr q0 ∈ xs
x : SymbolArrow α σ_1
a3_left : x ∈ M_1.symbol_arrow_list
a3_right : x.start_state = p0 ∧ x.symbol = c ∧ List.map Sum.inr x.stop_state_list = xs
⊢ ∃ stop_state_list,
    { start_state := p0, symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
      q0 ∈ stop_state_list
Tactic:
cases a3_right
State after:
case intro
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List (σ_0 ⊕ σ_1)
a2_right : Sum.inr q0 ∈ xs
x : SymbolArrow α σ_1
a3_left : x ∈ M_1.symbol_arrow_list
left✝ : x.start_state = p0
right✝ : x.symbol = c ∧ List.map Sum.inr x.stop_state_list = xs
⊢ ∃ stop_state_list,
    { start_state := p0, symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
      q0 ∈ stop_state_list

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List (σ_0 ⊕ σ_1)
a2_right : Sum.inr q0 ∈ xs
x : SymbolArrow α σ_1
a3_left : x ∈ M_1.symbol_arrow_list
a3_right_left : x.start_state = p0
a3_right_right : x.symbol = c ∧ List.map Sum.inr x.stop_state_list = xs
⊢ ∃ stop_state_list,
    { start_state := p0, symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
      q0 ∈ stop_state_list
Tactic:
cases a3_right_right
State after:
case intro
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List (σ_0 ⊕ σ_1)
a2_right : Sum.inr q0 ∈ xs
x : SymbolArrow α σ_1
a3_left : x ∈ M_1.symbol_arrow_list
a3_right_left : x.start_state = p0
left✝ : x.symbol = c
right✝ : List.map Sum.inr x.stop_state_list = xs
⊢ ∃ stop_state_list,
    { start_state := p0, symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
      q0 ∈ stop_state_list

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List (σ_0 ⊕ σ_1)
a2_right : Sum.inr q0 ∈ xs
x : SymbolArrow α σ_1
a3_left : x ∈ M_1.symbol_arrow_list
a3_right_left : x.start_state = p0
a3_right_right_left : x.symbol = c
a3_right_right_right : List.map Sum.inr x.stop_state_list = xs
⊢ ∃ stop_state_list,
    { start_state := p0, symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
      q0 ∈ stop_state_list
Tactic:
simp only [← a3_right_right_right] at a2_right
State after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_1
a3_left : x ∈ M_1.symbol_arrow_list
a3_right_left : x.start_state = p0
a3_right_right_left : x.symbol = c
a3_right_right_right : List.map Sum.inr x.stop_state_list = xs
a2_right : Sum.inr q0 ∈ List.map Sum.inr x.stop_state_list
⊢ ∃ stop_state_list,
    { start_state := p0, symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
      q0 ∈ stop_state_list

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_1
a3_left : x ∈ M_1.symbol_arrow_list
a3_right_left : x.start_state = p0
a3_right_right_left : x.symbol = c
a3_right_right_right : List.map Sum.inr x.stop_state_list = xs
a2_right : Sum.inr q0 ∈ List.map Sum.inr x.stop_state_list
⊢ ∃ stop_state_list,
    { start_state := p0, symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
      q0 ∈ stop_state_list
Tactic:
clear a3_right_right_right
State after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_1
a3_left : x ∈ M_1.symbol_arrow_list
a3_right_left : x.start_state = p0
a3_right_right_left : x.symbol = c
a2_right : Sum.inr q0 ∈ List.map Sum.inr x.stop_state_list
⊢ ∃ stop_state_list,
    { start_state := p0, symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
      q0 ∈ stop_state_list

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_1
a3_left : x ∈ M_1.symbol_arrow_list
a3_right_left : x.start_state = p0
a3_right_right_left : x.symbol = c
a2_right : Sum.inr q0 ∈ List.map Sum.inr x.stop_state_list
⊢ ∃ stop_state_list,
    { start_state := p0, symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
      q0 ∈ stop_state_list
Tactic:
simp only [← a3_right_left]
State after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_1
a3_left : x ∈ M_1.symbol_arrow_list
a3_right_left : x.start_state = p0
a3_right_right_left : x.symbol = c
a2_right : Sum.inr q0 ∈ List.map Sum.inr x.stop_state_list
⊢ ∃ stop_state_list,
    { start_state := x.start_state, symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
      q0 ∈ stop_state_list

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_1
a3_left : x ∈ M_1.symbol_arrow_list
a3_right_left : x.start_state = p0
a3_right_right_left : x.symbol = c
a2_right : Sum.inr q0 ∈ List.map Sum.inr x.stop_state_list
⊢ ∃ stop_state_list,
    { start_state := x.start_state, symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
      q0 ∈ stop_state_list
Tactic:
simp only [← a3_right_right_left]
State after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_1
a3_left : x ∈ M_1.symbol_arrow_list
a3_right_left : x.start_state = p0
a3_right_right_left : x.symbol = c
a2_right : Sum.inr q0 ∈ List.map Sum.inr x.stop_state_list
⊢ ∃ stop_state_list,
    { start_state := x.start_state, symbol := x.symbol, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
      q0 ∈ stop_state_list

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_1
a3_left : x ∈ M_1.symbol_arrow_list
a3_right_left : x.start_state = p0
a3_right_right_left : x.symbol = c
a2_right : Sum.inr q0 ∈ List.map Sum.inr x.stop_state_list
⊢ ∃ stop_state_list,
    { start_state := x.start_state, symbol := x.symbol, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
      q0 ∈ stop_state_list
Tactic:
simp at a2_right
State after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_1
a3_left : x ∈ M_1.symbol_arrow_list
a3_right_left : x.start_state = p0
a3_right_right_left : x.symbol = c
a2_right : q0 ∈ x.stop_state_list
⊢ ∃ stop_state_list,
    { start_state := x.start_state, symbol := x.symbol, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
      q0 ∈ stop_state_list

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_1
a3_left : x ∈ M_1.symbol_arrow_list
a3_right_left : x.start_state = p0
a3_right_right_left : x.symbol = c
a2_right : q0 ∈ x.stop_state_list
⊢ ∃ stop_state_list,
    { start_state := x.start_state, symbol := x.symbol, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
      q0 ∈ stop_state_list
Tactic:
apply Exists.intro x.stop_state_list
State after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_1
a3_left : x ∈ M_1.symbol_arrow_list
a3_right_left : x.start_state = p0
a3_right_right_left : x.symbol = c
a2_right : q0 ∈ x.stop_state_list
⊢ { start_state := x.start_state, symbol := x.symbol, stop_state_list := x.stop_state_list } ∈ M_1.symbol_arrow_list ∧
    q0 ∈ x.stop_state_list

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_1
a3_left : x ∈ M_1.symbol_arrow_list
a3_right_left : x.start_state = p0
a3_right_right_left : x.symbol = c
a2_right : q0 ∈ x.stop_state_list
⊢ { start_state := x.start_state, symbol := x.symbol, stop_state_list := x.stop_state_list } ∈ M_1.symbol_arrow_list ∧
    q0 ∈ x.stop_state_list
Tactic:
constructor
State after:
case left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_1
a3_left : x ∈ M_1.symbol_arrow_list
a3_right_left : x.start_state = p0
a3_right_right_left : x.symbol = c
a2_right : q0 ∈ x.stop_state_list
⊢ { start_state := x.start_state, symbol := x.symbol, stop_state_list := x.stop_state_list } ∈ M_1.symbol_arrow_list

case right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_1
a3_left : x ∈ M_1.symbol_arrow_list
a3_right_left : x.start_state = p0
a3_right_right_left : x.symbol = c
a2_right : q0 ∈ x.stop_state_list
⊢ q0 ∈ x.stop_state_list

State before:
case left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_1
a3_left : x ∈ M_1.symbol_arrow_list
a3_right_left : x.start_state = p0
a3_right_right_left : x.symbol = c
a2_right : q0 ∈ x.stop_state_list
⊢ { start_state := x.start_state, symbol := x.symbol, stop_state_list := x.stop_state_list } ∈ M_1.symbol_arrow_list
Tactic:
exact a3_left
State after:
no goals

State before:
case right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_1
a3_left : x ∈ M_1.symbol_arrow_list
a3_right_left : x.start_state = p0
a3_right_right_left : x.symbol = c
a2_right : q0 ∈ x.stop_state_list
⊢ q0 ∈ x.stop_state_list
Tactic:
exact a2_right
State after:
no goals

State before:
case mpr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
⊢ (∃ stop_state_list,
      { start_state := p0, symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
        q0 ∈ stop_state_list) →
    ∃ stop_state_list,
      (∃ a ∈ M_1.symbol_arrow_list,
          a.start_state = p0 ∧ a.symbol = c ∧ List.map Sum.inr a.stop_state_list = stop_state_list) ∧
        Sum.inr q0 ∈ stop_state_list
Tactic:
intro a1
State after:
case mpr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
a1 :
  ∃ stop_state_list,
    { start_state := p0, symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
      q0 ∈ stop_state_list
⊢ ∃ stop_state_list,
    (∃ a ∈ M_1.symbol_arrow_list,
        a.start_state = p0 ∧ a.symbol = c ∧ List.map Sum.inr a.stop_state_list = stop_state_list) ∧
      Sum.inr q0 ∈ stop_state_list

State before:
case mpr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
a1 :
  ∃ stop_state_list,
    { start_state := p0, symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
      q0 ∈ stop_state_list
⊢ ∃ stop_state_list,
    (∃ a ∈ M_1.symbol_arrow_list,
        a.start_state = p0 ∧ a.symbol = c ∧ List.map Sum.inr a.stop_state_list = stop_state_list) ∧
      Sum.inr q0 ∈ stop_state_list
Tactic:
cases a1
State after:
case mpr.intro
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
w✝ : List σ_1
h✝ : { start_state := p0, symbol := c, stop_state_list := w✝ } ∈ M_1.symbol_arrow_list ∧ q0 ∈ w✝
⊢ ∃ stop_state_list,
    (∃ a ∈ M_1.symbol_arrow_list,
        a.start_state = p0 ∧ a.symbol = c ∧ List.map Sum.inr a.stop_state_list = stop_state_list) ∧
      Sum.inr q0 ∈ stop_state_list

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List σ_1
a2 : { start_state := p0, symbol := c, stop_state_list := xs } ∈ M_1.symbol_arrow_list ∧ q0 ∈ xs
⊢ ∃ stop_state_list,
    (∃ a ∈ M_1.symbol_arrow_list,
        a.start_state = p0 ∧ a.symbol = c ∧ List.map Sum.inr a.stop_state_list = stop_state_list) ∧
      Sum.inr q0 ∈ stop_state_list
Tactic:
cases a2
State after:
case intro
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List σ_1
left✝ : { start_state := p0, symbol := c, stop_state_list := xs } ∈ M_1.symbol_arrow_list
right✝ : q0 ∈ xs
⊢ ∃ stop_state_list,
    (∃ a ∈ M_1.symbol_arrow_list,
        a.start_state = p0 ∧ a.symbol = c ∧ List.map Sum.inr a.stop_state_list = stop_state_list) ∧
      Sum.inr q0 ∈ stop_state_list

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List σ_1
a2_left : { start_state := p0, symbol := c, stop_state_list := xs } ∈ M_1.symbol_arrow_list
a2_right : q0 ∈ xs
⊢ ∃ stop_state_list,
    (∃ a ∈ M_1.symbol_arrow_list,
        a.start_state = p0 ∧ a.symbol = c ∧ List.map Sum.inr a.stop_state_list = stop_state_list) ∧
      Sum.inr q0 ∈ stop_state_list
Tactic:
apply Exists.intro (xs.map Sum.inr)
State after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List σ_1
a2_left : { start_state := p0, symbol := c, stop_state_list := xs } ∈ M_1.symbol_arrow_list
a2_right : q0 ∈ xs
⊢ (∃ a ∈ M_1.symbol_arrow_list,
      a.start_state = p0 ∧ a.symbol = c ∧ List.map Sum.inr a.stop_state_list = List.map Sum.inr xs) ∧
    Sum.inr q0 ∈ List.map Sum.inr xs

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List σ_1
a2_left : { start_state := p0, symbol := c, stop_state_list := xs } ∈ M_1.symbol_arrow_list
a2_right : q0 ∈ xs
⊢ (∃ a ∈ M_1.symbol_arrow_list,
      a.start_state = p0 ∧ a.symbol = c ∧ List.map Sum.inr a.stop_state_list = List.map Sum.inr xs) ∧
    Sum.inr q0 ∈ List.map Sum.inr xs
Tactic:
constructor
State after:
case left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List σ_1
a2_left : { start_state := p0, symbol := c, stop_state_list := xs } ∈ M_1.symbol_arrow_list
a2_right : q0 ∈ xs
⊢ ∃ a ∈ M_1.symbol_arrow_list,
    a.start_state = p0 ∧ a.symbol = c ∧ List.map Sum.inr a.stop_state_list = List.map Sum.inr xs

case right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List σ_1
a2_left : { start_state := p0, symbol := c, stop_state_list := xs } ∈ M_1.symbol_arrow_list
a2_right : q0 ∈ xs
⊢ Sum.inr q0 ∈ List.map Sum.inr xs

State before:
case left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List σ_1
a2_left : { start_state := p0, symbol := c, stop_state_list := xs } ∈ M_1.symbol_arrow_list
a2_right : q0 ∈ xs
⊢ ∃ a ∈ M_1.symbol_arrow_list,
    a.start_state = p0 ∧ a.symbol = c ∧ List.map Sum.inr a.stop_state_list = List.map Sum.inr xs
Tactic:
apply Exists.intro { start_state := p0, symbol := c, stop_state_list := xs }
State after:
case left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List σ_1
a2_left : { start_state := p0, symbol := c, stop_state_list := xs } ∈ M_1.symbol_arrow_list
a2_right : q0 ∈ xs
⊢ { start_state := p0, symbol := c, stop_state_list := xs } ∈ M_1.symbol_arrow_list ∧
    { start_state := p0, symbol := c, stop_state_list := xs }.start_state = p0 ∧
      { start_state := p0, symbol := c, stop_state_list := xs }.symbol = c ∧
        List.map Sum.inr { start_state := p0, symbol := c, stop_state_list := xs }.stop_state_list = List.map Sum.inr xs

State before:
case left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List σ_1
a2_left : { start_state := p0, symbol := c, stop_state_list := xs } ∈ M_1.symbol_arrow_list
a2_right : q0 ∈ xs
⊢ { start_state := p0, symbol := c, stop_state_list := xs } ∈ M_1.symbol_arrow_list ∧
    { start_state := p0, symbol := c, stop_state_list := xs }.start_state = p0 ∧
      { start_state := p0, symbol := c, stop_state_list := xs }.symbol = c ∧
        List.map Sum.inr { start_state := p0, symbol := c, stop_state_list := xs }.stop_state_list = List.map Sum.inr xs
Tactic:
simp
State after:
case left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List σ_1
a2_left : { start_state := p0, symbol := c, stop_state_list := xs } ∈ M_1.symbol_arrow_list
a2_right : q0 ∈ xs
⊢ { start_state := p0, symbol := c, stop_state_list := xs } ∈ M_1.symbol_arrow_list

State before:
case left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List σ_1
a2_left : { start_state := p0, symbol := c, stop_state_list := xs } ∈ M_1.symbol_arrow_list
a2_right : q0 ∈ xs
⊢ { start_state := p0, symbol := c, stop_state_list := xs } ∈ M_1.symbol_arrow_list
Tactic:
exact a2_left
State after:
no goals

State before:
case right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List σ_1
a2_left : { start_state := p0, symbol := c, stop_state_list := xs } ∈ M_1.symbol_arrow_list
a2_right : q0 ∈ xs
⊢ Sum.inr q0 ∈ List.map Sum.inr xs
Tactic:
simp
State after:
case right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List σ_1
a2_left : { start_state := p0, symbol := c, stop_state_list := xs } ∈ M_1.symbol_arrow_list
a2_right : q0 ∈ xs
⊢ q0 ∈ xs

State before:
case right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
xs : List σ_1
a2_left : { start_state := p0, symbol := c, stop_state_list := xs } ∈ M_1.symbol_arrow_list
a2_right : q0 ∈ xs
⊢ q0 ∈ xs
Tactic:
exact a2_right
State after:
no goals

State before:
case right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
⊢ ((fun start_state stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, stop_state_list := 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 })
                  M_1.epsilon_arrow_list ∧
            stop_state ∈ stop_state_list) =
      fun p q =>
      match (p, q) with
      | (Sum.inl p', 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 p', Sum.inr q') =>
        ∃ stop_state_list,
          { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
      | x => False) ∧
    ((fun state => state ∈ List.map Sum.inl M_0.starting_state_list ++ List.map Sum.inr M_1.starting_state_list) =
        fun p =>
        match p with
        | Sum.inl p' => p' ∈ M_0.starting_state_list
        | Sum.inr p' => p' ∈ M_1.starting_state_list) ∧
      (fun state => state ∈ List.map Sum.inl M_0.accepting_state_list ++ List.map Sum.inr M_1.accepting_state_list) =
        fun p =>
        match p with
        | Sum.inl p' => p' ∈ M_0.accepting_state_list
        | Sum.inr p' => p' ∈ M_1.accepting_state_list
Tactic:
constructor
State after:
case right.left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
⊢ (fun start_state stop_state =>
      ∃ stop_state_list,
        { start_state := start_state, stop_state_list := 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 })
                M_1.epsilon_arrow_list ∧
          stop_state ∈ stop_state_list) =
    fun p q =>
    match (p, q) with
    | (Sum.inl p', 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 p', Sum.inr q') =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | x => False

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

State before:
case right.left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
⊢ (fun start_state stop_state =>
      ∃ stop_state_list,
        { start_state := start_state, stop_state_list := 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 })
                M_1.epsilon_arrow_list ∧
          stop_state ∈ stop_state_list) =
    fun p q =>
    match (p, q) with
    | (Sum.inl p', 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 p', Sum.inr q') =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | x => False
Tactic:
funext p q
State after:
case right.left.h.h
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p q : σ_0 ⊕ σ_1
⊢ (∃ stop_state_list,
      { start_state := p, stop_state_list := 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 })
              M_1.epsilon_arrow_list ∧
        q ∈ stop_state_list) =
    match (p, q) with
    | (Sum.inl p', 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 p', Sum.inr q') =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | x => False

State before:
case right.left.h.h
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p q : σ_0 ⊕ σ_1
⊢ (∃ stop_state_list,
      { start_state := p, stop_state_list := 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 })
              M_1.epsilon_arrow_list ∧
        q ∈ stop_state_list) =
    match (p, q) with
    | (Sum.inl p', 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 p', Sum.inr q') =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | x => False
Tactic:
cases p
State after:
case right.left.h.h.inl
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
q : σ_0 ⊕ σ_1
val✝ : σ_0
⊢ (∃ stop_state_list,
      { start_state := Sum.inl val✝, stop_state_list := 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 })
              M_1.epsilon_arrow_list ∧
        q ∈ stop_state_list) =
    match (Sum.inl val✝, q) with
    | (Sum.inl p', 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 p', Sum.inr q') =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | x => False

case right.left.h.h.inr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
q : σ_0 ⊕ σ_1
val✝ : σ_1
⊢ (∃ stop_state_list,
      { start_state := Sum.inr val✝, stop_state_list := 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 })
              M_1.epsilon_arrow_list ∧
        q ∈ stop_state_list) =
    match (Sum.inr val✝, q) with
    | (Sum.inl p', 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 p', Sum.inr q') =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | x => False

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
q : σ_0 ⊕ σ_1
p_0 : σ_0
⊢ (∃ stop_state_list,
      { start_state := Sum.inl p_0, stop_state_list := 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 })
              M_1.epsilon_arrow_list ∧
        q ∈ stop_state_list) =
    match (Sum.inl p_0, q) with
    | (Sum.inl p', 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 p', Sum.inr q') =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_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 val✝ : σ_0
⊢ (∃ stop_state_list,
      { start_state := Sum.inl p_0, stop_state_list := 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 })
              M_1.epsilon_arrow_list ∧
        Sum.inl val✝ ∈ stop_state_list) =
    match (Sum.inl p_0, Sum.inl val✝) with
    | (Sum.inl p', 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 p', Sum.inr q') =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | x => False

case inr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0
val✝ : σ_1
⊢ (∃ stop_state_list,
      { start_state := Sum.inl p_0, stop_state_list := 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 })
              M_1.epsilon_arrow_list ∧
        Sum.inr val✝ ∈ stop_state_list) =
    match (Sum.inl p_0, Sum.inr val✝) with
    | (Sum.inl p', 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 p', Sum.inr q') =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | x => False

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,
      { start_state := Sum.inl p_0, stop_state_list := 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 })
              M_1.epsilon_arrow_list ∧
        Sum.inr q_0 ∈ stop_state_list) =
    match (Sum.inl p_0, Sum.inr q_0) with
    | (Sum.inl p', 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 p', Sum.inr q') =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | x => False
Tactic:
case _ q_0 =>
  simp
  intro xs x _ _ 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 : σ_0
⊢ (∃ stop_state_list,
      { start_state := Sum.inl p_0, stop_state_list := 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 })
              M_1.epsilon_arrow_list ∧
        Sum.inl q_0 ∈ stop_state_list) =
    match (Sum.inl p_0, Sum.inl q_0) with
    | (Sum.inl p', 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 p', Sum.inr q') =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_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 : σ_0
⊢ (∃ stop_state_list,
      (∃ a ∈ M_0.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inl a.stop_state_list = stop_state_list) ∧
        Sum.inl q_0 ∈ stop_state_list) ↔
    ∃ stop_state_list,
      { start_state := p_0, stop_state_list := stop_state_list } ∈ M_0.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 : σ_0
⊢ (∃ stop_state_list,
      (∃ a ∈ M_0.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inl a.stop_state_list = stop_state_list) ∧
        Sum.inl q_0 ∈ stop_state_list) ↔
    ∃ stop_state_list,
      { start_state := p_0, stop_state_list := stop_state_list } ∈ M_0.epsilon_arrow_list ∧ q_0 ∈ stop_state_list
Tactic:
constructor
State after:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_0
⊢ (∃ stop_state_list,
      (∃ a ∈ M_0.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inl a.stop_state_list = stop_state_list) ∧
        Sum.inl q_0 ∈ stop_state_list) →
    ∃ stop_state_list,
      { start_state := p_0, stop_state_list := stop_state_list } ∈ M_0.epsilon_arrow_list ∧ q_0 ∈ stop_state_list

case mpr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_0
⊢ (∃ stop_state_list,
      { start_state := p_0, stop_state_list := stop_state_list } ∈ M_0.epsilon_arrow_list ∧ q_0 ∈ stop_state_list) →
    ∃ stop_state_list,
      (∃ a ∈ M_0.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inl a.stop_state_list = stop_state_list) ∧
        Sum.inl q_0 ∈ stop_state_list

State before:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_0
⊢ (∃ stop_state_list,
      (∃ a ∈ M_0.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inl a.stop_state_list = stop_state_list) ∧
        Sum.inl q_0 ∈ stop_state_list) →
    ∃ stop_state_list,
      { start_state := p_0, stop_state_list := stop_state_list } ∈ M_0.epsilon_arrow_list ∧ q_0 ∈ stop_state_list
Tactic:
intro a1
State after:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_0
a1 :
  ∃ stop_state_list,
    (∃ a ∈ M_0.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inl a.stop_state_list = stop_state_list) ∧
      Sum.inl q_0 ∈ stop_state_list
⊢ ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_0.epsilon_arrow_list ∧ q_0 ∈ stop_state_list

State before:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_0
a1 :
  ∃ stop_state_list,
    (∃ a ∈ M_0.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inl a.stop_state_list = stop_state_list) ∧
      Sum.inl q_0 ∈ stop_state_list
⊢ ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_0.epsilon_arrow_list ∧ q_0 ∈ stop_state_list
Tactic:
cases a1
State after:
case mp.intro
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_0
w✝ : List (σ_0 ⊕ σ_1)
h✝ : (∃ a ∈ M_0.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inl a.stop_state_list = w✝) ∧ Sum.inl q_0 ∈ w✝
⊢ ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_0.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 : σ_0
xs : List (σ_0 ⊕ σ_1)
a2 : (∃ a ∈ M_0.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inl a.stop_state_list = xs) ∧ Sum.inl q_0 ∈ xs
⊢ ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_0.epsilon_arrow_list ∧ q_0 ∈ stop_state_list
Tactic:
cases a2
State after:
case intro
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
left✝ : ∃ a ∈ M_0.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inl a.stop_state_list = xs
right✝ : Sum.inl q_0 ∈ xs
⊢ ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_0.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 : σ_0
xs : List (σ_0 ⊕ σ_1)
a2_left : ∃ a ∈ M_0.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inl a.stop_state_list = xs
a2_right : Sum.inl q_0 ∈ xs
⊢ ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_0.epsilon_arrow_list ∧ q_0 ∈ stop_state_list
Tactic:
cases a2_left
State after:
case intro
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
a2_right : Sum.inl q_0 ∈ xs
w✝ : EpsilonArrow σ_0
h✝ : w✝ ∈ M_0.epsilon_arrow_list ∧ w✝.start_state = p_0 ∧ List.map Sum.inl w✝.stop_state_list = xs
⊢ ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_0.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 : σ_0
xs : List (σ_0 ⊕ σ_1)
a2_right : Sum.inl q_0 ∈ xs
x : EpsilonArrow σ_0
a3 : x ∈ M_0.epsilon_arrow_list ∧ x.start_state = p_0 ∧ List.map Sum.inl x.stop_state_list = xs
⊢ ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_0.epsilon_arrow_list ∧ q_0 ∈ stop_state_list
Tactic:
cases a3
State after:
case intro
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
a2_right : Sum.inl q_0 ∈ xs
x : EpsilonArrow σ_0
left✝ : x ∈ M_0.epsilon_arrow_list
right✝ : x.start_state = p_0 ∧ List.map Sum.inl x.stop_state_list = xs
⊢ ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_0.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 : σ_0
xs : List (σ_0 ⊕ σ_1)
a2_right : Sum.inl q_0 ∈ xs
x : EpsilonArrow σ_0
a3_left : x ∈ M_0.epsilon_arrow_list
a3_right : x.start_state = p_0 ∧ List.map Sum.inl x.stop_state_list = xs
⊢ ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_0.epsilon_arrow_list ∧ q_0 ∈ stop_state_list
Tactic:
cases a3_right
State after:
case intro
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
a2_right : Sum.inl q_0 ∈ xs
x : EpsilonArrow σ_0
a3_left : x ∈ M_0.epsilon_arrow_list
left✝ : x.start_state = p_0
right✝ : List.map Sum.inl x.stop_state_list = xs
⊢ ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_0.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 : σ_0
xs : List (σ_0 ⊕ σ_1)
a2_right : Sum.inl q_0 ∈ xs
x : EpsilonArrow σ_0
a3_left : x ∈ M_0.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a3_right_right : List.map Sum.inl x.stop_state_list = xs
⊢ ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_0.epsilon_arrow_list ∧ q_0 ∈ stop_state_list
Tactic:
simp only [← a3_right_right] at a2_right
State after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_0
a3_left : x ∈ M_0.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a3_right_right : List.map Sum.inl x.stop_state_list = xs
a2_right : Sum.inl q_0 ∈ List.map Sum.inl x.stop_state_list
⊢ ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_0.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 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_0
a3_left : x ∈ M_0.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a3_right_right : List.map Sum.inl x.stop_state_list = xs
a2_right : Sum.inl q_0 ∈ List.map Sum.inl x.stop_state_list
⊢ ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_0.epsilon_arrow_list ∧ q_0 ∈ stop_state_list
Tactic:
clear a3_right_right
State after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_0
a3_left : x ∈ M_0.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a2_right : Sum.inl q_0 ∈ List.map Sum.inl x.stop_state_list
⊢ ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_0.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 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_0
a3_left : x ∈ M_0.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a2_right : Sum.inl q_0 ∈ List.map Sum.inl x.stop_state_list
⊢ ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_0.epsilon_arrow_list ∧ q_0 ∈ stop_state_list
Tactic:
simp at a2_right
State after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_0
a3_left : x ∈ M_0.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a2_right : q_0 ∈ x.stop_state_list
⊢ ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_0.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 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_0
a3_left : x ∈ M_0.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a2_right : q_0 ∈ x.stop_state_list
⊢ ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_0.epsilon_arrow_list ∧ q_0 ∈ stop_state_list
Tactic:
apply Exists.intro x.stop_state_list
State after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_0
a3_left : x ∈ M_0.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a2_right : q_0 ∈ x.stop_state_list
⊢ { start_state := p_0, stop_state_list := x.stop_state_list } ∈ M_0.epsilon_arrow_list ∧ q_0 ∈ x.stop_state_list

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_0
a3_left : x ∈ M_0.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a2_right : q_0 ∈ x.stop_state_list
⊢ { start_state := p_0, stop_state_list := x.stop_state_list } ∈ M_0.epsilon_arrow_list ∧ q_0 ∈ x.stop_state_list
Tactic:
simp only [← a3_right_left]
State after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_0
a3_left : x ∈ M_0.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a2_right : q_0 ∈ x.stop_state_list
⊢ { start_state := x.start_state, stop_state_list := x.stop_state_list } ∈ M_0.epsilon_arrow_list ∧
    q_0 ∈ x.stop_state_list

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_0
a3_left : x ∈ M_0.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a2_right : q_0 ∈ x.stop_state_list
⊢ { start_state := x.start_state, stop_state_list := x.stop_state_list } ∈ M_0.epsilon_arrow_list ∧
    q_0 ∈ x.stop_state_list
Tactic:
constructor
State after:
case left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_0
a3_left : x ∈ M_0.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a2_right : q_0 ∈ x.stop_state_list
⊢ { start_state := x.start_state, stop_state_list := x.stop_state_list } ∈ M_0.epsilon_arrow_list

case right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_0
a3_left : x ∈ M_0.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a2_right : q_0 ∈ x.stop_state_list
⊢ q_0 ∈ x.stop_state_list

State before:
case left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_0
a3_left : x ∈ M_0.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a2_right : q_0 ∈ x.stop_state_list
⊢ { start_state := x.start_state, stop_state_list := x.stop_state_list } ∈ M_0.epsilon_arrow_list
Tactic:
exact a3_left
State after:
no goals

State before:
case right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_0
a3_left : x ∈ M_0.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a2_right : q_0 ∈ x.stop_state_list
⊢ q_0 ∈ x.stop_state_list
Tactic:
exact a2_right
State after:
no goals

State before:
case mpr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_0
⊢ (∃ stop_state_list,
      { start_state := p_0, stop_state_list := stop_state_list } ∈ M_0.epsilon_arrow_list ∧ q_0 ∈ stop_state_list) →
    ∃ stop_state_list,
      (∃ a ∈ M_0.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inl a.stop_state_list = stop_state_list) ∧
        Sum.inl q_0 ∈ stop_state_list
Tactic:
intro a1
State after:
case mpr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_0
a1 :
  ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_0.epsilon_arrow_list ∧ q_0 ∈ stop_state_list
⊢ ∃ stop_state_list,
    (∃ a ∈ M_0.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inl a.stop_state_list = stop_state_list) ∧
      Sum.inl q_0 ∈ stop_state_list

State before:
case mpr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_0
a1 :
  ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_0.epsilon_arrow_list ∧ q_0 ∈ stop_state_list
⊢ ∃ stop_state_list,
    (∃ a ∈ M_0.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inl a.stop_state_list = stop_state_list) ∧
      Sum.inl q_0 ∈ stop_state_list
Tactic:
cases a1
State after:
case mpr.intro
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_0
w✝ : List σ_0
h✝ : { start_state := p_0, stop_state_list := w✝ } ∈ M_0.epsilon_arrow_list ∧ q_0 ∈ w✝
⊢ ∃ stop_state_list,
    (∃ a ∈ M_0.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inl a.stop_state_list = stop_state_list) ∧
      Sum.inl 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 : σ_0
xs : List σ_0
a2 : { start_state := p_0, stop_state_list := xs } ∈ M_0.epsilon_arrow_list ∧ q_0 ∈ xs
⊢ ∃ stop_state_list,
    (∃ a ∈ M_0.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inl a.stop_state_list = stop_state_list) ∧
      Sum.inl q_0 ∈ stop_state_list
Tactic:
cases a2
State after:
case intro
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_0
xs : List σ_0
left✝ : { start_state := p_0, stop_state_list := xs } ∈ M_0.epsilon_arrow_list
right✝ : q_0 ∈ xs
⊢ ∃ stop_state_list,
    (∃ a ∈ M_0.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inl a.stop_state_list = stop_state_list) ∧
      Sum.inl 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 : σ_0
xs : List σ_0
a2_left : { start_state := p_0, stop_state_list := xs } ∈ M_0.epsilon_arrow_list
a2_right : q_0 ∈ xs
⊢ ∃ stop_state_list,
    (∃ a ∈ M_0.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inl a.stop_state_list = stop_state_list) ∧
      Sum.inl q_0 ∈ stop_state_list
Tactic:
apply Exists.intro (xs.map Sum.inl)
State after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_0
xs : List σ_0
a2_left : { start_state := p_0, stop_state_list := xs } ∈ M_0.epsilon_arrow_list
a2_right : q_0 ∈ xs
⊢ (∃ a ∈ M_0.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inl a.stop_state_list = List.map Sum.inl xs) ∧
    Sum.inl q_0 ∈ List.map Sum.inl xs

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_0
xs : List σ_0
a2_left : { start_state := p_0, stop_state_list := xs } ∈ M_0.epsilon_arrow_list
a2_right : q_0 ∈ xs
⊢ (∃ a ∈ M_0.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inl a.stop_state_list = List.map Sum.inl xs) ∧
    Sum.inl q_0 ∈ List.map Sum.inl xs
Tactic:
constructor
State after:
case left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_0
xs : List σ_0
a2_left : { start_state := p_0, stop_state_list := xs } ∈ M_0.epsilon_arrow_list
a2_right : q_0 ∈ xs
⊢ ∃ a ∈ M_0.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inl a.stop_state_list = List.map Sum.inl xs

case right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_0
xs : List σ_0
a2_left : { start_state := p_0, stop_state_list := xs } ∈ M_0.epsilon_arrow_list
a2_right : q_0 ∈ xs
⊢ Sum.inl q_0 ∈ List.map Sum.inl xs

State before:
case left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_0
xs : List σ_0
a2_left : { start_state := p_0, stop_state_list := xs } ∈ M_0.epsilon_arrow_list
a2_right : q_0 ∈ xs
⊢ ∃ a ∈ M_0.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inl a.stop_state_list = List.map Sum.inl xs
Tactic:
apply Exists.intro { start_state := p_0, stop_state_list := xs }
State after:
case left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_0
xs : List σ_0
a2_left : { start_state := p_0, stop_state_list := xs } ∈ M_0.epsilon_arrow_list
a2_right : q_0 ∈ xs
⊢ { start_state := p_0, stop_state_list := xs } ∈ M_0.epsilon_arrow_list ∧
    { start_state := p_0, stop_state_list := xs }.start_state = p_0 ∧
      List.map Sum.inl { start_state := p_0, stop_state_list := xs }.stop_state_list = List.map Sum.inl xs

State before:
case left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_0
xs : List σ_0
a2_left : { start_state := p_0, stop_state_list := xs } ∈ M_0.epsilon_arrow_list
a2_right : q_0 ∈ xs
⊢ { start_state := p_0, stop_state_list := xs } ∈ M_0.epsilon_arrow_list ∧
    { start_state := p_0, stop_state_list := xs }.start_state = p_0 ∧
      List.map Sum.inl { start_state := p_0, stop_state_list := xs }.stop_state_list = List.map Sum.inl xs
Tactic:
simp
State after:
case left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_0
xs : List σ_0
a2_left : { start_state := p_0, stop_state_list := xs } ∈ M_0.epsilon_arrow_list
a2_right : q_0 ∈ xs
⊢ { start_state := p_0, stop_state_list := xs } ∈ M_0.epsilon_arrow_list

State before:
case left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_0
xs : List σ_0
a2_left : { start_state := p_0, stop_state_list := xs } ∈ M_0.epsilon_arrow_list
a2_right : q_0 ∈ xs
⊢ { start_state := p_0, stop_state_list := xs } ∈ M_0.epsilon_arrow_list
Tactic:
exact a2_left
State after:
no goals

State before:
case right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_0
xs : List σ_0
a2_left : { start_state := p_0, stop_state_list := xs } ∈ M_0.epsilon_arrow_list
a2_right : q_0 ∈ xs
⊢ Sum.inl q_0 ∈ List.map Sum.inl xs
Tactic:
simp
State after:
case right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_0
xs : List σ_0
a2_left : { start_state := p_0, stop_state_list := xs } ∈ M_0.epsilon_arrow_list
a2_right : q_0 ∈ xs
⊢ q_0 ∈ xs

State before:
case right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_0
xs : List σ_0
a2_left : { start_state := p_0, stop_state_list := xs } ∈ M_0.epsilon_arrow_list
a2_right : q_0 ∈ xs
⊢ q_0 ∈ xs
Tactic:
exact a2_right
State after:
no goals

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,
      { start_state := Sum.inl p_0, stop_state_list := 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 })
              M_1.epsilon_arrow_list ∧
        Sum.inr q_0 ∈ stop_state_list) =
    match (Sum.inl p_0, Sum.inr q_0) with
    | (Sum.inl p', 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 p', Sum.inr q') =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | x => False
Tactic:
simp
State after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0
q_0 : σ_1
⊢ ∀ (x : List (σ_0 ⊕ σ_1)),
    ∀ x_1 ∈ M_0.epsilon_arrow_list, x_1.start_state = p_0 → List.map Sum.inl x_1.stop_state_list = x → Sum.inr q_0 ∉ x

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

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0
q_0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_0
a✝¹ : x ∈ M_0.epsilon_arrow_list
a✝ : x.start_state = p_0
a3 : List.map Sum.inl x.stop_state_list = xs
⊢ Sum.inr 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 : σ_0
q_0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_0
a✝¹ : x ∈ M_0.epsilon_arrow_list
a✝ : x.start_state = p_0
a3 : List.map Sum.inl x.stop_state_list = xs
⊢ Sum.inr q_0 ∉ List.map Sum.inl x.stop_state_list

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0
q_0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_0
a✝¹ : x ∈ M_0.epsilon_arrow_list
a✝ : x.start_state = p_0
a3 : List.map Sum.inl x.stop_state_list = xs
⊢ Sum.inr q_0 ∉ List.map Sum.inl 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
q : σ_0 ⊕ σ_1
p_0 : σ_1
⊢ (∃ stop_state_list,
      { start_state := Sum.inr p_0, stop_state_list := 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 })
              M_1.epsilon_arrow_list ∧
        q ∈ stop_state_list) =
    match (Sum.inr p_0, q) with
    | (Sum.inl p', 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 p', Sum.inr q') =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_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✝ : σ_0
⊢ (∃ stop_state_list,
      { start_state := Sum.inr p_0, stop_state_list := 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 })
              M_1.epsilon_arrow_list ∧
        Sum.inl val✝ ∈ stop_state_list) =
    match (Sum.inr p_0, Sum.inl val✝) with
    | (Sum.inl p', 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 p', Sum.inr q') =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_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 p_0, stop_state_list := 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 })
              M_1.epsilon_arrow_list ∧
        Sum.inr val✝ ∈ stop_state_list) =
    match (Sum.inr p_0, Sum.inr val✝) with
    | (Sum.inl p', 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 p', Sum.inr q') =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_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 p_0, stop_state_list := 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 })
              M_1.epsilon_arrow_list ∧
        Sum.inl q_0 ∈ stop_state_list) =
    match (Sum.inr p_0, Sum.inl q_0) with
    | (Sum.inl p', 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 p', Sum.inr q') =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | x => False
Tactic:
case _ q_0 =>
  simp
  intro xs x _ _ 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
⊢ (∃ stop_state_list,
      { start_state := Sum.inr p_0, stop_state_list := 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 })
              M_1.epsilon_arrow_list ∧
        Sum.inl q_0 ∈ stop_state_list) =
    match (Sum.inr p_0, Sum.inl q_0) with
    | (Sum.inl p', 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 p', Sum.inr q') =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_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 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 : σ_0
⊢ ∀ (x : List (σ_0 ⊕ σ_1)),
    ∀ x_1 ∈ M_1.epsilon_arrow_list, x_1.start_state = p_0 → List.map Sum.inr x_1.stop_state_list = x → Sum.inl q_0 ∉ x
Tactic:
intro xs x _ _ 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
a✝¹ : x ∈ M_1.epsilon_arrow_list
a✝ : x.start_state = p_0
a3 : List.map 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 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a✝¹ : x ∈ M_1.epsilon_arrow_list
a✝ : x.start_state = p_0
a3 : List.map 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 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a✝¹ : x ∈ M_1.epsilon_arrow_list
a✝ : x.start_state = p_0
a3 : List.map Sum.inr x.stop_state_list = xs
⊢ Sum.inl q_0 ∉ List.map 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
a✝¹ : x ∈ M_1.epsilon_arrow_list
a✝ : x.start_state = p_0
a3 : List.map Sum.inr x.stop_state_list = xs
⊢ Sum.inl q_0 ∉ List.map 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 p_0, stop_state_list := 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 })
              M_1.epsilon_arrow_list ∧
        Sum.inr q_0 ∈ stop_state_list) =
    match (Sum.inr p_0, Sum.inr q_0) with
    | (Sum.inl p', 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 p', Sum.inr q') =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_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 a.stop_state_list = stop_state_list) ∧
        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 a.stop_state_list = stop_state_list) ∧
        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:
constructor
State after:
case mp
α : 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 a.stop_state_list = stop_state_list) ∧
        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

case mpr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
⊢ (∃ stop_state_list,
      { start_state := p_0, stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q_0 ∈ stop_state_list) →
    ∃ stop_state_list,
      (∃ a ∈ M_1.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inr a.stop_state_list = stop_state_list) ∧
        Sum.inr q_0 ∈ stop_state_list

State before:
case mp
α : 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 a.stop_state_list = stop_state_list) ∧
        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:
intro a1
State after:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
a1 :
  ∃ stop_state_list,
    (∃ a ∈ M_1.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inr a.stop_state_list = stop_state_list) ∧
      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:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
a1 :
  ∃ stop_state_list,
    (∃ a ∈ M_1.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inr a.stop_state_list = stop_state_list) ∧
      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:
cases a1
State after:
case mp.intro
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
w✝ : List (σ_0 ⊕ σ_1)
h✝ : (∃ a ∈ M_1.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inr a.stop_state_list = w✝) ∧ Sum.inr q_0 ∈ w✝
⊢ ∃ 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
xs : List (σ_0 ⊕ σ_1)
a2 : (∃ a ∈ M_1.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inr a.stop_state_list = xs) ∧ Sum.inr q_0 ∈ xs
⊢ ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q_0 ∈ stop_state_list
Tactic:
cases a2
State after:
case intro
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List (σ_0 ⊕ σ_1)
left✝ : ∃ a ∈ M_1.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inr a.stop_state_list = xs
right✝ : Sum.inr q_0 ∈ xs
⊢ ∃ 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
xs : List (σ_0 ⊕ σ_1)
a2_left : ∃ a ∈ M_1.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inr a.stop_state_list = xs
a2_right : Sum.inr q_0 ∈ xs
⊢ ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q_0 ∈ stop_state_list
Tactic:
cases a2_left
State after:
case intro
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List (σ_0 ⊕ σ_1)
a2_right : Sum.inr q_0 ∈ xs
w✝ : EpsilonArrow σ_1
h✝ : w✝ ∈ M_1.epsilon_arrow_list ∧ w✝.start_state = p_0 ∧ List.map Sum.inr w✝.stop_state_list = xs
⊢ ∃ 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
xs : List (σ_0 ⊕ σ_1)
a2_right : Sum.inr q_0 ∈ xs
x : EpsilonArrow σ_1
a3 : x ∈ M_1.epsilon_arrow_list ∧ x.start_state = p_0 ∧ List.map Sum.inr x.stop_state_list = xs
⊢ ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q_0 ∈ stop_state_list
Tactic:
cases a3
State after:
case intro
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List (σ_0 ⊕ σ_1)
a2_right : Sum.inr q_0 ∈ xs
x : EpsilonArrow σ_1
left✝ : x ∈ M_1.epsilon_arrow_list
right✝ : x.start_state = p_0 ∧ List.map Sum.inr x.stop_state_list = xs
⊢ ∃ 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
xs : List (σ_0 ⊕ σ_1)
a2_right : Sum.inr q_0 ∈ xs
x : EpsilonArrow σ_1
a3_left : x ∈ M_1.epsilon_arrow_list
a3_right : x.start_state = p_0 ∧ List.map Sum.inr x.stop_state_list = xs
⊢ ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q_0 ∈ stop_state_list
Tactic:
cases a3_right
State after:
case intro
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List (σ_0 ⊕ σ_1)
a2_right : Sum.inr q_0 ∈ xs
x : EpsilonArrow σ_1
a3_left : x ∈ M_1.epsilon_arrow_list
left✝ : x.start_state = p_0
right✝ : List.map Sum.inr x.stop_state_list = xs
⊢ ∃ 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
xs : List (σ_0 ⊕ σ_1)
a2_right : Sum.inr q_0 ∈ xs
x : EpsilonArrow σ_1
a3_left : x ∈ M_1.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a3_right_right : List.map Sum.inr x.stop_state_list = xs
⊢ ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q_0 ∈ stop_state_list
Tactic:
simp only [← a3_right_right] at a2_right
State after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a3_left : x ∈ M_1.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a3_right_right : List.map Sum.inr x.stop_state_list = xs
a2_right : Sum.inr q_0 ∈ List.map Sum.inr x.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
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a3_left : x ∈ M_1.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a3_right_right : List.map Sum.inr x.stop_state_list = xs
a2_right : Sum.inr q_0 ∈ List.map Sum.inr x.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:
clear a3_right_right
State after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a3_left : x ∈ M_1.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a2_right : Sum.inr q_0 ∈ List.map Sum.inr x.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
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a3_left : x ∈ M_1.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a2_right : Sum.inr q_0 ∈ List.map Sum.inr x.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:
simp at a2_right
State after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a3_left : x ∈ M_1.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a2_right : q_0 ∈ x.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
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a3_left : x ∈ M_1.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a2_right : q_0 ∈ x.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:
apply Exists.intro x.stop_state_list
State after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a3_left : x ∈ M_1.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a2_right : q_0 ∈ x.stop_state_list
⊢ { start_state := p_0, stop_state_list := x.stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q_0 ∈ x.stop_state_list

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a3_left : x ∈ M_1.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a2_right : q_0 ∈ x.stop_state_list
⊢ { start_state := p_0, stop_state_list := x.stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q_0 ∈ x.stop_state_list
Tactic:
simp only [← a3_right_left]
State after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a3_left : x ∈ M_1.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a2_right : q_0 ∈ x.stop_state_list
⊢ { start_state := x.start_state, stop_state_list := x.stop_state_list } ∈ M_1.epsilon_arrow_list ∧
    q_0 ∈ x.stop_state_list

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a3_left : x ∈ M_1.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a2_right : q_0 ∈ x.stop_state_list
⊢ { start_state := x.start_state, stop_state_list := x.stop_state_list } ∈ M_1.epsilon_arrow_list ∧
    q_0 ∈ x.stop_state_list
Tactic:
constructor
State after:
case left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a3_left : x ∈ M_1.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a2_right : q_0 ∈ x.stop_state_list
⊢ { start_state := x.start_state, stop_state_list := x.stop_state_list } ∈ M_1.epsilon_arrow_list

case right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a3_left : x ∈ M_1.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a2_right : q_0 ∈ x.stop_state_list
⊢ q_0 ∈ x.stop_state_list

State before:
case left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a3_left : x ∈ M_1.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a2_right : q_0 ∈ x.stop_state_list
⊢ { start_state := x.start_state, stop_state_list := x.stop_state_list } ∈ M_1.epsilon_arrow_list
Tactic:
exact a3_left
State after:
no goals

State before:
case right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a3_left : x ∈ M_1.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a2_right : q_0 ∈ x.stop_state_list
⊢ q_0 ∈ x.stop_state_list
Tactic:
exact a2_right
State after:
no goals

State before:
case mpr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
⊢ (∃ stop_state_list,
      { start_state := p_0, stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q_0 ∈ stop_state_list) →
    ∃ stop_state_list,
      (∃ a ∈ M_1.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inr a.stop_state_list = stop_state_list) ∧
        Sum.inr q_0 ∈ stop_state_list
Tactic:
intro a1
State after:
case mpr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
a1 :
  ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q_0 ∈ stop_state_list
⊢ ∃ stop_state_list,
    (∃ a ∈ M_1.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inr a.stop_state_list = stop_state_list) ∧
      Sum.inr q_0 ∈ stop_state_list

State before:
case mpr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
a1 :
  ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q_0 ∈ stop_state_list
⊢ ∃ stop_state_list,
    (∃ a ∈ M_1.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inr a.stop_state_list = stop_state_list) ∧
      Sum.inr q_0 ∈ stop_state_list
Tactic:
cases a1
State after:
case mpr.intro
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
w✝ : List σ_1
h✝ : { start_state := p_0, stop_state_list := w✝ } ∈ M_1.epsilon_arrow_list ∧ q_0 ∈ w✝
⊢ ∃ stop_state_list,
    (∃ a ∈ M_1.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inr a.stop_state_list = stop_state_list) ∧
      Sum.inr 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
xs : List σ_1
a2 : { start_state := p_0, stop_state_list := xs } ∈ M_1.epsilon_arrow_list ∧ q_0 ∈ xs
⊢ ∃ stop_state_list,
    (∃ a ∈ M_1.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inr a.stop_state_list = stop_state_list) ∧
      Sum.inr q_0 ∈ stop_state_list
Tactic:
cases a2
State after:
case intro
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List σ_1
left✝ : { start_state := p_0, stop_state_list := xs } ∈ M_1.epsilon_arrow_list
right✝ : q_0 ∈ xs
⊢ ∃ stop_state_list,
    (∃ a ∈ M_1.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inr a.stop_state_list = stop_state_list) ∧
      Sum.inr 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
xs : List σ_1
a2_left : { start_state := p_0, stop_state_list := xs } ∈ M_1.epsilon_arrow_list
a2_right : q_0 ∈ xs
⊢ ∃ stop_state_list,
    (∃ a ∈ M_1.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inr a.stop_state_list = stop_state_list) ∧
      Sum.inr q_0 ∈ stop_state_list
Tactic:
apply Exists.intro (xs.map Sum.inr)
State after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List σ_1
a2_left : { start_state := p_0, stop_state_list := xs } ∈ M_1.epsilon_arrow_list
a2_right : q_0 ∈ xs
⊢ (∃ a ∈ M_1.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inr a.stop_state_list = List.map Sum.inr xs) ∧
    Sum.inr q_0 ∈ List.map Sum.inr xs

State before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List σ_1
a2_left : { start_state := p_0, stop_state_list := xs } ∈ M_1.epsilon_arrow_list
a2_right : q_0 ∈ xs
⊢ (∃ a ∈ M_1.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inr a.stop_state_list = List.map Sum.inr xs) ∧
    Sum.inr q_0 ∈ List.map Sum.inr xs
Tactic:
constructor
State after:
case left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List σ_1
a2_left : { start_state := p_0, stop_state_list := xs } ∈ M_1.epsilon_arrow_list
a2_right : q_0 ∈ xs
⊢ ∃ a ∈ M_1.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inr a.stop_state_list = List.map Sum.inr xs

case right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List σ_1
a2_left : { start_state := p_0, stop_state_list := xs } ∈ M_1.epsilon_arrow_list
a2_right : q_0 ∈ xs
⊢ Sum.inr q_0 ∈ List.map Sum.inr xs

State before:
case left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List σ_1
a2_left : { start_state := p_0, stop_state_list := xs } ∈ M_1.epsilon_arrow_list
a2_right : q_0 ∈ xs
⊢ ∃ a ∈ M_1.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inr a.stop_state_list = List.map Sum.inr xs
Tactic:
apply Exists.intro { start_state := p_0, stop_state_list := xs }
State after:
case left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List σ_1
a2_left : { start_state := p_0, stop_state_list := xs } ∈ M_1.epsilon_arrow_list
a2_right : q_0 ∈ xs
⊢ { start_state := p_0, stop_state_list := xs } ∈ M_1.epsilon_arrow_list ∧
    { start_state := p_0, stop_state_list := xs }.start_state = p_0 ∧
      List.map Sum.inr { start_state := p_0, stop_state_list := xs }.stop_state_list = List.map Sum.inr xs

State before:
case left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List σ_1
a2_left : { start_state := p_0, stop_state_list := xs } ∈ M_1.epsilon_arrow_list
a2_right : q_0 ∈ xs
⊢ { start_state := p_0, stop_state_list := xs } ∈ M_1.epsilon_arrow_list ∧
    { start_state := p_0, stop_state_list := xs }.start_state = p_0 ∧
      List.map Sum.inr { start_state := p_0, stop_state_list := xs }.stop_state_list = List.map Sum.inr xs
Tactic:
simp
State after:
case left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List σ_1
a2_left : { start_state := p_0, stop_state_list := xs } ∈ M_1.epsilon_arrow_list
a2_right : q_0 ∈ xs
⊢ { start_state := p_0, stop_state_list := xs } ∈ M_1.epsilon_arrow_list

State before:
case left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List σ_1
a2_left : { start_state := p_0, stop_state_list := xs } ∈ M_1.epsilon_arrow_list
a2_right : q_0 ∈ xs
⊢ { start_state := p_0, stop_state_list := xs } ∈ M_1.epsilon_arrow_list
Tactic:
exact a2_left
State after:
no goals

State before:
case right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List σ_1
a2_left : { start_state := p_0, stop_state_list := xs } ∈ M_1.epsilon_arrow_list
a2_right : q_0 ∈ xs
⊢ Sum.inr q_0 ∈ List.map Sum.inr xs
Tactic:
simp
State after:
case right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List σ_1
a2_left : { start_state := p_0, stop_state_list := xs } ∈ M_1.epsilon_arrow_list
a2_right : q_0 ∈ xs
⊢ q_0 ∈ xs

State before:
case right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List σ_1
a2_left : { start_state := p_0, stop_state_list := xs } ∈ M_1.epsilon_arrow_list
a2_right : q_0 ∈ xs
⊢ q_0 ∈ xs
Tactic:
exact a2_right
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.inl M_0.starting_state_list ++ List.map Sum.inr M_1.starting_state_list) =
      fun p =>
      match p with
      | Sum.inl p' => p' ∈ M_0.starting_state_list
      | Sum.inr p' => p' ∈ M_1.starting_state_list) ∧
    (fun state => state ∈ List.map Sum.inl M_0.accepting_state_list ++ List.map Sum.inr M_1.accepting_state_list) =
      fun p =>
      match p with
      | Sum.inl p' => p' ∈ M_0.accepting_state_list
      | Sum.inr p' => p' ∈ M_1.accepting_state_list
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.inl M_0.starting_state_list ++ List.map Sum.inr M_1.starting_state_list) = fun p =>
    match p with
    | Sum.inl p' => p' ∈ M_0.starting_state_list
    | Sum.inr p' => p' ∈ M_1.starting_state_list

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

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.inl M_0.starting_state_list ++ List.map Sum.inr M_1.starting_state_list) = fun p =>
    match p with
    | Sum.inl p' => p' ∈ M_0.starting_state_list
    | Sum.inr p' => p' ∈ M_1.starting_state_list
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.inl M_0.starting_state_list ++ List.map Sum.inr M_1.starting_state_list) =
    match p with
    | Sum.inl p' => p' ∈ M_0.starting_state_list
    | Sum.inr p' => p' ∈ M_1.starting_state_list

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.inl M_0.starting_state_list ++ List.map Sum.inr M_1.starting_state_list) =
    match p with
    | Sum.inl p' => p' ∈ M_0.starting_state_list
    | Sum.inr p' => p' ∈ M_1.starting_state_list
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✝ : σ_0
⊢ (Sum.inl val✝ ∈ List.map Sum.inl M_0.starting_state_list ++ List.map Sum.inr M_1.starting_state_list) =
    match Sum.inl val✝ with
    | Sum.inl p' => p' ∈ M_0.starting_state_list
    | Sum.inr p' => p' ∈ M_1.starting_state_list

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

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

State before:
case right.right.left.h.inr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
val✝ : σ_1
⊢ (Sum.inr val✝ ∈ List.map Sum.inl M_0.starting_state_list ++ List.map Sum.inr M_1.starting_state_list) =
    match Sum.inr val✝ with
    | Sum.inl p' => p' ∈ M_0.starting_state_list
    | Sum.inr p' => p' ∈ M_1.starting_state_list
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.inl M_0.accepting_state_list ++ List.map Sum.inr M_1.accepting_state_list) =
    fun p =>
    match p with
    | Sum.inl p' => p' ∈ M_0.accepting_state_list
    | Sum.inr p' => p' ∈ M_1.accepting_state_list
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.inl M_0.accepting_state_list ++ List.map Sum.inr M_1.accepting_state_list) =
    match p with
    | Sum.inl p' => p' ∈ M_0.accepting_state_list
    | Sum.inr p' => p' ∈ M_1.accepting_state_list

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.inl M_0.accepting_state_list ++ List.map Sum.inr M_1.accepting_state_list) =
    match p with
    | Sum.inl p' => p' ∈ M_0.accepting_state_list
    | Sum.inr p' => p' ∈ M_1.accepting_state_list
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✝ : σ_0
⊢ (Sum.inl val✝ ∈ List.map Sum.inl M_0.accepting_state_list ++ List.map Sum.inr M_1.accepting_state_list) =
    match Sum.inl val✝ with
    | Sum.inl p' => p' ∈ M_0.accepting_state_list
    | Sum.inr p' => p' ∈ M_1.accepting_state_list

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

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

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