Predictable Seq Step left Continuous

lemma predictableSeqStep_leftContinuous {ι Ω : Type*} [TopologicalSpace ι]    [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι]    [ClosedIicTopology ι]    {mΩ : MeasurableSpace Ω} {P : Measure Ω} {S : ι → Ω → ℝ}    {𝓕 : Filtration ι mΩ} (n : ℕ) (ω : Ω) (t : ι) :    ContinuousWithinAt (fun s ↦ predictableSeqStep P S 𝓕 n s ω) (Set.Iio t) t := by  have hrw : (fun s ↦ predictableSeqStep P S 𝓕 n s ω)      = fun s ↦ ∑ u : mesh ι n, (meshPredIoc n u).indicator          (fun _ : ι ↦ predictablePart (S ∘ Subtype.val) (meshFiltration 𝓕 n) P u ω) s := by    funext s    simp only [predictableSeqStep, Finset.sum_apply]    exact Finset.sum_congr rfl fun u _ ↦ Set.indicator_apply_apply _ _ s ω  rw [hrw]  exact tendsto_finsetSum _ fun u _ ↦ continuousWithinAt_Iio_indicator_Ioc _ _ _ t