simp only [RegExp.languageOf]
α : 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
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w : List α
⊢ w ∈
      {x |
        ∃ r ∈ RegExp.languageOf α (RegExp.derivative a e),
          ∃ s ∈ {l | ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = l}, r ++ s = x} ↔
    a :: w ∈ {l | ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = l}