cases a3
α : 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)
ys : List (List α)
a3 : (∀ r ∈ ys, r ∈ RegExp.languageOf α e) ∧ xs ++ ys.join = w
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w
case intro
α : 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)
ys : List (List α)
left✝ : ∀ r ∈ ys, r ∈ RegExp.languageOf α e
right✝ : xs ++ ys.join = w
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w