Acc lang concat ne

theorem acc_lang_concat_ne :    (M0.Concat acc0 M1).AcceptedLang (inr '' acc1) =    (M0.AcceptedLang acc0) * (M1.AcceptedLang acc1 \ {[]}) := by  ext al ; constructor  · rintro ⟨m, as, ⟨ss, h_run, h_acc⟩, rfl⟩    have h_s1_ex : ∃ s1, ss m = inr s1 := by      rcases h_acc with ⟨s1, _, h_s1⟩      use s1 ; rw [h_s1]    obtain ⟨n, h_n, ⟨ss0, h_run0, h_acc0, h_ss0⟩, ⟨ss1, h_run1, h_ss1⟩⟩ := na_concat_fin_run_1.mp ⟨h_run, h_s1_ex⟩    use (as.extract 0 n), (as.extract n m)    simp (disch := omega) [append_extract_extract, extract_eq_nil_iff, h_n]    constructor    · use n, as ; simp ; use ss0    · use (m - n), (as.drop n) ; simp (disch := omega) [extract_drop]      use ss1 ; simp [h_run1]      obtain ⟨s1, h_acc1, h_s1⟩ := h_ss1 m (by omega) (by omega) ▸ h_acc      simpa [← inr.inj h_s1]  . rintro ⟨al0, al1, h_al0, h_al1, rfl⟩    obtain ⟨h_al1, h_al1_ne⟩ := h_al1    simp at h_al1_ne    rcases h_al0 with ⟨n, as0, ⟨⟨ss0, ⟨h_init0, h_next0⟩, h_acc0⟩, rfl⟩⟩    rcases h_al1 with ⟨m, as1, ⟨⟨ss1, ⟨h_init1, h_next1⟩, h_acc1⟩, rfl⟩⟩    have h_m : 0 < m := by simp [extract_eq_nil_iff] at h_al1_ne ; omega    let as := (as0.extract 0 n) ++ₛ as1    use (n + m), as ; constructor    · let ss := fun k ↦ if k < n + 1 then inl (ss0 k) else inr (ss1 (k - n))      use ss ; constructor      · suffices (M0.Concat acc0 M1).FinRun (n + m) as ss ∧ (∃ s1, ss (n + m) = inr s1) by tauto        apply na_concat_fin_run_1.mpr        use n ; constructor <;> [skip ; constructor]        · omega        · use ss0 ; simp [as, ss, h_acc0] ; constructor          · exact h_init0          · 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_next0 k h_k]        · use ss1 ; simp ; constructor <;> [constructor ; skip]          · exact h_init1          · intro k h_k            have h1 : (as0.extract 0 n).length = n := by simp [length_extract]            rw [← h1] ; simp [as, drop_append_stream]            exact h_next1 k h_k          · simp [ss] ; omega      · use (ss1 m)        have h_ss_nm : ss (n + m) = inr (ss1 m) := by          have h_m1 : ¬ n + m < n + 1 := by omega          simp [ss, h_m1]        simp [h_acc1, h_ss_nm]    · have h1 : (as0.extract 0 n).length ≤ n + m := by simp [length_extract]      simp [as, extract_append_zero_right h1, length_extract]