I Sum run iff

@[simp, scoped grind =]theorem iSum_run_iff {na : (i : I) → NA (State i) Symbol}    {xs : ωSequence Symbol} {ss : ωSequence (Σ i, State i)} :    (iSum na).Run xs ss ↔ ∃ i ss_i, (na i).Run xs ss_i ∧ ss_i.map (Sigma.mk i) = ss := by  constructor  · rintro ⟨h_init, h_next⟩    obtain ⟨i, s0, h_s0, h_ss0⟩ := mem_iUnion.mp h_init    have h_exists n : ∃ s_i, ⟨i, s_i⟩ = ss n := by      induction n      case zero => use s0      case succ n h_ind =>        obtain ⟨j, s_j, t_j, _⟩ := h_next n        grind    choose ss_i h_ss_i using h_exists    use i, ss_i    refine ⟨⟨?_, ?_⟩, ?_⟩    · grind    · intro n      obtain ⟨j, _⟩ := h_next n      grind    · ext <;> grind  · rintro ⟨i, ss, h_run, rfl⟩    constructor    · simp only [iSum, get_map, mem_iUnion]      grind only [NA.Run, = mem_image]    · simp only [LTS.OmegaExecution]      grind only [NA.Run, = get_map, iSum, LTS.OmegaExecution]