Subseq Idx find ne of plateau

lemma subseqIdx_find_ne_of_plateau {ℒ : Type*} [Nontrivial ℒ] [Lattice ℒ] [BoundedOrder ℒ](f : ℕ → ℒ) (hf0 : f 0 = ⊤) (atf : ∃ k, f k = ⊥) (hfat : Antitone f) (k : ℕ) (hk : f k = ⊥)(htech : ∃ N : ℕ, N + 1 ≤ k ∧ f N = f (N + 1)) :  (Nat.find <| subseqIdx_hits_bot f atf hfat hf0) ≠ k := by  let A := Nat.find <| subseqIdx_hits_bot f atf hfat hf0  let 𝒮 := {f t | (t ≤ k)}  have helper : ∀ t : ℕ, ∃ l : ℕ, l ≤ k ∧ f (subseqIdx f atf hfat t) = f l := by    intro t    if hcond : f (subseqIdx f atf hfat t) = ⊥ then exact ⟨k,⟨le_rfl,hcond ▸ hk.symm⟩⟩    else      refine ⟨subseqIdx f atf hfat t, ?_, rfl⟩      by_contra hlt      exact hcond <| le_bot_iff.mp <| hk ▸ hfat (le_of_lt (lt_of_not_ge hlt))  let Φ : Fin (A+1) → 𝒮 := fun d ↦    let l := (helper d).choose    let hl := (helper d).choose_spec    ⟨f (subseqIdx f atf hfat d), Set.mem_setOf.mpr ⟨l, ⟨hl.1, hl.2.symm⟩⟩⟩  have hΦ : Function.Injective Φ := by    intro d1 d2 h    have this : f (subseqIdx f atf hfat d1) = f (subseqIdx f atf hfat d2) := by      exact congrArg Subtype.val h    if hd : d1 < d2 then      have hlt' := subseqIdx_strictAnti f hf0 atf hfat d1 d2 hd (Fin.is_le d2)      simp [this] at hlt'    else      if hd' : d2 < d1 then        have hlt' := subseqIdx_strictAnti f hf0 atf hfat d2 d1 hd' (Fin.is_le d1)        simp [this] at hlt'      else exact Fin.le_antisymm (le_of_not_gt hd') (le_of_not_gt hd)  let fS : Fin (k+1) → 𝒮 := fun n ↦ ⟨f n,Set.mem_setOf.mpr ⟨n,⟨Fin.is_le n,rfl⟩⟩⟩  have fSsuj : Function.Surjective fS := by    intro y    rcases y.prop.out with ⟨n1,n2,n3⟩    use ⟨n1,Nat.lt_succ_of_le n2⟩, SetCoe.ext n3  have : Fintype 𝒮 :=  Set.Finite.fintype <| Finite.of_surjective fS fSsuj  have ineq1: A + 1 ≤ Fintype.card ↑𝒮 := Fintype.card_fin (A+1) ▸ Fintype.card_le_of_injective Φ hΦ  have ineq2 : Fintype.card ↑𝒮 < k + 1 := Fintype.card_fin (k+1) ▸    Fintype.card_lt_of_surjective_not_injective fS fSsuj <| Function.not_injective_iff.mpr    ⟨⟨htech.choose,Nat.lt_add_right 1 htech.choose_spec.1⟩, ⟨htech.choose+1,Nat.add_lt_add_right    htech.choose_spec.1 1⟩,⟨SetCoe.ext htech.choose_spec.2,by simp⟩⟩  exact ne_of_lt <| Nat.succ_lt_succ_iff.mp <| lt_of_le_of_lt ineq1 ineq2