apply Exists.elim a1
case mpr
α : Type
inst✝ : DecidableEq α
a : α
r s : RegExp α
r_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a r) ↔ a :: w ∈ RegExp.languageOf α r
s_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a s) ↔ a :: w ∈ RegExp.languageOf α s
w : List α
c1 : r.is_nullable
a1 : ∃ r_1 ∈ RegExp.languageOf α r, ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = a :: w
⊢ ∃ r_1 ∈ RegExp.languageOf α (RegExp.derivative a r), ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = w
case mpr
α : Type
inst✝ : DecidableEq α
a : α
r s : RegExp α
r_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a r) ↔ a :: w ∈ RegExp.languageOf α r
s_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a s) ↔ a :: w ∈ RegExp.languageOf α s
w : List α
c1 : r.is_nullable
a1 : ∃ r_1 ∈ RegExp.languageOf α r, ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = a :: w
⊢ ∀ (a_1 : List α),
    (a_1 ∈ RegExp.languageOf α r ∧ ∃ s_1 ∈ RegExp.languageOf α s, a_1 ++ s_1 = a :: w) →
      ∃ r_1 ∈ RegExp.languageOf α (RegExp.derivative a r), ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = w