Da concat ptr2 exists

theorem da_concat_ptr2_exists (as : Stream' A) (n : ℕ) (h_n : M1.DetRun as n ∈ acc1) (k : ℕ) :    ∃ i, ((M1.Concat acc1 M2).DetRun as (n + k + 1)).2 i = some (M2.DetRun (as.drop n) (k + 1)) ∧      if k = 0 then        ((M1.Concat acc1 M2).DetRun as (n + k)).2 i = none ∧        ∀ j < i, (((M1.Concat acc1 M2).DetRun as (n + k)).2 j).isSome      else        ((M1.Concat acc1 M2).DetRun as (n + k)).2 i = some (M2.DetRun (as.drop n) k) ∧        ∀ j < i, ((M1.Concat acc1 M2).DetRun as (n + k)).2 j ≠ ((M1.Concat acc1 M2).DetRun as (n + k)).2 i := by  induction' k with k h_ind  . let I := {i | ((M1.Concat acc1 M2).DetRun as n).2 i = none}    have h_fin : I.Finite := by exact toFinite I    have h_ne : I.Nonempty := by exact da_concat_det_run_cnt2 M1 acc1 M2 as n    obtain ⟨i, h_i, h_min⟩ := Finite.exists_minimal h_fin h_ne    simp [I] at h_i h_min    use i    simp [h_i, DA.DetRun, da_concat_next_2, da_concat_det_run_1, h_n, get_drop', ← ne_none_iff_isSome]    intro j h_j h_contra ; have := h_min h_contra ; fin_omega  obtain ⟨i, h_i, _⟩ := h_ind  let I := {j | ((M1.Concat acc1 M2).DetRun as (n + k + 1)).2 j = some (M2.DetRun (as.drop n) (k + 1))}  have h_fin : I.Finite := by exact toFinite I  have h_ne : I.Nonempty := by use i ; simp [I, h_i]  obtain ⟨j, h_j, h_min⟩ := Finite.exists_minimal h_fin h_ne  simp [I] at h_j h_min  use j  simp [h_j, ← add_assoc]  rw [DA.DetRun]  simp [da_concat_next_2, h_j]  have h_min' : ∀ j' < j, ¬((M1.Concat acc1 M2).DetRun as (n + k + 1)).2 j' = some (M2.DetRun (as.drop n) (k + 1)) := by    intro j' h_j' h_contra ; have := h_min h_contra ; fin_omega  constructorm* _ ∧ _  · grind  · simp [DA.DetRun, get_drop', (show n + (k + 1) = n + k + 1 by omega)]  · grind