Concat run exists

theorem concat_run_exists {xs1 : List Symbol} {xs2 : ωSequence Symbol} {ss2 : ωSequence State2}    (h1 : xs1 ∈ language na1) (h2 : na2.Run xs2 ss2) :    ∃ ss, (concat na1 na2).Run (xs1 ++ω xs2) ss ∧ ss.drop xs1.length = ss2.map inr := by  by_cases h_xs1 : xs1.length = 0  · obtain ⟨rfl⟩ : xs1 = [] := List.eq_nil_iff_length_eq_zero.mpr h_xs1    use ss2.map inr    split_ands    · simp [concat]      grind only [LTS.OmegaExecution, = Set.mem_union, = get_map, = Set.mem_image, Run]    · simp  · obtain ⟨s0, _, _, _, h_mtr⟩ := h1    obtain ⟨ss1, _, _, _, _⟩ := LTS.Execution.of_mTr h_mtr    let ss := (ss1.map inl).take xs1.length ++ω ss2.map inr    refine ⟨ss, Run.mk ?_ ?_, ?_⟩    · grind [concat, get_append_left]    · have (k) (h_k : ¬ k < xs1.length) : k + 1 - xs1.length = k - xs1.length + 1 := by grind      simp only [concat]      grind only [Run, LTS.OmegaExecution, get_append_right', get_append_left,        = List.length_take, = get_map, = List.length_map, = min_def, = List.getElem_take,        = List.getElem_map]    · grind [drop_append_of_le_length]