case union r s r_ih s_ih =>
  simp only [RegExp.languageOf] at r_ih
  simp only [RegExp.languageOf] at s_ih
  simp only [RegExp.languageOf]
  simp only [r_ih]
  simp only [s_ih]
  simp only [RegExp.is_nullable]
  ext cs
  simp
  tauto
α : Type
r s : RegExp α
r_ih :
  RegExp.languageOf α r.delta =
    if r.is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
s_ih :
  RegExp.languageOf α s.delta =
    if s.is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
⊢ RegExp.languageOf α (r.union s).delta =
    if (r.union s).is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
no goals