case zero =>
  simp only [RegExp.derivative]
  simp only [RegExp.languageOf]
  simp
α : Type
inst✝ : DecidableEq α
a : α
w : List α
⊢ w ∈ RegExp.languageOf α (RegExp.derivative a RegExp.zero) ↔ a :: w ∈ RegExp.languageOf α RegExp.zero
no goals