Det muller lang concat

theorem det_muller_lang_concat {L0 : Set (List A)} {L1 : Set (Stream' A)}    (h0 : RegLang L0) (h1 : DetMullerLang L1) : DetMullerLang (L0 * L1) := by  obtain ⟨M0, acc0, h_fin0, rfl⟩ := reg_lang_det_accept h0  obtain ⟨M1, accSet1, h_fin1, rfl⟩ := h1  use (M0.Concat acc0 M1), (Automata.DA.MullerAcc_Concat M0 acc0 M1 accSet1)  constructor  · apply Finite.instProd  · ext as ; constructor    · intro h_acc      obtain ⟨n, h_acc0, h_acc1⟩ := Automata.da_concat_of_muller_accept M0 acc0 M1 accSet1 as h_acc      use (as.extract 0 n), (as.drop n)      simp [h_acc1, append_extract_drop]      use n, as    · rintro ⟨al0, as1, ⟨n, as0, h_as0, rfl⟩, h_as1, h_as⟩      have h_acc0 : M0.toNA.FinAccept acc0 n as := by        obtain ⟨ss0, h_run0, h_acc0⟩ := h_as0        use ss0 ; simp [← h_as, h_acc0] ; constructor        · exact h_run0.1        intro k h_k        have h1 : k < (as0.extract 0 n).length := by simp [length_extract, h_k]        simp (disch := omega) [get_append_left' h1, get_extract', h_run0.2 k h_k]      have h_acc1 : M1.MullerAccept accSet1 (as.drop n) := by        have h1 : n = (as0.extract 0 n).length := by simp [length_extract]        rw [h1] ; simp [← h_as, drop_append_stream] ; exact h_as1      exact Automata.da_concat_to_muller_accept M0 acc0 M1 accSet1 as n h_acc0 h_acc1