case char b =>
  simp only [RegExp.derivative]
  split_ifs
  case pos c1 =>
    simp only [c1]
    simp only [RegExp.languageOf]
    simp
  case neg c1 =>
    simp only [RegExp.languageOf]
    simp
    intro a1
    contradiction
α : Type
inst✝ : DecidableEq α
a b : α
w : List α
⊢ w ∈ RegExp.languageOf α (RegExp.derivative a (RegExp.char b)) ↔ a :: w ∈ RegExp.languageOf α (RegExp.char b)
no goals