Μ bot JH eq μ tot

lemma μ_bot_JH_eq_μ_tot {ℒ : Type*} [Nontrivial ℒ] [Lattice ℒ] [BoundedOrder ℒ] [WellFoundedGT ℒ]{S : Type*} [CompleteLinearOrder S]{μ : {p : ℒ × ℒ // p.1 < p.2} → S}[hsl : SlopeLike μ] (JH : JordanHolderFiltration μ) :∀ i : ℕ, (hi : i < Nat.find JH.fin_len) → μ ⟨(⊥, JH.filtration i), by  rw [← Nat.find_spec JH.fin_len]  apply JH.strict_anti  · exact hi  · exact le_rfl  ⟩ = μ ⟨(⊥, ⊤), bot_lt_top⟩ := by  intro i hi  induction i with  | zero => simp only [JH.first_eq_top]  | succ i hi' =>    have := seesaw' μ hsl ⊥ (JH.filtration (i + 1)) ⊤ ⟨by      rw [← Nat.find_spec JH.fin_len]      apply JH.strict_anti      · exact hi      · exact le_rfl      ,by      rw [← JH.first_eq_top]      apply JH.strict_anti      · exact Nat.zero_lt_succ i      · exact le_of_lt hi      ⟩    refine (this.2.2.2.2 ?_).1    rw [← JH.step_cond₁ i <| Nat.lt_of_succ_lt hi]    if htop : JH.filtration i = ⊤ then      simp only [htop]    else    have := seesaw' μ hsl (JH.filtration (i + 1)) (JH.filtration i) ⊤ ⟨by      apply JH.strict_anti      · exact lt_add_one i      · exact Nat.le_of_succ_le hi      ,Ne.lt_top' fun a ↦ htop (id (Eq.symm a))      ⟩    refine (this.2.2.2.1 ?_).1    specialize hi' (Nat.lt_of_succ_lt hi)    have := seesaw' μ hsl ⊥ (JH.filtration i) ⊤ ⟨by      rw [← Nat.find_spec JH.fin_len]      apply JH.strict_anti      · exact Nat.lt_of_succ_lt hi      · exact le_rfl      ,Ne.lt_top' fun a ↦ htop (id (Eq.symm a))⟩    rw [← (this.2.2.1 hi').2,JH.step_cond₁ i <| Nat.lt_of_succ_lt hi]