awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
this_1 : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      Eq (α := ℝ) (μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω)
        ((fun (x : Ω) ↦ μ.real (s (n + 1))) ω)
ω : Ω
hω :
  ∀ (n : ℕ),
    μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω = μ.real (s (n + 1))
⊢ {ω : Ω |
        Tendsto (β := ℝ)
          (fun (n : ℕ) ↦
            ∑ k ∈ Finset.range n,
              μ[(s (k + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) k] ω)
          atTop atTop}
      ω =
    Set.univ ω

Tactic:
eq_true (?_ : Tendsto _ _ _)

Premises used: Set.univ, setOf, eq_true
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
this_1 : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      Eq (α := ℝ) (μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω)
        ((fun (x : Ω) ↦ μ.real (s (n + 1))) ω)
ω : Ω
hω :
  ∀ (n : ℕ),
    μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω = μ.real (s (n + 1))
h :
  Tendsto (β := ℝ)
    (fun (n : ℕ) ↦
      ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) k] ω)
    atTop atTop
⊢ {ω : Ω |
        Tendsto (β := ℝ)
          (fun (n : ℕ) ↦
            ∑ k ∈ Finset.range n,
              μ[(s (k + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) k] ω)
          atTop atTop}
      ω =
    Set.univ ω

Tactic:
refine eq_true (?_ : Tendsto _ _ _)

Premises used: eq_true
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
this_1 : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      Eq (α := ℝ) (μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω)
        ((fun (x : Ω) ↦ μ.real (s (n + 1))) ω)
ω : Ω
hω :
  ∀ (n : ℕ),
    μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω = μ.real (s (n + 1))
h : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1))) atTop atTop
⊢ Tendsto (β := ℝ)
    (fun (n : ℕ) ↦
      ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) k] ω)
    atTop atTop

Tactic:
simp_rw [hω]
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
this_1 : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      Eq (α := ℝ) (μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω)
        ((fun (x : Ω) ↦ μ.real (s (n + 1))) ω)
ω : Ω
hω :
  ∀ (n : ℕ),
    μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω = μ.real (s (n + 1))
rw :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))) atTop
    (𝓝 (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s (n + 1))))
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))) atTop (𝓝 ∞)

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

Premises used: ENNReal.tsum_add_one_eq_top, MeasureTheory.measure_ne_top
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
this_1 : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      Eq (α := ℝ) (μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω)
        ((fun (x : Ω) ↦ μ.real (s (n + 1))) ω)
ω : Ω
hω :
  ∀ (n : ℕ),
    μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω = μ.real (s (n + 1))
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))) atTop
    (𝓝 (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s (n + 1))))

Tactic:
ENNReal.tendsto_nat_tsum _

Premises used: ENNReal.tendsto_nat_tsum
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
this_1 : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      Eq (α := ℝ) (μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω)
        ((fun (x : Ω) ↦ μ.real (s (n + 1))) ω)
ω : Ω
hω :
  ∀ (n : ℕ),
    μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω = μ.real (s (n + 1))
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))) atTop
    (𝓝 (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s (n + 1))))

Tactic:
exact ENNReal.tendsto_nat_tsum _

Premises used: ENNReal.tendsto_nat_tsum
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
this_1 : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      Eq (α := ℝ) (μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω)
        ((fun (x : Ω) ↦ μ.real (s (n + 1))) ω)
ω : Ω
hω :
  ∀ (n : ℕ),
    μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω = μ.real (s (n + 1))
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))) 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 _
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
this_1 : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      Eq (α := ℝ) (μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω)
        ((fun (x : Ω) ↦ μ.real (s (n + 1))) ω)
ω : Ω
hω :
  ∀ (n : ℕ),
    μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω = μ.real (s (n + 1))
htends : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))) atTop (𝓝 ∞)
⊢ ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, (↑x : ℝ≥0∞) < ∑ k ∈ Finset.range a, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))

Tactic:
rw [ENNReal.tendsto_nhds_top_iff_nnreal] at htends

Premises used: ENNReal.tendsto_nhds_top_iff_nnreal
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
this_1 : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      Eq (α := ℝ) (μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω)
        ((fun (x : Ω) ↦ μ.real (s (n + 1))) ω)
ω : Ω
hω :
  ∀ (n : ℕ),
    μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, (↑x : ℝ≥0∞) < ∑ k ∈ Finset.range a, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1))) atTop atTop

