-- Mathlib/Probability/BorelCantelli.lean
theorem measure_limsup_eq_one {s : ℕ → Set Ω} (hsm : ∀ n, MeasurableSet (s n)) (hs : iIndepSet s μ)
    (hs' : (∑' n, μ (s n)) = ∞) : μ (limsup s atTop) = 1

Proof state:
case h.refine_2.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : ∑' (n : ℕ), μ (s n) = ⊤
this✝ : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ), (μ[(s (n + 1)).indicator 1|↑(filtrationOfSet hsm) n]) ω = (fun x => (μ (s (n + 1))).toReal) ω
ω : Ω
hω : ∀ (n : ℕ), (μ[(s (n + 1)).indicator 1|↑(filtrationOfSet hsm) n]) ω = (μ (s (n + 1))).toReal
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, ↑x < ∑ k ∈ Finset.range a, μ (s (k + 1))
B : ℝ
hB : ∀ x ∈ Set.range fun n => ∑ x ∈ Finset.range n, (μ (s (x + 1))).toReal, x ≤ B
n : ℕ
⊢ (fun n => ∑ x ∈ Finset.range n, (μ (s (x + 1))).toReal) n = (∑ k ∈ Finset.range n, μ (s (k + 1))).toReal

Tactic:
rw [ENNReal.toReal_sum]

Result:
case h.refine_2.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : ∑' (n : ℕ), μ (s n) = ⊤
this✝ : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ), (μ[(s (n + 1)).indicator 1|↑(filtrationOfSet hsm) n]) ω = (fun x => (μ (s (n + 1))).toReal) ω
ω : Ω
hω : ∀ (n : ℕ), (μ[(s (n + 1)).indicator 1|↑(filtrationOfSet hsm) n]) ω = (μ (s (n + 1))).toReal
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, ↑x < ∑ k ∈ Finset.range a, μ (s (k + 1))
B : ℝ
hB : ∀ x ∈ Set.range fun n => ∑ x ∈ Finset.range n, (μ (s (x + 1))).toReal, x ≤ B
n : ℕ
⊢ ∀ a ∈ Finset.range n, μ (s (a + 1)) ≠ ⊤

Proof state:
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : ∑' (n : ℕ), μ (s n) = ⊤
this✝ : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ), (μ[(s (n + 1)).indicator 1|↑(filtrationOfSet hsm) n]) ω = (fun x => (μ (s (n + 1))).toReal) ω
ω : Ω
hω : ∀ (n : ℕ), (μ[(s (n + 1)).indicator 1|↑(filtrationOfSet hsm) n]) ω = (μ (s (n + 1))).toReal
⊢ Tendsto (fun n => ∑ x ∈ Finset.range n, (μ (s (x + 1))).toReal) atTop atTop

Tactic:
have htends : Tendsto (fun n => ∑ k ∈ Finset.range n, μ (s (k + 1))) atTop (𝓝 ∞) := by
  rw [← ENNReal.tsum_add_one_eq_top hs' (measure_ne_top _ _)]
  exact ENNReal.tendsto_nat_tsum _

Result:
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : ∑' (n : ℕ), μ (s n) = ⊤
this✝ : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ), (μ[(s (n + 1)).indicator 1|↑(filtrationOfSet hsm) n]) ω = (fun x => (μ (s (n + 1))).toReal) ω
ω : Ω
hω : ∀ (n : ℕ), (μ[(s (n + 1)).indicator 1|↑(filtrationOfSet hsm) n]) ω = (μ (s (n + 1))).toReal
htends : Tendsto (fun n => ∑ k ∈ Finset.range n, μ (s (k + 1))) atTop (𝓝 ⊤)
⊢ Tendsto (fun n => ∑ x ∈ Finset.range n, (μ (s (x + 1))).toReal) atTop atTop

Proof state:
case h.refine_2.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : ∑' (n : ℕ), μ (s n) = ⊤
this✝ : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ), (μ[(s (n + 1)).indicator 1|↑(filtrationOfSet hsm) n]) ω = (fun x => (μ (s (n + 1))).toReal) ω
ω : Ω
hω : ∀ (n : ℕ), (μ[(s (n + 1)).indicator 1|↑(filtrationOfSet hsm) n]) ω = (μ (s (n + 1))).toReal
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, ↑x < ∑ k ∈ Finset.range a, μ (s (k + 1))
B : ℝ
hB : ∀ x ∈ Set.range fun n => ∑ x ∈ Finset.range n, (μ (s (x + 1))).toReal, x ≤ B
n : ℕ
⊢ ∀ a ∈ Finset.range n, μ (s (a + 1)) ≠ ⊤

Tactic:
exact fun _ _ => measure_ne_top _ _

