apply Exists.intro ys
case right
α : 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
xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a r)
ys : List α
a3_left : ys ∈ RegExp.languageOf α s
a3_right : xs ++ ys = w
⊢ ∃ s_1 ∈ RegExp.languageOf α s, a :: xs ++ s_1 = a :: w
case right
α : 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
xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a r)
ys : List α
a3_left : ys ∈ RegExp.languageOf α s
a3_right : xs ++ ys = w
⊢ ys ∈ RegExp.languageOf α s ∧ a :: xs ++ ys = a :: w