Stable of step cond₂

lemma stable_of_step_cond₂{ℒ : Type*} [Nontrivial ℒ] [Lattice ℒ] [BoundedOrder ℒ] [WellFoundedGT ℒ]{S : Type*} [CompleteLinearOrder S](μ : {p : ℒ × ℒ // p.1 < p.2} → S) [SlopeLike μ] [sdc : StrongDescendingChainCondition' μ](filtration : ℕ → ℒ) (fin_len : ∃ N : ℕ, filtration N = ⊥)(strict_anti : ∀ i j : ℕ, i < j → j ≤ Nat.find (fin_len) → filtration j < filtration i) :(∀ i : ℕ, (hi : i < Nat.find fin_len) →    ∀ z : ℒ, (h' : filtration (i+1) < z) → (h'' : z < filtration i) →    μ ⟨(filtration (i+1), z), h'⟩ < μ ⟨(filtration (i+1), filtration i),      strict_anti i (i+1) (lt_add_one i) hi⟩)→ (∀ i : ℕ, (hi : i < Nat.find fin_len) → Stable (Resμ ⟨(filtration (i+1), filtration i),  strict_anti i (i+1) (lt_add_one i) hi⟩ μ)) := by    intro h i hi    refine {      toSemistable := semistable_of_step_cond₂ μ filtration fin_len strict_anti h i hi, stable := ?_      }    · intro x hx hx'      let stepI : {p : ℒ × ℒ // p.1 < p.2} :=        ⟨(filtration (i + 1), filtration i), strict_anti i (i + 1) (lt_add_one i) hi⟩      have hx_left : filtration (i + 1) < x.val := lt_of_le_of_ne x.prop.1 (by        by_contra hc        exact hx <| Subtype.coe_inj.1 <| id (Eq.symm hc))      have hAstar_step := (proposition_4_1 (Resμ stepI μ) inferInstance inferInstance).1      have hAstar_x := (proposition_4_1 (Resμ ⟨(filtration (i + 1), x.val), hx_left⟩ μ)        inferInstance inferInstance).1      simp only [μAstar, μA_res_intvl,μmin_res_intvl] at *      rw [hAstar_step]      simp only [strip_bot <| strict_anti i (i + 1) (lt_add_one i) hi,        strip_top hx_left, strip_bot hx_left] at *      rw [hAstar_x]      have hss := semistable_of_step_cond₂ μ filtration fin_len strict_anti h i hi      have hNash_step :=        (impl.thm4d21 (Resμ stepI μ) inferInstance inferInstance inferInstance).2.1 hss      have hμmin_step := (List.TFAE.out        (impl.thm4d21 (Resμ stepI μ) inferInstance inferInstance inferInstance).1 1 3).2 hNash_step      simp only [μmin_res_intvl,μ_res_intvl] at hμmin_step      simp only [strip_bot <| strict_anti i (i + 1) (lt_add_one i) hi,        strip_top <| strict_anti i (i + 1) (lt_add_one i) hi] at *      rw [hμmin_step]      apply ne_of_lt      have hμmin_le :          μmin μ ⟨(filtration (i + 1), ↑x), hx_left⟩ ≤            μ ⟨(filtration (i + 1), ↑x), hx_left⟩ := by        apply sInf_le        simp only [ne_eq, Set.mem_setOf_eq]        use filtration (i + 1)        simp only [exists_prop, and_true]        refine ⟨⟨le_rfl,x.prop.1⟩, ?_⟩        by_contra hc        refine hx ?_        apply Subtype.coe_inj.1        simpa [← hc] using by rfl      refine lt_of_le_of_lt hμmin_le ?_      exact (h i hi) x.val hx_left <| lt_iff_le_not_ge.mpr (lt_top_iff_ne_top.2 hx')