Result:
no goals

Proof state:
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : ∑' (n : ℕ), μ (s n) = ⊤
this✝ : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ), (μ[(s (n + 1)).indicator 1|↑(filtrationOfSet hsm) n]) ω = (fun x => (μ (s (n + 1))).toReal) ω
ω : Ω
hω : ∀ (n : ℕ), (μ[(s (n + 1)).indicator 1|↑(filtrationOfSet hsm) n]) ω = (μ (s (n + 1))).toReal
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, ↑x < ∑ k ∈ Finset.range a, μ (s (k + 1))
⊢ Tendsto (fun n => ∑ x ∈ Finset.range n, (μ (s (x + 1))).toReal) atTop atTop

Tactic:
refine tendsto_atTop_atTop_of_monotone' ?_ ?_

Result:
case h.refine_1
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : ∑' (n : ℕ), μ (s n) = ⊤
this✝ : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ), (μ[(s (n + 1)).indicator 1|↑(filtrationOfSet hsm) n]) ω = (fun x => (μ (s (n + 1))).toReal) ω
ω : Ω
hω : ∀ (n : ℕ), (μ[(s (n + 1)).indicator 1|↑(filtrationOfSet hsm) n]) ω = (μ (s (n + 1))).toReal
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, ↑x < ∑ k ∈ Finset.range a, μ (s (k + 1))
⊢ Monotone fun n => ∑ x ∈ Finset.range n, (μ (s (x + 1))).toReal

case h.refine_2
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : ∑' (n : ℕ), μ (s n) = ⊤
this✝ : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ), (μ[(s (n + 1)).indicator 1|↑(filtrationOfSet hsm) n]) ω = (fun x => (μ (s (n + 1))).toReal) ω
ω : Ω
hω : ∀ (n : ℕ), (μ[(s (n + 1)).indicator 1|↑(filtrationOfSet hsm) n]) ω = (μ (s (n + 1))).toReal
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, ↑x < ∑ k ∈ Finset.range a, μ (s (k + 1))
⊢ ¬BddAbove (Set.range fun n => ∑ x ∈ Finset.range n, (μ (s (x + 1))).toReal)

Proof state:
case h.refine_2.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : ∑' (n : ℕ), μ (s n) = ⊤
this✝ : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ), (μ[(s (n + 1)).indicator 1|↑(filtrationOfSet hsm) n]) ω = (fun x => (μ (s (n + 1))).toReal) ω
ω : Ω
hω : ∀ (n : ℕ), (μ[(s (n + 1)).indicator 1|↑(filtrationOfSet hsm) n]) ω = (μ (s (n + 1))).toReal
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, ↑x < ∑ k ∈ Finset.range a, μ (s (k + 1))
B : ℝ
hB : B ∈ upperBounds (Set.range fun n => ∑ x ∈ Finset.range n, (μ (s (x + 1))).toReal)
n : ℕ
⊢ ¬↑B.toNNReal < ∑ k ∈ Finset.range n, μ (s (k + 1))

Tactic:
rw [mem_upperBounds] at hB

Result:
case h.refine_2.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : ∑' (n : ℕ), μ (s n) = ⊤
this✝ : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ), (μ[(s (n + 1)).indicator 1|↑(filtrationOfSet hsm) n]) ω = (fun x => (μ (s (n + 1))).toReal) ω
ω : Ω
hω : ∀ (n : ℕ), (μ[(s (n + 1)).indicator 1|↑(filtrationOfSet hsm) n]) ω = (μ (s (n + 1))).toReal
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, ↑x < ∑ k ∈ Finset.range a, μ (s (k + 1))
B : ℝ
hB : ∀ x ∈ Set.range fun n => ∑ x ∈ Finset.range n, (μ (s (x + 1))).toReal, x ≤ B
n : ℕ
⊢ ¬↑B.toNNReal < ∑ k ∈ Finset.range n, μ (s (k + 1))

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : ∑' (n : ℕ), μ (s n) = ⊤
this✝ : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ), (μ[(s (n + 1)).indicator 1|↑(filtrationOfSet hsm) n]) ω = (fun x => (μ (s (n + 1))).toReal) ω
ω : Ω
hω : ∀ (n : ℕ), (μ[(s (n + 1)).indicator 1|↑(filtrationOfSet hsm) n]) ω = (μ (s (n + 1))).toReal
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, ↑x < ∑ k ∈ Finset.range a, μ (s (k + 1))
B : ℝ
n : ℕ
hB : (∑ k ∈ Finset.range n, μ (s (k + 1))).toReal ≤ B
⊢ 0 ≤ (∑ k ∈ Finset.range n, μ (s (k + 1))).toReal

Tactic:
positivity

Result:
no goals