JHFil step payoff eq tot

lemma JHFil_step_payoff_eq_tot{ℒ : Type*} [Nontrivial ℒ] [Lattice ℒ] [BoundedOrder ℒ] [hacc : WellFoundedGT ℒ]{S : Type*} [CompleteLinearOrder S](μ : {p : ℒ × ℒ // p.1 < p.2} → S)(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 > ⊥) → μ ⟨(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⟩ = μ ⟨(⊥,⊤),bot_lt_top⟩ := by  intro k  induction k with  | zero =>    intro hk'    simp only [JHFil]    by_cases this : {p : ℒ | ∃ h : ⊥ < p, p < ⊤ ∧ μ ⟨(⊥,p),h⟩ = μ ⟨(⊥,⊤),bot_lt_top⟩}.Nonempty    · simp only [this]      let minTop := hacc.wf.has_min _ this      have this' := minTop.choose_spec.1.2.2      exact ((Or.resolve_left <| (Or.resolve_left <| (impl.prop4d6 μ).1 hμsl ⊥        minTop.choose ⊤ ⟨minTop.choose_spec.1.choose, minTop.choose_spec.1.out.choose_spec.1⟩)        (by aesop)) (by aesop)).2.symm    · simp only [this, ↓reduceDIte]  | succ k hk =>    intro hk'    have jh_kp1_ntop : {p : ℒ | ∃ h : ⊥ < p, p < JHFil μ hμ hμsl hst hdc k ∧ μ ⟨(⊥,p),h⟩ =      μ ⟨(⊥,⊤),bot_lt_top⟩}.Nonempty := by      by_contra!      simp only [JHFil,this, Set.not_nonempty_empty, ↓reduceDIte, gt_iff_lt,        lt_self_iff_false] at hk'    let min1 := hacc.wf.has_min _ jh_kp1_ntop    have jh_kp1_ntop' : JHFil μ hμ hμsl hst hdc k > ⊥ := by      refine lt_trans hk' ?_      simp only [JHFil,jh_kp1_ntop]      exact min1.choose_spec.1.out.choose_spec.1    have bot_jh_kp1_eq_ans := min1.choose_spec.1.2.2    by_cases jh_kp2_ntop : {p : ℒ | ∃ h : ⊥ < p, p < JHFil μ hμ hμsl hst hdc (k + 1) ∧ μ ⟨(⊥,p),h⟩      = μ ⟨(⊥,⊤),bot_lt_top⟩}.Nonempty    · let min2 := hacc.wf.has_min _ jh_kp2_ntop      have smart : μ ⟨(⊥, min2.choose), min2.choose_spec.1.out.1⟩ =          μ ⟨(⊥, JHFil μ hμ hμsl hst hdc (k + 1)), hk'⟩ := by        rw [min2.choose_spec.1.out.choose_spec.2,← bot_jh_kp1_eq_ans]        simp only [JHFil,jh_kp1_ntop ]        simp only [exists_and_left, Set.mem_setOf_eq, and_imp, forall_exists_index,          ↓reduceDIte]      have hfinal : μ ⟨(⊥, JHFil μ hμ hμsl hst hdc (k + 1)), hk'⟩ =        μ ⟨(min2.choose, JHFil μ hμ hμsl hst hdc (k + 1)),        min2.choose_spec.1.out.choose_spec.1⟩ := by        refine (Or.resolve_left ((Or.resolve_left <| (impl.prop4d6 μ).1 hμsl ⊥          min2.choose (JHFil μ hμ hμsl hst hdc (k + 1))          ⟨min2.choose_spec.1.out.choose, min2.choose_spec.1.out.choose_spec.1⟩) (?_)) (?_)).2        · apply not_and_iff_not_or_not.2          refine Or.inl ?_          simp only [smart]; simp only [JHFil,jh_kp1_ntop]          simp only [↓reduceDIte,            exists_and_left, Set.mem_setOf_eq, and_imp, forall_exists_index,            lt_self_iff_false, not_false_eq_true]        · apply not_and_iff_not_or_not.2          refine Or.inl ?_          simp only [smart]; simp only [JHFil,jh_kp1_ntop]          simp only [↓reduceDIte, exists_and_left, Set.mem_setOf_eq, gt_iff_lt, and_imp,            forall_exists_index, lt_self_iff_false, not_false_eq_true]      conv_lhs =>        arg 1; arg 1; arg 1        unfold JHFil        simp only [jh_kp2_ntop]        simp only [↓reduceDIte, exists_and_left, Set.mem_setOf_eq, gt_iff_lt, and_imp,          forall_exists_index]      simp only [exists_and_left, Set.mem_setOf_eq, and_imp,        forall_exists_index] at hfinal      rw [← hfinal]      simp only [JHFil,jh_kp1_ntop]      simp only [↓reduceDIte, exists_and_left, Set.mem_setOf_eq, and_imp,        forall_exists_index]      simp only [exists_and_left, Set.mem_setOf_eq, and_imp,        forall_exists_index] at bot_jh_kp1_eq_ans      exact bot_jh_kp1_eq_ans    · conv_lhs =>        arg 1; arg 1; arg 1        unfold JHFil        simp only [jh_kp2_ntop]        simp only [↓reduceDIte]      have this': μ ⟨(⊥, JHFil μ hμ hμsl hst hdc k), jh_kp1_ntop'⟩ = μ ⟨(⊥,⊤),bot_lt_top⟩ := by        by_cases hh : k = 0        · simp only [hh,JHFil]        · have : JHFil μ hμ hμsl hst hdc k = JHFil μ hμ hμsl hst hdc ((k-1)+1) := by            simp only [Nat.sub_one_add_one hh]          simp only [this]          have : {p | ∃ (h : ⊥ < p), p < JHFil μ hμ hμsl hst hdc (k-1) ∧ μ ⟨(⊥, p), h⟩ = μ ⟨(⊥, ⊤),            bot_lt_top⟩}.Nonempty := by            by_contra hthis            rw [this] at jh_kp1_ntop'            simp only [JHFil,hthis] at jh_kp1_ntop'; simp only [↓reduceDIte, gt_iff_lt,              lt_self_iff_false] at jh_kp1_ntop'          simp only [JHFil,this]          simp only [↓reduceDIte, exists_and_left, Set.mem_setOf_eq, and_imp,            forall_exists_index]          simpa only [exists_and_left, Set.mem_setOf_eq, gt_iff_lt, and_imp,            forall_exists_index] using (hacc.wf.has_min _ this).choose_spec.1.out.choose_spec.2      simp only [← this']      have : JHFil μ hμ hμsl hst hdc (k + 1) < JHFil μ hμ hμsl hst hdc k := by        simpa only [JHFil, jh_kp1_ntop, ↓reduceDIte] using          min1.choose_spec.1.out.choose_spec.1      have this'' :  μ ⟨(⊥, JHFil μ hμ hμsl hst hdc (k + 1)), hk'⟩ = μ ⟨(JHFil μ hμ hμsl hst hdc        (k + 1), JHFil μ hμ hμsl hst hdc k), this⟩ := by        rw [hk jh_kp1_ntop',← bot_jh_kp1_eq_ans]        simp only [JHFil,jh_kp1_ntop]        simp only [↓reduceDIte, exists_and_left, Set.mem_setOf_eq, and_imp,          forall_exists_index]      exact ((Or.resolve_left <| (Or.resolve_left <| (impl.prop4d6 μ).1 hμsl ⊥ (JHFil μ hμ hμsl hst        hdc (k + 1)) (JHFil μ hμ hμsl hst hdc k) ⟨hk',this⟩) (fun this_1 ↦ ne_of_lt        (lt_trans this_1.left this_1.right) this'')) (fun this_1 ↦ ne_of_lt        (gt_trans this_1.1 this_1.2) (Eq.symm this''))).1