Fair Deliver Msg schedule Msgs

theorem fairDeliverMsg_scheduleMsgs {d : DeliverMsg P M S} {ps : Set P} {q : State P M S → Prop}    (hd : a.FairDeliverMsg d ps q) (s : State P M S) (hs : q s) :    let xl := (d.scheduleMsgs ps s).fst    let t := (d.scheduleMsgs ps s).snd    q t ∧ a.lts.MTr s xl t ∧ xl.length > 0 ∧ ∀ m, m ∈ s.msgs → m.dest ∈ ps → some m ∈ xl := by  classical  intro xl t  let ms := s.msgs.filter (fun m ↦ m.dest ∈ ps)  by_cases h_ms : ms = 0  · have h1 : xl = [none] ∧ t = s := by grind [DeliverMsg.scheduleMsgs]    simp [ms, eq_zero_iff_forall_notMem] at h_ms    simp only [h1, hs, List.length_cons, List.length_nil, zero_add, Order.lt_one_iff, true_and]    split_ands    · apply LTS.MTr.single      grind [Algorithm.lts]    · grind  · have : q t ∧ a.lts.MTr s xl t ∧ ∀ m, m ∈ ms.toList → some m ∈ xl := by      grind [DeliverMsg.scheduleMsgs, fairDeliverMsg_foldList hd s ms.toList ∅ (by simp [ms, hs])]    obtain ⟨m, _⟩ := exists_mem_of_ne_zero h_ms    have : some m ∈ xl := by grind [mem_toList]    split_ands <;> grind [mem_toList, mem_filter]