Tendsto right Lim nhds LT

lemma tendsto_rightLim_nhdsLT (hTd : Dense T)    (hr : ∀ᶠ y in 𝓝[<] x, Tendsto h (𝓝[T ∩ Set.Ioi y] y) (𝓝 (r y))) {L : ℝ}    (hL : Tendsto h (𝓝[T ∩ Set.Iio x] x) (𝓝 L)) :    Tendsto r (𝓝[<] x) (𝓝 L) := by  by_cases hex : ∃ u, u < x  swap  · have hempty : Set.Iio x = ∅ := Set.eq_empty_iff_forall_notMem.2      (fun u hu ↦ hex ⟨u, hu⟩)    rw [nhdsWithin, hempty, Filter.principal_empty, inf_bot_eq]    exact tendsto_bot  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 hex).eventually_iff.1    (Filter.eventually_inf_principal.1 hev)  filter_upwards [Ioo_mem_nhdsLT hvx, hr] with y hy hr  have hne := nhdsWithin_Ioi_inter_neBot hTd y  rw [Set.inter_comm] at hne  refine hCclosed.mem_of_tendsto hr ?_  rw [Set.inter_comm, ← nhdsWithin_inf_principal]  refine Filter.eventually_inf_principal.2 ?_  filter_upwards [Ioo_mem_nhdsGT hy.2] with s hs hsT  exact hv ⟨hy.1.trans hs.1, hs.2⟩ hsT