Subseq Idx inherit step predicate

lemma subseqIdx_inherit_step_predicate {ℒ : Type*} [Nontrivial ℒ] [Lattice ℒ] [BoundedOrder ℒ](f : ℕ → ℒ) (hf0 : f 0 = ⊤) (atf : ∃ k, f k = ⊥) (hfat : Antitone f)(P : {z : ℒ × ℒ // z.1 < z.2} → Prop)(ho : ∀ i : ℕ, i < Nat.find atf → (hfi :f (i + 1) < f i) → P ⟨(f (i+1), f i),hfi⟩) :∀ i : ℕ, (hi : i < Nat.find (subseqIdx_hits_bot f atf hfat hf0)) →  P ⟨(f (subseqIdx f atf hfat (i + 1)), f (subseqIdx f atf hfat i)),    subseqIdx_strictAnti f hf0 atf hfat i (i + 1) (Nat.lt_succ_self i) (Nat.succ_le_iff.2 hi)⟩ := by  intro i hi  have hbot : f (subseqIdx f atf hfat i) ≠ ⊥ := by    intro h    exact (Nat.find_min (subseqIdx_hits_bot f atf hfat hf0) hi) h  let n := subseqIdx f atf hfat (i + 1)  have hn : subseqIdx f atf hfat i < n := by    dsimp [n]    rw [subseqIdx.succ_eq_find f atf hfat i hbot]    exact (Nat.find_spec (subseqIdx.next_exists f atf hfat i hbot)).1  have hstep : f n < f (subseqIdx f atf hfat i) := by    dsimp [n]    rw [subseqIdx.succ_eq_find f atf hfat i hbot]    exact (Nat.find_spec (subseqIdx.next_exists f atf hfat i hbot)).2  have hpred_eq : f (n - 1) = f (subseqIdx f atf hfat i) := by    apply subseqIdx.const_between f atf hfat i (n - 1)    repeat omega  have hpred_lt : f n < f (n - 1) := by rwa [hpred_eq]  have hpred_bd : n - 1 < Nat.find atf := by    by_contra hge    have hbot_pred : f (n - 1) = ⊥ := le_bot_iff.mp <| (Nat.find_spec atf) ▸ hfat (le_of_not_gt hge)    have hbot_n : f n = ⊥ := by      apply le_bot_iff.mp      exact (Nat.find_spec atf) ▸ hfat (le_trans (le_of_not_gt hge) (Nat.sub_le n 1))    exact (lt_self_iff_false ⊥).mp (hbot_n ▸ hbot_pred ▸ hpred_lt)  have hn_pos : 0 < n := by    exact lt_of_lt_of_le (Nat.zero_lt_succ i) <|      by simpa [n] using subseqIdx.ge_self f atf hfat (i + 1)  have hpred_lt' : f ((n - 1) + 1) < f (n - 1) := by    simpa [Nat.sub_add_cancel (Nat.succ_le_of_lt hn_pos)] using hpred_lt  convert ho (n - 1) hpred_bd hpred_lt' using 1  simp [n, hpred_eq, Nat.sub_add_cancel (Nat.succ_le_of_lt hn_pos)]