Da concat det run cnt2

theorem da_concat_det_run_cnt2 (as : Stream' A) (n : ℕ) :    ∃ i, ((M1.Concat acc1 M2).DetRun as n).2 i = none := by  induction' n with n h_ind  · use 0 ; simp [DA.DetRun, DA.Concat]  let s_n := (M1.Concat acc1 M2).DetRun as n  obtain ⟨i, h_i⟩ := h_ind  rcases Classical.em (∃ j, j ≠ i ∧ s_n.2 j = none) with h_none | h_some  · obtain ⟨j, h_ne, h_j⟩ := h_none    simp [s_n] at h_j    wlog h : i < j generalizing i j with h'    · exact h' j h_j i (Ne.symm h_ne) h_i (by fin_omega)    use j ; simp [DA.DetRun, da_concat_next_2, h_j]    intro _ ; use i  · simp [ne_none_iff_isSome] at h_some    have h1 : {j | (s_n.2 j).isSome} = {i}ᶜ := by ext j ; simp ; grind    have h2 : {j | (s_n.2 j).isSome}.ncard = Nat.card M2.State + 1 := by      have h_sum := ncard_add_ncard_compl {i} ; simp at h_sum      rw [h1] ; omega    obtain ⟨j1, j2, h_ne, s2, h_j1, h_j2⟩ := option_some_pigeonhole s_n.2 (by omega)    wlog h : j1 < j2 generalizing j1 j2 with h'    · exact h' j2 j1 (Ne.symm h_ne) h_j2 h_j1 (by fin_omega)    simp [s_n] at h_j1 h_j2    use j2 ; simp [DA.DetRun, da_concat_next_2, h_j2]    use j1 ; simp [h, h_j1]