Exists unique rel Series is Interval Semistable of complete Linear Order

theorem exists_unique_relSeries_isIntervalSemistable_of_completeLinearOrder{ℒ : Type*} [Nontrivial ℒ] [Lattice ℒ] [BoundedOrder ℒ] [WellFoundedGT ℒ]{S : Type*} [CompleteLinearOrder S](μ : {p :ℒ × ℒ // p.1 < p.2} → S)[hμ : μA_DescendingChainCondition μ] [hμcvx : Convex μ] :------------∃! s : RelSeries (IntervalSemistableRel μ),  s.head = ⊥ ∧ s.last = ⊤ ∧  ∀ i : ℕ, (hi : i + 1 < s.length) →    ¬   μA μ ⟨(s.toFun i, s.toFun ↑(i+1)), impl.relSeries_step_lt s hi⟩      ≤ μA μ ⟨(s.toFun ↑(i+1), s.toFun ↑(i+2)), impl.relSeries_succ_step_lt s hi⟩------------:= by  apply existsUnique_of_exists_of_unique  · exact exists_relSeries_isIntervalSemistable μ  · intro F1 F2 h1 h2    rcases impl.hHFil_of_hNSeries μ F1 h1 with ⟨HN1,len1⟩    rcases impl.hHFil_of_hNSeries μ F2 h2 with ⟨HN2,len2⟩    have t2 := instUniqueHarderNarasimhanFiltration.uniq HN2    have := t2.symm ▸ (instUniqueHarderNarasimhanFiltration.uniq HN1)    have len_eq : F1.length = F2.length := by      rw [← len1.2, ← len2.2, this]    ext x    · rw [← len1.2, ← len2.2, this]    · simp only [Function.comp_apply]      have := congrFun (congrArg HarderNarasimhanFiltration.filtration this) ↑x      rw [len1.1,len2.1] at this      convert this      · simp only [Fin.cast_val_eq_self]        if hx : ↑x ≤ F1.length then          simp only [hx, ↓reduceIte]        else          simp only [hx, ↓reduceIte]          simp only [not_le] at hx          have := Fin.is_le x          exfalso          linarith      · if hx : ↑x ≤ F2.length then          simp only [hx, ↓reduceIte]          congr          refine Fin.eq_of_val_eq <| Eq.symm (Fin.val_cast_of_lt ?_)          exact Nat.lt_add_one_of_le hx        else          simp only [hx, ↓reduceIte]          simp only [not_le] at hx          have : ↑x ≤ F2.length := len_eq ▸ Fin.is_le x          exfalso          linarith