Is Regular i Sup

@[simp]theorem IsRegular.iSup {I : Type*} [Finite I] {s : Set I} {l : I → Language Symbol}    (h : ∀ i ∈ s, (l i).IsRegular) : (⨆ i ∈ s, l i).IsRegular := by  generalize h_n : s.ncard = n  induction n generalizing s  case zero =>    obtain ⟨rfl⟩ := (ncard_eq_zero (s := s)).mp h_n    simp only [mem_empty_iff_false, not_false_eq_true, iSup_neg, iSup_bot]    exact IsRegular.zero  case succ n h_ind =>    obtain ⟨i, t, h_i, rfl, rfl⟩ := (ncard_eq_succ (s := s)).mp h_n    rw [iSup_insert]    apply IsRegular.add <;> grind