simp only [RegExp.derivative]
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w : List α
⊢ w ∈ RegExp.languageOf α (RegExp.derivative a e.closure) ↔ a :: w ∈ RegExp.languageOf α e.closure
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w : List α
⊢ w ∈ RegExp.languageOf α ((RegExp.derivative a e).concat e.closure) ↔ a :: w ∈ RegExp.languageOf α e.closure