Measure infinite Alt

lemma measure_infiniteAlt [IsFiniteMeasure μ]    (hX : IsRealQuasimartingale 𝓕 X μ) (hab : a < b) (hT : T.Countable) :    μ (infiniteAlt T t X a b) = 0 := by  suffices μ (⋂ m : ℕ, ⋃ F ∈ {F : Finset ι | ↑F ⊆ T ∩ Set.Iic t}, altSet X F a b (m + 1)) = 0 by    refine measure_mono_null ?_ this    intro ω    simp only [infiniteAlt, Set.subset_inter_iff, Set.mem_ofPred_eq, Set.mem_iInter, Set.mem_iUnion,      exists_prop]    exact fun h i ↦ h (i + 1)  refine le_antisymm ?_ zero_le  have hbound : ∀ m : ℕ,      μ (⋂ m : ℕ, ⋃ F ∈ {F : Finset ι | ↑F ⊆ T ∩ Set.Iic t}, altSet X F a b (m + 1))        ≤ ENNReal.ofReal ((variationBound X 𝓕 μ t + ∫ ω, (a - X t ω)⁺ ∂μ) / (b - a) / (m + 1)) := by    intro m    refine (measure_mono (Set.iInter_subset _ m)).trans ?_    have := measure_biUnion_altSet_le (μ := μ) hX hab (Nat.succ_pos m) hT t    simpa using this  have hlim : Tendsto (fun m : ℕ ↦      ENNReal.ofReal ((variationBound X 𝓕 μ t + ∫ ω, (a - X t ω)⁺ ∂μ) / (b - a) / (m + 1)))        atTop (𝓝 0) := by    rw [← ENNReal.ofReal_zero]    refine (ENNReal.continuous_ofReal.tendsto 0).comp ?_    have h1 : Tendsto (fun n : ℕ ↦ ((variationBound X 𝓕 μ t + ∫ ω, (a - X t ω)⁺ ∂μ) / (b - a)) / n)        atTop (𝓝 0) := tendsto_const_div_atTop_nhds_zero_nat _    have h2 := h1.comp (tendsto_add_atTop_nat 1)    refine h2.congr fun m ↦ ?_    simp [Function.comp, div_div]  exact ge_of_tendsto' hlim hbound