-- Mathlib/Probability/Martingale/BorelCantelli.lean
theorem tendsto_sum_indicator_atTop_iff [IsFiniteMeasure μ]
    (hfmono : ∀ᵐ ω ∂μ, ∀ n, f n ω ≤ f (n + 1) ω) (hf : Adapted ℱ f) (hint : ∀ n, Integrable (f n) μ)
    (hbdd : ∀ᵐ ω ∂μ, ∀ n, |f (n + 1) ω - f n ω| ≤ R) :
    ∀ᵐ ω ∂μ, Tendsto (fun n => f n ω) atTop atTop ↔
      Tendsto (fun n => predictablePart f ℱ μ n ω) atTop atTop

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : Adapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ ↑R
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop atTop ↔ Tendsto (fun n => predictablePart f ℱ μ n ω) atTop atTop

Tactic:
have h₂ := (martingale_martingalePart hf hint).ae_not_tendsto_atTop_atBot
  (martingalePart_bdd_difference ℱ hbdd)

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : Adapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ ↑R
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop atTop ↔ Tendsto (fun n => predictablePart f ℱ μ n ω) atTop atTop

Proof state:
case h.mpr
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : Adapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ ↑R
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
ω : Ω
hω₁ : ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
hω₂ : ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
ht : Tendsto (fun n => predictablePart f ℱ μ n ω) atTop atTop
⊢ ¬BddAbove (Set.range fun n => f n ω)

Tactic:
rintro ⟨b, hbdd⟩

Result:
case h.mpr.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : Adapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd✝ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ ↑R
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
ω : Ω
hω₁ : ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
hω₂ : ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
ht : Tendsto (fun n => predictablePart f ℱ μ n ω) atTop atTop
b : ℝ
hbdd : b ∈ upperBounds (Set.range fun n => f n ω)
⊢ False

Proof state:
case h.mpr
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : Adapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ ↑R
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
ω : Ω
hω₁ : ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
hω₂ : ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
ht : Tendsto (fun n => predictablePart f ℱ μ n ω) atTop atTop
⊢ Tendsto (fun n => f n ω) atTop atTop

Tactic:
refine tendsto_atTop_atTop_of_monotone' (monotone_nat_of_le_succ hω₄) ?_

Result:
case h.mpr
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : Adapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ ↑R
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
ω : Ω
hω₁ : ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
hω₂ : ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
ht : Tendsto (fun n => predictablePart f ℱ μ n ω) atTop atTop
⊢ ¬BddAbove (Set.range fun n => f n ω)

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : Adapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ ↑R
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop atTop ↔ Tendsto (fun n => predictablePart f ℱ μ n ω) atTop atTop

Tactic:
have h₃ : ∀ᵐ ω ∂μ, ∀ n, 0 ≤ (μ[f (n + 1) - f n|ℱ n]) ω := by
  refine ae_all_iff.2 fun n => condExp_nonneg ?_
  filter_upwards [ae_all_iff.1 hfmono n] with ω hω using sub_nonneg.2 hω

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : Adapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ ↑R
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop atTop ↔ Tendsto (fun n => predictablePart f ℱ μ n ω) atTop atTop