Is Regular mul

@[simp]theorem IsRegular.mul {l1 l2 : Language Symbol}    (h1 : l1.IsRegular) (h2 : l2.IsRegular) : (l1 * l2).IsRegular := by  obtain (he | hne) := isEmpty_or_nonempty Symbol  · obtain (rfl | rfl) := Language.eq_zero_or_one_ofIsEmpty l1 <;>    obtain (rfl | rfl) := Language.eq_zero_or_one_ofIsEmpty l2 <;> simp  · have := Classical.inhabited_of_nonempty hne    rw [IsRegular.iff_nfa] at h1 h2 ⊢    obtain ⟨State1, h_fin1, nfa1, rfl⟩ := h1    obtain ⟨State2, h_fin1, nfa2, rfl⟩ := h2    use Option State1 ⊕ Option State2, inferInstance,      ⟨finConcat nfa1 nfa2, inr '' (some '' nfa2.accept)⟩    exact finConcat_language_eq