Measure bi Union alt Set le

lemma measure_biUnion_altSet_le [IsFiniteMeasure μ]    (hX : IsRealQuasimartingale 𝓕 X μ)    (hab : a < b) (hm : 0 < m) (hT : T.Countable) (t : ι) :    μ (⋃ F ∈ {F : Finset ι | ↑F ⊆ T ∩ Set.Iic t}, altSet X F a b m)      ≤ ENNReal.ofReal ((variationBound X 𝓕 μ t + ∫ ω, (a - X t ω)⁺ ∂μ) / (b - a) / m) := by  have hcnt : {F : Finset ι | ↑F ⊆ T ∩ Set.Iic t}.Countable :=    countable_setOf_finset_coe_subset (hT.mono Set.inter_subset_left)  have hdir : DirectedOn (Function.onFun (· ⊆ ·) fun F : Finset ι ↦ altSet X F a b m)      {F : Finset ι | ↑F ⊆ T ∩ Set.Iic t} :=    fun F₁ h₁ F₂ h₂ ↦ ⟨F₁ ∪ F₂, by grind, altSet_mono subset_union_left,      altSet_mono subset_union_right⟩  rw [measure_biUnion_eq_iSup hcnt hdir]  refine iSup₂_le fun F hF ↦ ?_  have hF' : ∀ s ∈ F, s ≤ t := fun s hs ↦ (hF hs).2  calc μ (altSet X F a b m)  _ = ENNReal.ofReal (μ.real (altSet X F a b m)) :=    (ENNReal.ofReal_toReal (measure_ne_top μ _)).symm  _ ≤ _ := ENNReal.ofReal_le_ofReal (measureReal_altSet_le (μ := μ) hX.adapted hX.integrable        (hX.integral_indicator_le_variationBound t) hab hm hF')