case union r s r_ih s_ih =>
  simp only [RegExp.derivative]
  simp only [RegExp.languageOf]
  specialize r_ih w
  specialize s_ih w
  simp
  tauto
α : Type
inst✝ : DecidableEq α
a : α
r s : RegExp α
r_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a r) ↔ a :: w ∈ RegExp.languageOf α r
s_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a s) ↔ a :: w ∈ RegExp.languageOf α s
w : List α
⊢ w ∈ RegExp.languageOf α (RegExp.derivative a (r.union s)) ↔ a :: w ∈ RegExp.languageOf α (r.union s)
no goals