Maximal ineq countable

theorem maximal_ineq_countable (hsub : Submartingale Y 𝓕 P) (hnonneg : 0 ≤ Y) (ε : ℝ≥0) (n : ι) :    -- We use `⨆ i : Set.Iic n` instead of `⨆ i ≤ n` because of incomplete API for `cbiSup`.    ε • P.real {ω | (ε : ℝ) ≤ ⨆ i : Set.Iic n, Y i ω} ≤      ∫ ω in {ω | (ε : ℝ) ≤ ⨆ i : Set.Iic n, Y i ω}, Y n ω ∂P := by  have (ω : Ω) : ⨆ i : Set.Iic n, Y i ω = (⨆ i ≤ n, ENNReal.ofReal (Y i ω)).toReal := by    rw [iSup_subtype', ENNReal.toReal_iSup]    · congr with i      rw [ENNReal.toReal_ofReal (hnonneg _ _)]    · finiteness  have : {ω | ε ≤ ⨆ i : Set.Iic n, Y i ω} =ᵐ[P] {ω | ε ≤ ⨆ i ≤ n, ENNReal.ofReal (Y i ω)} := by    filter_upwards [hsub.iSup_ofReal_ne_top hnonneg n] with ω htop    ext    change _ ≤ _ ↔ _ ≤ _    rw [← ENNReal.ofReal_coe_nnreal, ENNReal.ofReal_le_iff_le_toReal htop, this]  rw [measureReal_congr this, setIntegral_congr_set this]  exact maximal_ineq_countable_ennreal hsub hnonneg ε n