case _ a3_left a3_right =>
  cases a3_left
  case _ a3_left_left a3_left_right =>
    simp only [a2_left_left]
    simp only [a3_left_left]
    simp only [a2_left_right] at a3_right
    simp only [a3_left_right] at a3_right
    simp at a3_right
    tauto
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs xs : List α
a2_left_left : r.is_nullable
a2_left_right : xs = []
ys : List α
a3_left : s.is_nullable ∧ ys = []
a3_right : xs ++ ys = cs
⊢ (r.is_nullable ∧ s.is_nullable) ∧ cs = []
no goals