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

Tactic:
rw [← sub_nonneg, Finset.sum_range_succ_sub_sum]

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 : ℕ
⊢ 0 ≤ (μ (s (n + 1))).toReal

Proof state:
Ω : 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

Tactic:
rw [measure_congr (eventuallyEq_set.2 (ae_mem_limsup_atTop_iff μ <|
  measurableSet_filtrationOfSet' hsm) : (limsup s atTop : Set Ω) =ᵐ[μ]
    {ω | Tendsto (fun n => ∑ k ∈ Finset.range n,
      (μ[(s (k + 1)).indicator (1 : Ω → ℝ)|filtrationOfSet hsm k]) ω) atTop atTop})]

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : ∑' (n : ℕ), μ (s n) = ⊤
this : IsProbabilityMeasure μ
⊢ μ {ω | Tendsto (fun n => ∑ k ∈ Finset.range n, (μ[(s (k + 1)).indicator 1|↑(filtrationOfSet hsm) k]) ω) atTop atTop} =
    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 => ∑ k ∈ Finset.range n, (μ[(s (k + 1)).indicator 1|↑(filtrationOfSet hsm) k]) ω) atTop atTop

Tactic:
simp_rw [hω]

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

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : ∑' (n : ℕ), μ (s n) = ⊤
this : IsProbabilityMeasure μ
⊢ {ω |
      Tendsto (fun n => ∑ k ∈ Finset.range n, (μ[(s (k + 1)).indicator 1|↑(filtrationOfSet hsm) k]) ω) atTop
        atTop} =ᶠ[ae μ]
    Set.univ

Tactic:
have : ∀ᵐ ω ∂μ, ∀ n, (μ[(s (n + 1)).indicator (1 : Ω → ℝ)|filtrationOfSet hsm n]) ω = _ :=
  ae_all_iff.2 fun n => hs.condExp_indicator_filtrationOfSet_ae_eq hsm n.lt_succ_self

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) ω
⊢ {ω |
      Tendsto (fun n => ∑ k ∈ Finset.range n, (μ[(s (k + 1)).indicator 1|↑(filtrationOfSet hsm) k]) ω) atTop
        atTop} =ᶠ[ae μ]
    Set.univ

Proof state:
case h.refine_2.intro.ha
Ω : 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
⊢ ∑ k ∈ Finset.range n, μ (s (k + 1)) ≠ ⊤

Tactic:
simp

Result:
no goals

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 :
  {ω |
      Tendsto (fun n => ∑ k ∈ Finset.range n, (μ[(s (k + 1)).indicator 1|↑(filtrationOfSet hsm) k]) ω) atTop
        atTop} =ᶠ[ae μ]
    Set.univ
⊢ μ {ω | Tendsto (fun n => ∑ k ∈ Finset.range n, (μ[(s (k + 1)).indicator 1|↑(filtrationOfSet hsm) k]) ω) atTop atTop} =
    1

Tactic:
rw [measure_congr this, measure_univ]

Result:
no goals

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) ω
⊢ {ω |
      Tendsto (fun n => ∑ k ∈ Finset.range n, (μ[(s (k + 1)).indicator 1|↑(filtrationOfSet hsm) k]) ω) atTop
        atTop} =ᶠ[ae μ]
    Set.univ

Tactic:
filter_upwards [this] with ω hω

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
⊢ {ω | Tendsto (fun n => ∑ k ∈ Finset.range n, (μ[(s (k + 1)).indicator 1|↑(filtrationOfSet hsm) k]) ω) atTop atTop} ω =
    Set.univ ω

Proof state:
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)

Tactic:
rintro ⟨B, 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 : B ∈ upperBounds (Set.range fun n => ∑ x ∈ Finset.range n, (μ (s (x + 1))).toReal)
⊢ False