simp only [RegExp.derivative]
α : 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.concat s)) ↔ a :: w ∈ RegExp.languageOf α (r.concat s)
α : 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 α
        (if r.is_nullable then (RegExp.derivative a r).concat s else r.delta.concat (RegExp.derivative a s)) ↔
    a :: w ∈ RegExp.languageOf α (r.concat s)