Da acc lang compl

theorem da_acc_lang_compl [Inhabited A] :    M.toNA.AcceptedLang accᶜ = (M.toNA.AcceptedLang acc)ᶜ := by  ext al  constructor  · rintro ⟨n, as, ⟨ss, h_run, h_acc⟩, h_al⟩    rintro ⟨n', as', ⟨ss', h_run', h_acc'⟩, h_al'⟩    have h_len : al.length = n := by simp [← h_al, length_extract]    have h_len' : al.length = n' := by simp [← h_al', length_extract]    obtain ⟨rfl⟩ := show n' = n by rw [← h_len, ← h_len']    have h_run_n := na_FinRun_fixSuffix h_run    have h_run_n' := na_FinRun_fixSuffix h_run'    have h_as_eq : fixSuffix as' n default = fixSuffix as n default := by      ext k ; simp [get.eq_1] ; rcases Classical.em (k < n) with h_k | h_k <;> simp [fixSuffix, h_k]      have h_as_k : as k = al.get ⟨k, (by omega)⟩ := by simp (disch := omega) [← h_al, get_extract']      have h_as_k' : as' k = al.get ⟨k, (by omega)⟩ := by simp (disch := omega) [← h_al', get_extract']      rw [h_as_k, h_as_k']    rw [h_as_eq] at h_run_n'    have h_ss_n := da_fin_run_unique h_run_n n (by omega)    have h_ss_n' := da_fin_run_unique h_run_n' n (by omega)    simp [fixSuffix] at h_ss_n h_ss_n'    rw [h_ss_n] at h_acc ; rw [h_ss_n'] at h_acc'    contradiction  · intro h_compl--    let as := fun k ↦ if h : k < al.length then al[k] else default    let as := al.padDefault    have h_al : as.extract 0 al.length = al := by simp [as, extract_padDefault]    use al.length, as ; simp [h_al]    let ss := M.DetRun as    have h_run : M.toNA.FinRun al.length as ss := by exact da_fin_run_exists al.length as    use ss ; constructor    · exact h_run    intro h_acc    have : al ∈ (M.toNA.AcceptedLang acc) := by      use al.length, as ; simp [h_al] ; use! ss    contradiction