-- Mathlib/Probability/StrongLaw.lean
theorem strong_law_aux5 :
    ∀ᵐ ω, (fun n : ℕ => ∑ i ∈ range n, truncation (X i) i ω - ∑ i ∈ range n, X i ω) =o[atTop]
    fun n : ℕ => (n : ℝ)

Proof state:
case h
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A : ∑' (j : ℕ), ℙ {ω | X j ω ∈ Set.Ioi ↑j} < ⊤
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, X n ω ∉ Set.Ioi ↑n
n : ℕ
hn : X n ω ∉ Set.Ioi ↑n
npos : n ∈ Set.Ioi 0
⊢ 0 = (if -↑n < X n ω ∧ X n ω ≤ ↑n then X n ω else 0) - X n ω

Tactic:
split_ifs with h

Result:
case pos
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A : ∑' (j : ℕ), ℙ {ω | X j ω ∈ Set.Ioi ↑j} < ⊤
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, X n ω ∉ Set.Ioi ↑n
n : ℕ
hn : X n ω ∉ Set.Ioi ↑n
npos : n ∈ Set.Ioi 0
h : -↑n < X n ω ∧ X n ω ≤ ↑n
⊢ 0 = X n ω - X n ω

case neg
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A : ∑' (j : ℕ), ℙ {ω | X j ω ∈ Set.Ioi ↑j} < ⊤
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, X n ω ∉ Set.Ioi ↑n
n : ℕ
hn : X n ω ∉ Set.Ioi ↑n
npos : n ∈ Set.Ioi 0
h : ¬(-↑n < X n ω ∧ X n ω ≤ ↑n)
⊢ 0 = 0 - X n ω

Proof state:
case h.e'_3.h.e'_5
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
⊢ (fun j => ℙ {ω | X j ω ∈ Set.Ioi ↑j}) = fun j => ℙ {ω | X 0 ω ∈ Set.Ioi ↑j}

Tactic:
ext1 j

Result:
case h.e'_3.h.e'_5.h
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
j : ℕ
⊢ ℙ {ω | X j ω ∈ Set.Ioi ↑j} = ℙ {ω | X 0 ω ∈ Set.Ioi ↑j}

Proof state:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
⊢ ∀ᵐ (ω : Ω), (fun n => ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) =o[atTop] fun n => ↑n

Tactic:
have A : (∑' j : ℕ, ℙ {ω | X j ω ∈ Set.Ioi (j : ℝ)}) < ∞ := by
  convert tsum_prob_mem_Ioi_lt_top hint (hnonneg 0) using 2
  ext1 j
  exact (hident j).measure_mem_eq measurableSet_Ioi

Result:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A : ∑' (j : ℕ), ℙ {ω | X j ω ∈ Set.Ioi ↑j} < ⊤
⊢ ∀ᵐ (ω : Ω), (fun n => ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) =o[atTop] fun n => ↑n

Proof state:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
⊢ ∑' (j : ℕ), ℙ {ω | X j ω ∈ Set.Ioi ↑j} < ⊤

Tactic:
convert tsum_prob_mem_Ioi_lt_top hint (hnonneg 0) using 2

Result:
case h.e'_3.h.e'_5
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
⊢ (fun j => ℙ {ω | X j ω ∈ Set.Ioi ↑j}) = fun j => ℙ {ω | X 0 ω ∈ Set.Ioi ↑j}

Proof state:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A : ∑' (j : ℕ), ℙ {ω | X j ω ∈ Set.Ioi ↑j} < ⊤
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, X n ω ∉ Set.Ioi ↑n
⊢ (fun x => 0) =ᶠ[atTop] fun n => truncation (X n) (↑n) ω - X n ω

Tactic:
filter_upwards [hω, Ioi_mem_atTop 0] with n hn npos

Result:
case h
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A : ∑' (j : ℕ), ℙ {ω | X j ω ∈ Set.Ioi ↑j} < ⊤
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, X n ω ∉ Set.Ioi ↑n
n : ℕ
hn : X n ω ∉ Set.Ioi ↑n
npos : n ∈ Set.Ioi 0
⊢ 0 = truncation (X n) (↑n) ω - X n ω

Proof state:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A : ∑' (j : ℕ), ℙ {ω | X j ω ∈ Set.Ioi ↑j} < ⊤
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, X n ω ∉ Set.Ioi ↑n
n : ℕ
hn : X n ω ∉ Set.Ioi ↑n
npos : n ∈ Set.Ioi 0
h : ¬(-↑n < X n ω ∧ X n ω ≤ ↑n)
⊢ -↑n < 0

Tactic:
simpa only [Right.neg_neg_iff, Nat.cast_pos] using npos

Result:
no goals

Proof state:
case h.e'_3.h.e'_5.h
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
j : ℕ
⊢ ℙ {ω | X j ω ∈ Set.Ioi ↑j} = ℙ {ω | X 0 ω ∈ Set.Ioi ↑j}

Tactic:
exact (hident j).measure_mem_eq measurableSet_Ioi

Result:
no goals

Proof state:
case neg
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A : ∑' (j : ℕ), ℙ {ω | X j ω ∈ Set.Ioi ↑j} < ⊤
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, X n ω ∉ Set.Ioi ↑n
n : ℕ
hn : X n ω ∉ Set.Ioi ↑n
npos : n ∈ Set.Ioi 0
h : ¬(-↑n < X n ω ∧ X n ω ≤ ↑n)
this : -↑n < X n ω
⊢ 0 = 0 - X n ω

Tactic:
simp only [this, true_and, not_le] at h

Result:
case neg
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A : ∑' (j : ℕ), ℙ {ω | X j ω ∈ Set.Ioi ↑j} < ⊤
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, X n ω ∉ Set.Ioi ↑n
n : ℕ
hn : X n ω ∉ Set.Ioi ↑n
npos : n ∈ Set.Ioi 0
this : -↑n < X n ω
h : ↑n < X n ω
⊢ 0 = 0 - X n ω

Proof state:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A : ∑' (j : ℕ), ℙ {ω | X j ω ∈ Set.Ioi ↑j} < ⊤
B : ∀ᵐ (ω : Ω), Tendsto (fun n => truncation (X n) (↑n) ω - X n ω) atTop (𝓝 0)
⊢ ∀ᵐ (ω : Ω), (fun n => ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) =o[atTop] fun n => ↑n

Tactic:
filter_upwards [B] with ω hω

Result:
case h
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A : ∑' (j : ℕ), ℙ {ω | X j ω ∈ Set.Ioi ↑j} < ⊤
B : ∀ᵐ (ω : Ω), Tendsto (fun n => truncation (X n) (↑n) ω - X n ω) atTop (𝓝 0)
ω : Ω
hω : Tendsto (fun n => truncation (X n) (↑n) ω - X n ω) atTop (𝓝 0)
⊢ (fun n => ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) =o[atTop] fun n => ↑n