Inter language eq

@[simp, scoped grind =]theorem inter_language_eq :    language (Buchi.mk (interNA na acc) (interAccept acc)) =    ⨅ i, language (Buchi.mk (na i) (acc i)) := by  apply mem_ext  intro xs  simp only [ωLanguage.mem_iInf]  constructor  · intro ⟨ss, h_run, h_inf⟩ i    use ss.map (fun s ↦ s.fst i)    constructor    · apply iProd_run_iff.mp <| hist_run_proj h_run    · simp only [interAccept, mem_union, frequently_or_distrib] at h_inf      cases i      · rcases h_inf with h_inf_f | h_inf_t        · apply Frequently.mono h_inf_f          grind        · apply Frequently.mono <| inter_freq_acc_freq_acc h_run h_inf_t          grind      · rcases h_inf with h_inf_f | h_inf_t        · apply Frequently.mono <| inter_freq_acc_freq_acc h_run h_inf_f          grind        · apply Frequently.mono h_inf_t          grind  · intro h    choose ss_i h_ss_i using h    let ss_p : ωSequence (Π i, State i) := fun k i ↦ ss_i i k    have h_ss_p : (iProd na).Run xs ss_p := by      grind only [Run, = iProd_run_iff, = get_fun, = LTS.OmegaExecution, = get_map]    have (k : ℕ) (i : Bool) : ss_p k i = ss_i i k := rfl    obtain ⟨ss, h_run, _⟩ := hist_run_exists h_ss_p    use ss, h_run    apply inter_freq_comp_acc_freq_acc h_run    · apply Frequently.mono (h_ss_i false).2      grind    · apply Frequently.mono (h_ss_i true).2      grind