Step cond₂ of stable

lemma step_cond₂_of_stable {ℒ : 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) → Stable (Resμ ⟨(filtration (i+1), filtration i),  strict_anti i (i+1) (lt_add_one i) hi⟩ μ))→ (∀ 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⟩) := by  intro hst i hi z hz hz'  let stepI : {p : ℒ × ℒ // p.1 < p.2} :=    ⟨(filtration (i + 1), filtration i), strict_anti i (i + 1) (lt_add_one i) hi⟩  let midI : Interval stepI := ⟨z, le_of_lt hz, le_of_lt hz'⟩  have hmid_ne_bot : midI ≠ ⊥ := by    by_contra hc    apply Subtype.coe_inj.2 at hc    simp only [midI, stepI] at hc    rw [hc] at hz    exact False.elim <| (lt_self_iff_false (filtration (i + 1))).mp hz  have hmid_ne_top : midI ≠ ⊤ := by    by_contra hc    apply Subtype.coe_inj.2 at hc    simp only [midI, stepI] at hc    rw [hc] at hz'    exact False.elim <| (lt_self_iff_false (filtration i)).mp hz'  have hss := (hst i hi).toSemistable.semistable midI hmid_ne_bot  simp only [gt_iff_lt, not_lt] at hss  have hst' := (hst i hi).stable midI hmid_ne_bot hmid_ne_top  have hst' := lt_of_le_of_ne hss hst'  have hAstar_step := (proposition_4_1 (Resμ stepI μ) inferInstance inferInstance).1  unfold μAstar at hAstar_step  rw [hAstar_step] at hst'  have hAstar_mid := (proposition_4_1 (Resμ ⟨(filtration (i + 1), z), hz⟩ μ)    inferInstance inferInstance).1  unfold μAstar at hAstar_mid  have hb : μA (Resμ ⟨(filtration (i + 1), filtration i), gt_trans hz' hz⟩ μ)    ⟨(⊥, midI), bot_lt_iff_ne_bot.2 hmid_ne_bot⟩ =    μA (Resμ ⟨(filtration (i + 1), z), hz⟩ μ) ⟨(⊥, ⊤), bot_lt_top⟩ := by    simp only [μA_res_intvl,μmin_res_intvl] at *    rfl  rw [hb, hAstar_mid] at hst'  have hNash_step := (impl.thm4d21 (Resμ stepI μ) inferInstance inferInstance inferInstance).2.1    (hst i hi).toSemistable  have hμmin_step := (List.TFAE.out    (impl.thm4d21 (Resμ stepI μ) inferInstance inferInstance inferInstance).1 1 3).2 hNash_step  rw [hμmin_step] at hst'  have hμmax_step := (List.TFAE.out    (impl.thm4d21 (Resμ stepI μ) inferInstance inferInstance inferInstance).1 0 3).2 hNash_step  simp only [μmin_res_intvl,μ_res_intvl] at hst'  unfold μmax at hμmax_step  have hsSup_step := le_of_eq hμmax_step  apply sSup_le_iff.1 at hsSup_step  simp only [ne_eq, Set.mem_setOf_eq, forall_exists_index] at hsSup_step  have hsSup_step_bak := hsSup_step  have hsSup_mid := hsSup_step (Resμ ⟨(filtration (i + 1), filtration i), gt_trans hz' hz⟩    μ ⟨(⊥, midI), bot_lt_iff_ne_bot.2 hmid_ne_bot⟩)    midI ⟨in_TotIntvl _, fun hc => hmid_ne_bot hc.symm⟩ rfl  have hsSup_mid' : μ ⟨(filtration (i + 1), z), hz⟩ ≤ μ ⟨(filtration (i + 1), filtration i),      strict_anti i (i + 1) (lt_add_one i) hi⟩ := hsSup_mid  refine lt_of_le_of_ne hsSup_mid' ?_  by_contra hc  simp only [strip_bot (gt_trans hz' hz), strip_top (gt_trans hz' hz)] at hst'  rw [← hc] at hst'  have t1 : ↑(@Bot.bot (Interval ⟨(filtration (i + 1), z), hz⟩) instBoundedOrderInterval.toBot :    Interval ⟨(filtration (i + 1), z), hz⟩) = filtration (i + 1) := rfl  have t2 : ↑(@Top.top (Interval ⟨(filtration (i + 1), z), hz⟩) instBoundedOrderInterval.toTop :    Interval ⟨(filtration (i + 1), z), hz⟩) = z := rfl  simp only [t1, t2] at hst'  unfold μmin at hst'  apply sInf_lt_iff.1 at hst'  rcases hst' with ⟨s,⟨y,hy1,hy2⟩,hs⟩  rw [← hy2] at hs  have := ((seesaw' μ inferInstance (filtration (i + 1)) y z ⟨by    refine lt_of_le_of_ne hy1.1.1 ?_    by_contra hc    simp only [hc, lt_self_iff_false] at hs    ,lt_of_le_of_ne hy1.1.2 hy1.2⟩).2.1.2.2 hs).1  simp only [hc, gt_iff_lt] at this  have res := hsSup_step_bak (Resμ ⟨(filtration (i + 1), filtration i), gt_trans hz' hz⟩    μ ⟨(⊥, ⟨y,hy1.1.1,le_of_lt <| lt_of_le_of_lt hy1.1.2 hz'⟩), by    refine lt_of_le_of_ne hy1.1.1 ?_    by_contra hc    simp only at hc    apply Subtype.coe_inj.2 at hc    simp only at hc    simp only [← hc, strip_bot (gt_trans hz' hz), lt_self_iff_false] at hs⟩)      ⟨y,hy1.1.1,le_of_lt <| lt_of_le_of_lt hy1.1.2 hz'⟩ ⟨in_TotIntvl _, by      by_contra hc      apply Subtype.coe_inj.2 at hc      simp only at hc      have hy_bot : y = filtration (i + 1) := by        simpa only [strip_bot (gt_trans hz' hz)] using hc.symm      exact (lt_self_iff_false (μ ⟨(filtration (i + 1), z), hz⟩)).mp <| by        simpa only [hy_bot] using hs    ⟩ rfl  simp only [stepI, μ_res_intvl, strip_bot (gt_trans hz' hz), strip_top (gt_trans hz' hz)] at res  exact (not_le_of_gt this) res