Dense monotone of is Right Continuous

lemma Dense.monotone_of_isRightContinuous {α β : Type*} [LinearOrder α] [OrderTop α]    [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] [TopologicalSpace β]    [Preorder β] [t : OrderClosedTopology β] {f : α → β} {D : Set α} (hD : Dense D) (htop : ⊤ ∈ D)    (hm : Monotone (f ∘ (↑) : D → β)) (hf : f.IsRightContinuous) :    Monotone f := by  refine monotone_iff_forall_lt.2 fun a b hab => ?_  by_cases! hbtop : b = ⊤  · have : (comap ((↑) : D → α) (𝓝[>] a)).NeBot := hD.comap_val_nhdsWithin_Ioi_neBot hab    rw [hbtop]    refine (isClosed_Iic (a := f ⊤)).mem_of_tendsto (Tendsto.comp (hf a)      (tendsto_comap (f := ((↑) : D → α)))) ?_    rw [eventually_comap, eventually_nhdsWithin_iff]    filter_upwards with z hz d rfl using hm (Subtype.mk_le_mk.2 le_top : d ≤ ⟨⊤, htop⟩)  · -- This part should work when `α` satisfies `NoTopOrder α`.    let I : D × D → α × α := Prod.map Subtype.val Subtype.val    have : ((𝓝[Set.Ioi a ×ˢ Set.Ioi b] ⟨a, b⟩).comap I).NeBot := by      simp only [nhdsWithin_prod_eq, comap_prodMap_prod, I]      exact (hD.comap_val_nhdsWithin_Ioi_neBot hab).prod        (hD.comap_val_nhdsWithin_Ioi_neBot hbtop.lt_top)    have : ∀ᶠ (p : D × D) in (𝓝[Set.Ioi a ×ˢ Set.Ioi b] ⟨a, b⟩).comap I, p.1 ≤ p.2 := by      rw [eventually_comap, eventually_nhdsWithin_iff]      have := isOpen_lt_prod.mem_nhds_iff.2 (by simp [hab] : ⟨a, b⟩ ∈ {p : α × α | p.1 < p.2})      filter_upwards [this] with p hlt _ a rfl using hlt.le    exact t.isClosed_le'.mem_of_tendsto (Tendsto.comp ((hf a).prodMap (hf b)) tendsto_comap)      (this.mono fun d hd => hm hd)