Tactic:
tendsto_atTop_atTop_of_monotone' ?_ ?_

Premises used: Filter.tendsto_atTop_atTop_of_monotone'
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
this_1 : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      Eq (α := ℝ) (μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω)
        ((fun (x : Ω) ↦ μ.real (s (n + 1))) ω)
ω : Ω
hω :
  ∀ (n : ℕ),
    μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, (↑x : ℝ≥0∞) < ∑ k ∈ Finset.range a, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))
h : Monotone (β := ℝ) fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1))
h₁ : ¬BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1)))
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1))) atTop atTop

Tactic:
refine tendsto_atTop_atTop_of_monotone' ?_ ?_

Premises used: Filter.tendsto_atTop_atTop_of_monotone'
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
this_1 : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      Eq (α := ℝ) (μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω)
        ((fun (x : Ω) ↦ μ.real (s (n + 1))) ω)
ω : Ω
hω :
  ∀ (n : ℕ),
    μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, (↑x : ℝ≥0∞) < ∑ k ∈ Finset.range a, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))
⊢ Monotone (β := ℝ) fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1))

Tactic:
monotone_nat_of_le_succ fun n => ?_

Premises used: monotone_nat_of_le_succ
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
this_1 : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      Eq (α := ℝ) (μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω)
        ((fun (x : Ω) ↦ μ.real (s (n + 1))) ω)
ω : Ω
hω :
  ∀ (n : ℕ),
    μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, (↑x : ℝ≥0∞) < ∑ k ∈ Finset.range a, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))
h :
  ∀ (n : ℕ), LE.le (α := ℝ) (∑ x ∈ Finset.range n, μ.real (s (x + 1))) (∑ x ∈ Finset.range (n + 1), μ.real (s (x + 1)))
⊢ Monotone (β := ℝ) fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1))

Tactic:
refine monotone_nat_of_le_succ fun n => ?_

Premises used: monotone_nat_of_le_succ
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
this_1 : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      Eq (α := ℝ) (μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω)
        ((fun (x : Ω) ↦ μ.real (s (n + 1))) ω)
ω : Ω
hω :
  ∀ (n : ℕ),
    μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, (↑x : ℝ≥0∞) < ∑ k ∈ Finset.range a, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))
n : ℕ
h : 0 ≤ μ.real (s (n + 1))
⊢ LE.le (α := ℝ) (∑ x ∈ Finset.range n, μ.real (s (x + 1))) (∑ x ∈ Finset.range (n + 1), μ.real (s (x + 1)))

Tactic:
rw [← sub_nonneg, Finset.sum_range_succ_sub_sum]

Premises used: Finset.sum_range_succ_sub_sum, sub_nonneg
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
this_1 : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      Eq (α := ℝ) (μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω)
        ((fun (x : Ω) ↦ μ.real (s (n + 1))) ω)
ω : Ω
hω :
  ∀ (n : ℕ),
    μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, (↑x : ℝ≥0∞) < ∑ k ∈ Finset.range a, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))
n : ℕ
⊢ 0 ≤ μ.real (s (n + 1))

Tactic:
ENNReal.toReal_nonneg

Premises used: MeasureTheory.Measure.real, ENNReal.toReal_nonneg
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
this_1 : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      Eq (α := ℝ) (μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω)
        ((fun (x : Ω) ↦ μ.real (s (n + 1))) ω)
ω : Ω
hω :
  ∀ (n : ℕ),
    μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, (↑x : ℝ≥0∞) < ∑ k ∈ Finset.range a, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))
n : ℕ
⊢ 0 ≤ μ.real (s (n + 1))

Tactic:
exact ENNReal.toReal_nonneg

Premises used: ENNReal.toReal_nonneg
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
this_1 : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      Eq (α := ℝ) (μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω)
        ((fun (x : Ω) ↦ μ.real (s (n + 1))) ω)
ω : Ω
hω :
  ∀ (n : ℕ),
    μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, (↑x : ℝ≥0∞) < ∑ k ∈ Finset.range a, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))
B : ℝ
hB : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1)))) B
⊢ False

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

Premises used: Iff.mpr, Filter.Frequently.of_forall, Filter.not_eventually, Real.toNNReal
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
this_1 : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      Eq (α := ℝ) (μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω)
        ((fun (x : Ω) ↦ μ.real (s (n + 1))) ω)
ω : Ω
hω :
  ∀ (n : ℕ),
    μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, (↑x : ℝ≥0∞) < ∑ k ∈ Finset.range a, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))
