Is Stable left limit

lemma isStable_left_limit :    IsStable 𝓕 (fun (X : ι → Ω → E) ↦ ∀ ω, ∀ x, ∃ l, Tendsto (X · ω) (𝓝[<] x) (𝓝 l)) := by  refine isStable_pathwise (fun X i ↦ ∃ l, Tendsto X (𝓝[<] i) (𝓝 l)) (fun i ↦ ?_) ?_ ?_  · exact ⟨0, tendsto_const_nhds⟩  · intro X a hX i hai    cases lt_or_eq_of_le hai with    | inl hai =>      refine ⟨X a, ?_⟩      have h_eq : (fun x ↦ X (min x a)) =ᶠ[𝓝[<] i] fun _ ↦ X a := by        rw [eventuallyEq_nhdsWithin_iff]        filter_upwards [eventually_gt_nhds hai] with j haj        rw [min_eq_right haj.le]        grind      rw [tendsto_congr' h_eq]      exact tendsto_const_nhds    | inr hai =>      simp only [hai]      obtain ⟨l, hl⟩ := hX i      refine ⟨l, hl.congr' ?_⟩      rw [eventuallyEq_nhdsWithin_iff]      filter_upwards [] with j hji      rw [min_eq_left]      grind  · intro X Y i hXY    have h_eq : X =ᶠ[𝓝[<] i] Y := by      rw [eventuallyEq_nhdsWithin_iff]      obtain ⟨k, hik, hk⟩ := hXY      filter_upwards [eventually_lt_nhds hik] with j hjk _      exact hk j hjk    constructor <;> rintro ⟨l, hl⟩ <;> refine ⟨l, hl.congr' ?_⟩    · exact h_eq    · exact h_eq.symm