JHFil refine lt step payoff

lemma JHFil_refine_lt_step_payoff{ℒ : Type*} [Nontrivial ℒ] [Lattice ℒ] [BoundedOrder ℒ] [hacc : WellFoundedGT ℒ]{S : Type*} [CompleteLinearOrder S](μ : {p : ℒ × ℒ // p.1 < p.2} → S) [hwdcc' : StrongDescendingChainCondition' μ](hμ : μ ⟨(⊥, ⊤), bot_lt_top⟩ ≠ ⊤)(hμsl : SlopeLike μ) (hst : Semistable μ)(hdc : ∀ x : ℕ → ℒ, (sax : StrictAnti x) → ∃ N : ℕ, μ ⟨(x (N +1), x N), sax <| lt_add_one N⟩ = ⊤) :∀ k : ℕ,  (hk : JHFil μ hμ hμsl hst hdc k > ⊥) → ∀ z : ℒ, (h' : JHFil μ hμ hμsl hst hdc (k + 1) < z)  → (h'' : z < JHFil μ hμ hμsl hst hdc k) →  μ ⟨(JHFil μ hμ hμsl hst hdc (k + 1), z), h'⟩ < μ ⟨(JHFil μ hμ hμsl hst hdc (k + 1),    JHFil μ hμ hμsl hst hdc k), JHFil_anti_mono μ hμ hμsl hst hdc k hk⟩ := by  intro k hk z h' h''  have this_new : Semistable μ → μmax μ TotIntvl = μ TotIntvl :=    fun a ↦ (List.TFAE.out (impl.thm4d21 μ hμsl inferInstance inferInstance).1 0 3).2      ((impl.thm4d21 μ hμsl inferInstance inferInstance).2.1 a)  specialize this_new hst  simp only [μmax, TotIntvl, ne_eq] at this_new  have this_q: μ ⟨(⊥, z), lt_of_le_of_lt bot_le h'⟩ ≤ μ ⟨(⊥, ⊤), bot_lt_top⟩ := by    rw [← this_new]    exact le_sSup ⟨z, ⟨in_TotIntvl z,      Ne.symm <| bot_lt_iff_ne_bot.1 <| lt_of_le_of_lt bot_le h'⟩, rfl⟩  by_cases hfp1bot : JHFil μ hμ hμsl hst hdc (k + 1) = ⊥  · simp only [hfp1bot]    have : ¬ {p | ∃ (h : ⊥ < p), p < JHFil μ hμ hμsl hst hdc k ∧ μ ⟨(⊥, p), h⟩ =      μ ⟨(⊥, ⊤), bot_lt_top⟩}.Nonempty := by      by_contra!      simp only [JHFil,this] at hfp1bot      have := (hacc.wf.has_min _ this).choose_spec.1.out.choose      simp only [↓reduceDIte, exists_and_left, Set.mem_setOf_eq, and_imp,        forall_exists_index] at hfp1bot      simp only [exists_and_left, Set.mem_setOf_eq, and_imp, forall_exists_index] at this      exact (ne_of_lt this) hfp1bot.symm    apply Set.not_nonempty_iff_eq_empty.1 at this    apply Set.eq_empty_iff_forall_notMem.1 at this    specialize this z    simp only [exists_and_left, Set.mem_setOf_eq, not_and, not_exists] at this    replace := lt_of_le_of_ne this_q <| this h'' (lt_of_le_of_lt bot_le h')    by_cases hk' : k = 0    · simpa only [hk',JHFil]    · conv_rhs =>        arg 1; arg 1; arg 2; arg 6        rw [← Nat.sub_one_add_one hk']      have hne : {p | ∃ (h : ⊥ < p), p < JHFil μ hμ hμsl hst hdc (k - 1) ∧ μ ⟨(⊥, p), h⟩ =        μ ⟨(⊥, ⊤), bot_lt_top⟩}.Nonempty := by        by_contra!        have this': JHFil μ hμ hμsl hst hdc k = JHFil μ hμ hμsl hst hdc ((k-1)+1) := by          conv_lhs =>            arg 6            rw [← Nat.sub_one_add_one hk']        simp only [this',JHFil,this] at hk        simp only [Set.not_nonempty_empty, ↓reduceDIte, gt_iff_lt, lt_self_iff_false] at hk      rw [← (hacc.wf.has_min _ hne).choose_spec.1.out.2.2] at this      simp only [JHFil,hne]      simp only [↓reduceDIte, exists_and_left, Set.mem_setOf_eq, gt_iff_lt, and_imp,        forall_exists_index]      simpa only [exists_and_left, Set.mem_setOf_eq,        gt_iff_lt, and_imp, forall_exists_index] using this  · have h''' : μ ⟨(⊥, z), lt_of_le_of_lt bot_le h'⟩ < μ ⟨(⊥, ⊤), bot_lt_top⟩ := by      refine lt_of_le_of_ne this_q ?_      by_contra!      by_cases hne : {p | ∃ (h : ⊥ < p), p < JHFil μ hμ hμsl hst hdc k ∧        μ ⟨(⊥, p), h⟩ = μ ⟨(⊥, ⊤), bot_lt_top⟩}.Nonempty      · have := (hacc.wf.has_min _ hne).choose_spec.2 z (by use lt_of_le_of_lt bot_le h')        simp only [JHFil,hne] at h'        simp only [gt_iff_lt, exists_and_left, Set.mem_setOf_eq, and_imp, forall_exists_index,          ↓reduceDIte] at *        exact this h'      · refine hne ?_        use z, lt_of_le_of_lt bot_le h'    have h'''' : μ ⟨(⊥, ⊤), bot_lt_top⟩ = μ ⟨(⊥, JHFil μ hμ hμsl hst hdc (k + 1)),      bot_lt_iff_ne_bot.2 hfp1bot⟩ := by      by_cases hne : {p | ∃ (h : ⊥ < p), p < JHFil μ hμ hμsl hst hdc k ∧ μ ⟨(⊥, p), h⟩ =        μ ⟨(⊥, ⊤), bot_lt_top⟩}.Nonempty      · simp only [JHFil,hne]        have := (hacc.wf.has_min _ hne).choose_spec.1.out.choose_spec.2        simp only [gt_iff_lt, exists_and_left, Set.mem_setOf_eq, and_imp, forall_exists_index,          ↓reduceDIte] at *        exact this.symm      · simp only [JHFil,hne] at hfp1bot        simp only [↓reduceDIte, not_true_eq_false] at hfp1bot    exact (JHFil_step_payoff_eq_tot μ hμ hμsl hst hdc k hk).symm ▸ lt_trans ((Or.resolve_right <|      (Or.resolve_left <| (impl.prop4d6 μ).1 hμsl ⊥ (JHFil μ hμ hμsl hst hdc (k + 1)) z      ⟨bot_lt_iff_ne_bot.2 hfp1bot,h'⟩) (not_and_iff_not_or_not.2 <| Or.inl <| not_lt_of_gt <|      h'''' ▸ h''')) (not_and_iff_not_or_not.2 <| Or.inl <| ne_of_gt <| h'''' ▸ h''')).2 h'''