B : ℝ
hB : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1)))) B
h : ∀ (n : ℕ), ¬(↑B.toNNReal : ℝ≥0∞) < ∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))
⊢ False

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

Premises used: Iff.mpr, Filter.Frequently.of_forall, Filter.not_eventually, Real.toNNReal
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
this_1 : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      Eq (α := ℝ) (μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω)
        ((fun (x : Ω) ↦ μ.real (s (n + 1))) ω)
ω : Ω
hω :
  ∀ (n : ℕ),
    μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, (↑x : ℝ≥0∞) < ∑ k ∈ Finset.range a, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))
B : ℝ
hB : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1)))) B
n : ℕ
h :
  ∀
    (hB :
      ∀ (x : ℝ),
        Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1))) x → x ≤ B)
    (n : ℕ), ¬(↑B.toNNReal : ℝ≥0∞) < ∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))
⊢ ¬(↑B.toNNReal : ℝ≥0∞) < ∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))

Tactic:
rw [mem_upperBounds] at hB

Premises used: mem_upperBounds
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
this_1 : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      Eq (α := ℝ) (μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω)
        ((fun (x : Ω) ↦ μ.real (s (n + 1))) ω)
ω : Ω
hω :
  ∀ (n : ℕ),
    μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, (↑x : ℝ≥0∞) < ∑ k ∈ Finset.range a, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))
B : ℝ
hB : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1))) x → x ≤ B
n : ℕ
h :
  Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1)))
    (ENNReal.toReal (∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))))
h₁ :
  ∀ (hB : ENNReal.toReal (∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))) ≤ B),
    ¬(↑B.toNNReal : ℝ≥0∞) < ∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))
⊢ ¬(↑B.toNNReal : ℝ≥0∞) < ∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))

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

Premises used: Finset.range, ENNReal.toReal, HAdd.hAdd, OfNat.ofNat, DFunLike.coe, Finset.sum
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
this_1 : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      Eq (α := ℝ) (μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω)
        ((fun (x : Ω) ↦ μ.real (s (n + 1))) ω)
ω : Ω
hω :
  ∀ (n : ℕ),
    μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, (↑x : ℝ≥0∞) < ∑ k ∈ Finset.range a, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))
B : ℝ
hB : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1))) x → x ≤ B
n : ℕ
⊢ Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1)))
    (ENNReal.toReal (∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))))

Tactic:
⟨n, ?_⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
this_1 : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      Eq (α := ℝ) (μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω)
        ((fun (x : Ω) ↦ μ.real (s (n + 1))) ω)
ω : Ω
hω :
  ∀ (n : ℕ),
    μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, (↑x : ℝ≥0∞) < ∑ k ∈ Finset.range a, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))
B : ℝ
hB : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1))) x → x ≤ B
n : ℕ
h :
  (fun (n : ℕ) ↦ (∑ x ∈ Finset.range n, μ.real (s (x + 1)) : ℝ)) n =
    ENNReal.toReal (∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1)))
⊢ Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1)))
    (ENNReal.toReal (∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))))

Tactic:
refine ⟨n, ?_⟩
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
this_1 : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      Eq (α := ℝ) (μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω)
        ((fun (x : Ω) ↦ μ.real (s (n + 1))) ω)
ω : Ω
hω :
  ∀ (n : ℕ),
    μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, (↑x : ℝ≥0∞) < ∑ k ∈ Finset.range a, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))
B : ℝ
hB : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1))) x → x ≤ B
n : ℕ
⊢ ∀ a ∈ Finset.range n, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s (a + 1)) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
this_1 : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      Eq (α := ℝ) (μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω)
        ((fun (x : Ω) ↦ μ.real (s (n + 1))) ω)
ω : Ω
hω :
  ∀ (n : ℕ),
    μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, (↑x : ℝ≥0∞) < ∑ k ∈ Finset.range a, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))
B : ℝ
hB : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1))) x → x ≤ B
n : ℕ
h :
  Eq (α := ℝ) ((fun (n : ℕ) ↦ (∑ x ∈ Finset.range n, μ.real (s (x + 1)) : ℝ)) n)
    (∑ a ∈ Finset.range n, ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) (s (a + 1))))
⊢ (fun (n : ℕ) ↦ (∑ x ∈ Finset.range n, μ.real (s (x + 1)) : ℝ)) n =
    ENNReal.toReal (∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1)))

Tactic:
rw [ENNReal.toReal_sum (by finiteness)]

Premises used: ENNReal.toReal_sum