-- 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_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

Tactic:
refine monotone_nat_of_le_succ fun n => ?_

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))
n : ℕ
⊢ ∑ x ∈ Finset.range n, (μ (s (x + 1))).toReal ≤ ∑ x ∈ Finset.range (n + 1), (μ (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)
⊢ False

Tactic:
refine not_eventually.2 (Frequently.of_forall fun n => ?_) (htends B.toNNReal)

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 : B ∈ upperBounds (Set.range fun n => ∑ x ∈ Finset.range n, (μ (s (x + 1))).toReal)
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
⊢ Tendsto (fun n => ∑ k ∈ Finset.range n, μ (s (k + 1))) atTop (𝓝 (∑' (n : ℕ), μ (s (n + 1))))

Tactic:
exact ENNReal.tendsto_nat_tsum _

Result:
no goals

Proof state:
case h.refine_2.intro.hb
Ω : 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 ≤ B

Tactic:
exact le_trans (by positivity) hB

Result:
no goals

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 : ℕ
⊢ ¬↑B.toNNReal < ∑ k ∈ Finset.range n, μ (s (k + 1))

Tactic:
specialize hB (∑ k ∈ Finset.range n, μ (s (k + 1))).toReal _

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 : ℕ
⊢ (∑ k ∈ Finset.range n, μ (s (k + 1))).toReal ∈ Set.range fun n => ∑ x ∈ Finset.range n, (μ (s (x + 1))).toReal

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 : ℝ
n : ℕ
hB : (∑ k ∈ Finset.range n, μ (s (k + 1))).toReal ≤ B
⊢ ¬↑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
⊢ Tendsto (fun n => ∑ k ∈ Finset.range n, μ (s (k + 1))) atTop (𝓝 ⊤)

Tactic:
rw [← ENNReal.tsum_add_one_eq_top hs' (measure_ne_top _ _)]

Result:
Ω : 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 => ∑ k ∈ Finset.range n, μ (s (k + 1))) atTop (𝓝 (∑' (n : ℕ), μ (s (n + 1))))

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : ∑' (n : ℕ), μ (s n) = ⊤
⊢ μ (limsup s atTop) = 1

Tactic:
have : IsProbabilityMeasure μ := hs.isProbabilityMeasure

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : ∑' (n : ℕ), μ (s n) = ⊤
this : IsProbabilityMeasure μ
⊢ μ (limsup s atTop) = 1