Measure Theory Submartingale i Sup of Real ne top

lemma _root_.MeasureTheory.Submartingale.iSup_ofReal_ne_top (hsub : Submartingale Y 𝓕 P)    (hnonneg : 0 ≤ Y) (n : ι) : ∀ᵐ ω ∂P, ⨆ i ≤ n, ENNReal.ofReal (Y i ω) ≠ ∞ := by  let supY (ω : Ω) := ⨆ i ≤ n, ENNReal.ofReal (Y i ω)  have hmeasY (i : ι) : Measurable (Y i) :=    (hsub.stronglyMeasurable i).measurable.mono (𝓕.le _) (le_refl _)  change P {ω | ¬supY ω ≠ ∞} = 0  push Not  convert Antitone.measure_iInter (s := fun ε : ℝ≥0 ↦ {ω | (ε : ℝ≥0∞) ≤ supY ω}) ?_ ?_ ?_  · ext ω    simp only [Set.mem_ofPred_eq, Set.mem_iInter]    constructor    · simp +contextual    · apply ENNReal.eq_top_of_forall_nnreal_le  · symm    erw [← le_bot_iff]    calc      _ ≤ ⨅ ε > (0 : ℝ≥0), ENNReal.ofReal (ε⁻¹ • ∫ ω in {ω | ε ≤ supY ω}, Y n ω ∂P) := by        gcongr with ε        refine le_iInf fun hε0 ↦ ?_        rw [ENNReal.ofReal_smul, le_inv_smul_iff_of_pos hε0, ENNReal.le_ofReal_iff_toReal_le]        · simp only [Measure.nnreal_smul_coe_apply, ENNReal.toReal_mul, ENNReal.coe_toReal]          exact maximal_ineq_countable_ennreal hsub hnonneg ε n        · finiteness        · exact setIntegral_nonneg (measurableSet_le measurable_const (by fun_prop))            fun ω _ ↦ hnonneg n ω      _ ≤ ⨅ ε > (0 : ℝ≥0), ENNReal.ofReal (ε⁻¹ • ∫ ω, Y n ω ∂P) := by        gcongr with ε hε0        · exact .of_forall (hnonneg n)        · exact hsub.integrable n        · exact P.restrict_le_self      _ = 0 := by        apply iInf_eq_of_tendsto        · intro ε₁ ε₂ h          refine le_iInf fun hε₁ ↦ ?_          simp only [iInf_pos (hε₁.trans_le h)]          gcongr          exact integral_nonneg (hnonneg n)        · convert (ENNReal.tendsto_ofReal ((tendsto_inv_atTop_zero (𝕜 := ℝ≥0)).smul_const            (∫ ω, Y n ω ∂P))).congr' ?_          · simp          · filter_upwards [eventually_gt_atTop 0] with ε hε0            simp [hε0]  · exact Set.monotone_preimage.comp_antitone ENNReal.coe_mono.Ici  · exact fun r ↦ (measurableSet_le measurable_const (by fun_prop)).nullMeasurableSet  · use 0; finiteness