Tendsto right Lim comp of lt

lemma tendsto_rightLim_comp_of_lt (hTd : Dense T) {T' : Set ι} (hTT' : T ⊆ T')    (hr : ∀ y, Tendsto h (𝓝[T ∩ Set.Ioi y] y) (𝓝 (r y))) {u : ℕ → ι} {L : ℝ}    (hux : ∀ k, u k < x) (hutend : Tendsto u atTop (𝓝 x))    (hL : Tendsto h (𝓝[T' ∩ Set.Iio x] x) (𝓝 L)) :    Tendsto (fun k ↦ r (u k)) atTop (𝓝 L) := by  rw [(closed_nhds_basis L).tendsto_right_iff]  rintro C ⟨hCmem, hCclosed⟩  have hev : ∀ᶠ s in 𝓝[<] x ⊓ 𝓟 T', h s ∈ C := by    rw [nhdsWithin_inf_principal, Set.inter_comm]; exact hL.eventually hCmem  obtain ⟨v, hvx, hv⟩ := (nhdsLT_basis_of_exists_lt ⟨u 0, hux 0⟩).eventually_iff.1    (Filter.eventually_inf_principal.1 hev)  have hevk : ∀ᶠ k in atTop, u k ∈ Set.Ioi v :=    hutend (IsOpen.mem_nhds isOpen_Ioi hvx)  filter_upwards [hevk] with k hk  have hne := nhdsWithin_Ioi_inter_neBot hTd (u k)  rw [Set.inter_comm] at hne  refine hCclosed.mem_of_tendsto (hr (u k)) ?_  rw [Set.inter_comm, ← nhdsWithin_inf_principal]  refine Filter.eventually_inf_principal.2 ?_  filter_upwards [Ioo_mem_nhdsGT (hux k)] with s hs hsT  exact hv ⟨hk.trans hs.1, hs.2⟩ (hTT' hsT)