Predictable Convex Step left Continuous

lemma predictableConvexStep_leftContinuous {ι Ω : Type*} [TopologicalSpace ι] [T1Space ι]    [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι]    [ClosedIicTopology ι]    {mΩ : MeasurableSpace Ω} {P : Measure Ω} [IsFiniteMeasure P] {S : ι → Ω → ℝ}    {𝓕 : Filtration ι mΩ} (hd : ClassD S 𝓕 P) (hs : Submartingale S 𝓕 P) (n : ℕ) (ω : Ω) (t : ι) :    ContinuousWithinAt (fun s ↦ predictableConvexStep hd hs n s ω) (Set.Iio t) t := by  have hrw : (fun s ↦ predictableConvexStep hd hs n s ω)      = fun s ↦ ∑ m ∈ (weight hd hs n).weights.support,          (weight hd hs n).weights m • predictableSeqStep P S 𝓕 m s ω := by    funext s    simp only [predictableConvexStep, Finsupp.sum, Finset.sum_apply, Pi.smul_apply]  rw [hrw]  exact tendsto_finsetSum _ fun m _ ↦ (predictableSeqStep_leftContinuous m ω t).fun_const_smul _