apply Exists.elim a2_right
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a e)
a2_right : ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α e) ∧ xs ++ a.join = w
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a e)
a2_right : ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α e) ∧ xs ++ a.join = w
⊢ ∀ (a_1 : List (List α)),
    (∀ r ∈ a_1, r ∈ RegExp.languageOf α e) ∧ xs ++ a_1.join = w →
      ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w