awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Zorn (goal)
Goal:
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s : Set α | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) cs
s : Set α
hs : s ∈ cs
y : α
sy : Set α
hsy : sy ∈ cs
hysy : y ∈ sy
z : α
sz : Set α
hsz : sz ∈ cs
hzsz : z ∈ sz
hyz : y ≠ z
hsseq : sy ≠ sz
refine_1 : ∀ (h : sy ⊆ sz), r y z ∨ r z y
⊢ r y z ∨ r z y
have refine_1₁ : ∀ (h : sz ⊆ sy), r y z ∨ r z y
Tactic: rcases hcs₁ hsy hsz hsseq with h | h
-- Lean 4 proof step from Mathlib.Order.ZornAtoms (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderTop α
h : ∀ (c : Set α), IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ (x : α), x ≠ ⊤ ∧ x ∈ upperBounds c
⊢ IsCoatomic α
have refine : ∀ (x : α) (hx : x < ⊤), ∃ (a : α), IsCoatom a ∧ x ≤ a
Tactic: refine ⟨fun x => le_top.eq_or_lt.imp_right fun hx => ?_⟩
-- Lean 4 proof step from Mathlib.Order.ZornAtoms (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderTop α
h : ∀ (c : Set α), IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ (x : α), x ≠ ⊤ ∧ x ∈ upperBounds c
x : α
hx : x < ⊤
⊢ ∃ (a : α), IsCoatom a ∧ x ≤ a
have refine_2 : ∀ (this : ∃ (m : α), x ≤ m ∧ Maximal (fun (x_1 : α) ↦ x_1 ∈ Ico x ⊤) m), ∃ (a : α), IsCoatom a ∧ x ≤ a
Tactic: have := zorn_le_nonempty₀ (Ico x ⊤) (fun c hxc hc y hy => ?_) x (left_mem_Ico.2 hx)
-- Lean 4 proof step from Mathlib.Order.ZornAtoms (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderTop α
h : ∀ (c : Set α), IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ (x : α), x ≠ ⊤ ∧ x ∈ upperBounds c
x : α
hx : x < ⊤
refine_2 : ∀ (this : ∃ (m : α), x ≤ m ∧ Maximal (fun (x_1 : α) ↦ x_1 ∈ Ico x ⊤) m), ∃ (a : α), IsCoatom a ∧ x ≤ a
⊢ ∃ (a : α), IsCoatom a ∧ x ≤ a
have refine_1 : ∀ (c : Set α) (hxc : c ⊆ Ico x ⊤) (hc : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c) (y : α) (hy : y ∈ c),
  ∃ ub ∈ Ico x ⊤, ∀ z ∈ c, z ≤ ub
Tactic: have := zorn_le_nonempty₀ (Ico x ⊤) (fun c hxc hc y hy => ?_) x (left_mem_Ico.2 hx)
-- Lean 4 proof step from Mathlib.Order.ZornAtoms (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderTop α
h : ∀ (c : Set α), IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ (x : α), x ≠ ⊤ ∧ x ∈ upperBounds c
x : α
hx : x < ⊤
this : ∃ (m : α), x ≤ m ∧ Maximal (fun (x_1 : α) ↦ x_1 ∈ Ico x ⊤) m
⊢ ∃ (a : α), IsCoatom a ∧ x ≤ a
have refine_2 : ∀ (y : α) (hxy : x ≤ y) (hmax : Maximal (fun (x_1 : α) ↦ x_1 ∈ Ico x ⊤) y), ∃ (a : α), IsCoatom a ∧ x ≤ a
Tactic: obtain ⟨y, hxy, hmax⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.ZornAtoms (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderTop α
h : ∀ (c : Set α), IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ (x : α), x ≠ ⊤ ∧ x ∈ upperBounds c
x : α
hx : x < ⊤
y : α
hxy : x ≤ y
hmax : Maximal (fun (x_1 : α) ↦ x_1 ∈ Ico x ⊤) y
⊢ ∃ (a : α), IsCoatom a ∧ x ≤ a
have refine_2 : ∀ (z : α) (hyz : y < z) (hz : z < ⊤), False
Tactic: refine ⟨y, ⟨hmax.prop.2.ne, fun z hyz ↦ le_top.eq_or_lt.resolve_right fun hz => ?_⟩, hxy⟩
-- Lean 4 proof step from Mathlib.Order.ZornAtoms (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderTop α
h : ∀ (c : Set α), IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ (x : α), x ≠ ⊤ ∧ x ∈ upperBounds c
x : α
hx : x < ⊤
c : Set α
hxc : c ⊆ Ico x ⊤
hc : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c
y : α
hy : y ∈ c
⊢ ∃ ub ∈ Ico x ⊤, ∀ z ∈ c, z ≤ ub
have refine_1 : ∀ (z : α) (hz : z ≠ ⊤) (hcz : z ∈ upperBounds c), ∃ ub ∈ Ico x ⊤, ∀ z ∈ c, z ≤ ub
Tactic: rcases h c hc ⟨y, hy⟩ fun h => (hxc h).2.ne rfl with ⟨z, hz, hcz⟩
-- Lean 4 proof step from Mathlib.Probability.BorelCantelli (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
β : Type u_3
inst : LinearOrder ι
mβ : MeasurableSpace β
inst_1 : NormedAddCommGroup β
inst_2 : BorelSpace β
f : ι → Ω → β
i j : ι
hf : ∀ (i : ι), StronglyMeasurable (f i)
hfi : iIndepFun (β := fun (x : ι) ↦ β) f μ
hij : i < j
this :
  Indep (⨆ (k : ι), ⨆ (_ : Membership.mem (γ := Set ι) {j} k), MeasurableSpace.comap (f k) mβ)
    (⨆ (k : ι), ⨆ (_ : Membership.mem (γ := Set ι) {k : ι | k ≤ i} k), MeasurableSpace.comap (f k) mβ) μ
⊢ Indep (MeasurableSpace.comap (f j) mβ) ((↑(Filtration.natural (β := fun (i : ι) ↦ β) f hf) : ι → MeasurableSpace Ω) i)
    μ
have rwa : ∀
  (this :
    Indep (MeasurableSpace.comap (f j) mβ)
      (⨆ (k : ι), ⨆ (_ : Membership.mem (γ := Set ι) {k : ι | k ≤ i} k), MeasurableSpace.comap (f k) mβ) μ),
  Indep (MeasurableSpace.comap (f j) mβ) ((↑(Filtration.natural (β := fun (i : ι) ↦ β) f hf) : ι → MeasurableSpace Ω) i)
    μ
Tactic: rwa [iSup_singleton] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Probability.BorelCantelli (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
β : Type u_3
inst : LinearOrder ι
mβ : MeasurableSpace β
inst_1 : NormedAddCommGroup β
inst_2 : BorelSpace β
f : ι → Ω → β
i j : ι
hf : ∀ (i : ι), StronglyMeasurable (f i)
hfi : iIndepFun (β := fun (x : ι) ↦ β) f μ
hij : i < j
⊢ Indep (MeasurableSpace.comap (f j) mβ) ((↑(Filtration.natural (β := fun (i : ι) ↦ β) f hf) : ι → MeasurableSpace Ω) i)
    μ
have suffices : Indep (⨆ (k : ι), ⨆ (_ : Membership.mem (γ := Set ι) {j} k), MeasurableSpace.comap (f k) mβ)
  (⨆ (k : ι), ⨆ (_ : Membership.mem (γ := Set ι) {k : ι | k ≤ i} k), MeasurableSpace.comap (f k) mβ) μ
Tactic: suffices Indep (⨆ k ∈ ({j} : Set ι), MeasurableSpace.comap (f k) mβ)
      (⨆ k ∈ {k | k ≤ i}, MeasurableSpace.comap (f k) mβ) μ by rwa [iSup_singleton] at this
-- Lean 4 proof step from Mathlib.Probability.BorelCantelli (hypothesis)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
β : Type u_3
inst : LinearOrder ι
mβ : MeasurableSpace β
inst_1 : NormedAddCommGroup β
inst_2 : BorelSpace β
f : ι → Ω → β
i j : ι
inst_3 : SecondCountableTopology β
inst_4 : CompleteSpace β
inst_5 : NormedSpace ℝ β
hf : ∀ (i : ι), StronglyMeasurable (f i)
hfi : iIndepFun (β := fun (x : ι) ↦ β) f μ
hij : i < j
⊢ μ[f j | (↑(Filtration.natural (β := fun (i : ι) ↦ β) f hf) : ι → MeasurableSpace Ω) i] =ᶠ[ae μ] fun (x : Ω) ↦
    ∫ (x : Ω), f j x ∂μ
have this : IsProbabilityMeasure μ
Tactic: have : IsProbabilityMeasure μ := hfi.isProbabilityMeasure
-- Lean 4 proof step from Mathlib.Probability.BorelCantelli (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
inst : LinearOrder ι
i j : ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s μ
hij : i < j
⊢ (ae μ).EventuallyEq (β := ℝ)
    μ[(s j).indicator fun (x : Ω) ↦ 1 | (↑(filtrationOfSet (s := s) hsm) : ι → MeasurableSpace Ω) i] fun (x : Ω) ↦
    μ.real (s j)
have rw : (ae μ).EventuallyEq (β := ℝ)
  μ[(s j).indicator fun (x : Ω) ↦ 1 |
    (↑(Filtration.natural (β := fun (x : ι) ↦ ℝ) (fun (i : ι) ↦ (s i).indicator fun (x : Ω) ↦ 1) sorry) :
        ι → MeasurableSpace Ω)
      i]
  fun (x : Ω) ↦ μ.real (s j)
Tactic: rw [Filtration.filtrationOfSet_eq_natural (β := fun _ ↦ ℝ) hsm]
-- Lean 4 proof step from Mathlib.Probability.BorelCantelli (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
inst : LinearOrder ι
i j : ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s μ
hij : i < j
⊢ (ae μ).EventuallyEq (β := ℝ)
    μ[(s j).indicator fun (x : Ω) ↦ 1 |
      (↑(Filtration.natural (β := fun (x : ι) ↦ ℝ) (fun (i : ι) ↦ (s i).indicator fun (x : Ω) ↦ 1) ⋯) :
          ι → MeasurableSpace Ω)
        i]
    fun (x : Ω) ↦ μ.real (s j)
have refine : (ae μ).EventuallyEq (β := ℝ) (fun (x : Ω) ↦ ∫ (x : Ω), (s j).indicator (fun (_ω : Ω) ↦ 1) x ∂μ) fun (x : Ω) ↦
  μ.real (s j)
Tactic: refine (iIndepFun.condExp_natural_ae_eq_of_lt _ hs.iIndepFun_indicator hij).trans ?_
-- Lean 4 proof step from Mathlib.Probability.BorelCantelli (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
inst : LinearOrder ι
i j : ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s μ
hij : i < j
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : Ω) ↦ ∫ (x : Ω), (s j).indicator (fun (_ω : Ω) ↦ 1) x ∂μ) fun (x : Ω) ↦
    μ.real (s j)
have simp : (ae μ).EventuallyEq (β := ℝ) (fun (x : Ω) ↦ μ.real (s j)) fun (x : Ω) ↦ μ.real (s j)
Tactic: simp only [integral_indicator_const _ (hsm _), smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Probability.BorelCantelli (hypothesis)
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)) ∞
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (limsup s atTop) : ℝ≥0∞) (1 : ℝ≥0∞)
have this : IsProbabilityMeasure μ
Tactic: have : IsProbabilityMeasure μ := hs.isProbabilityMeasure
-- Lean 4 proof step from Mathlib.Probability.BorelCantelli (goal)
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 : IsProbabilityMeasure μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (limsup s atTop) : ℝ≥0∞) (1 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞)
  ((μ : (a : Set Ω) → ℝ≥0∞)
      {ω : Ω |
        Tendsto (β := ℝ)
          (fun (n : ℕ) ↦
            ∑ k ∈ Finset.range n,
              μ[(s (k + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) k] ω)
          atTop atTop} :
    ℝ≥0∞)
  (1 : ℝ≥0∞)
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})]
-- Lean 4 proof step from Mathlib.Probability.BorelCantelli (goal)
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 :
  {ω : Ω |
      Tendsto (β := ℝ)
        (fun (n : ℕ) ↦
          ∑ k ∈ Finset.range n,
            μ[(s (k + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) k] ω)
        atTop atTop} =ᶠ[ae μ]
    Set.univ
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞)
        {ω : Ω |
          Tendsto (β := ℝ)
            (fun (n : ℕ) ↦
              ∑ k ∈ Finset.range n,
                μ[(s (k + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) k] ω)
            atTop atTop} :
      ℝ≥0∞)
    (1 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: rw [measure_congr this, measure_univ]
-- Lean 4 proof step from Mathlib.Probability.BorelCantelli (goal)
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 :
  {ω : Ω |
      Tendsto (β := ℝ)
        (fun (n : ℕ) ↦
          ∑ k ∈ Finset.range n,
            μ[(s (k + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) k] ω)
        atTop atTop} =ᶠ[ae μ]
    Set.univ
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞)
        {ω : Ω |
          Tendsto (β := ℝ)
            (fun (n : ℕ) ↦
              ∑ k ∈ Finset.range n,
                μ[(s (k + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) k] ω)
            atTop atTop} :
      ℝ≥0∞)
    (1 : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) 1 1
Tactic: rw [measure_congr this, measure_univ]
-- Lean 4 proof step from Mathlib.Probability.BorelCantelli (goal)
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 : IsProbabilityMeasure μ
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞)
        {ω : Ω |
          Tendsto (β := ℝ)
            (fun (n : ℕ) ↦
              ∑ k ∈ Finset.range n,
                μ[(s (k + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) k] ω)
            atTop atTop} :
      ℝ≥0∞)
    (1 : ℝ≥0∞)
have suffices : {ω : Ω |
    Tendsto (β := ℝ)
      (fun (n : ℕ) ↦
        ∑ k ∈ Finset.range n,
          μ[(s (k + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) k] ω)
      atTop atTop} =ᶠ[ae μ]
  Set.univ
Tactic: suffices {ω | Tendsto (fun n => ∑ k ∈ Finset.range n,
      (μ[(s (k + 1)).indicator (1 : Ω → ℝ)|filtrationOfSet hsm k]) ω) atTop atTop} =ᵐ[μ] Set.univ by
    rw [measure_congr this, measure_univ]
-- Lean 4 proof step from Mathlib.Probability.BorelCantelli (hypothesis)
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 : IsProbabilityMeasure μ
⊢ {ω : Ω |
      Tendsto (β := ℝ)
        (fun (n : ℕ) ↦
          ∑ k ∈ Finset.range n,
            μ[(s (k + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) k] ω)
        atTop atTop} =ᶠ[ae μ]
    Set.univ
have this₁ : ∀ᵐ (ω : Ω) ∂μ,
  ∀ (n : ℕ),
    Eq (α := ℝ) (μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω)
      ((fun (x : Ω) ↦ μ.real (s (n + 1))) ω)
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
-- Lean 4 proof step from Mathlib.Probability.BorelCantelli (goal)
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))) ω)
⊢ {ω : Ω |
      Tendsto (β := ℝ)
        (fun (n : ℕ) ↦
          ∑ k ∈ Finset.range n,
            μ[(s (k + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) k] ω)
        atTop atTop} =ᶠ[ae μ]
    Set.univ
have h : ∀ (ω : Ω)
  (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: filter_upwards [this] with ω hω
-- Lean 4 proof step from Mathlib.Probability.BorelCantelli (goal)
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 ω
have h : Tendsto (β := ℝ)
  (fun (n : ℕ) ↦
    ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) k] ω)
  atTop atTop
Tactic: refine eq_true (?_ : Tendsto _ _ _)
-- Lean 4 proof step from Mathlib.Probability.BorelCantelli (goal)
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
have h : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1))) atTop atTop
Tactic: simp_rw [hω]
-- Lean 4 proof step from Mathlib.Probability.BorelCantelli (goal)
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 (𝓝 ∞)
have rw : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))) atTop
  (𝓝 (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s (n + 1))))
Tactic: rw [← ENNReal.tsum_add_one_eq_top hs' (measure_ne_top _ _)]
-- Lean 4 proof step from Mathlib.Probability.BorelCantelli (hypothesis)
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 : ℕ) ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1))) atTop atTop
have htends : 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 _
-- Lean 4 proof step from Mathlib.Probability.BorelCantelli (hypothesis)
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 (𝓝 ∞)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1))) atTop atTop
have htends₁ : ∀ (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
Cleared hypotheses: htends
-- Lean 4 proof step from Mathlib.Probability.BorelCantelli (goal)
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
have h : Monotone (β := ℝ) fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1))
Tactic: refine tendsto_atTop_atTop_of_monotone' ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.BorelCantelli (goal)
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))
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1))) atTop atTop
have h₁ : ¬BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1)))
Tactic: refine tendsto_atTop_atTop_of_monotone' ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.BorelCantelli (goal)
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))
have h : ∀ (n : ℕ), LE.le (α := ℝ) (∑ x ∈ Finset.range n, μ.real (s (x + 1))) (∑ x ∈ Finset.range (n + 1), μ.real (s (x + 1)))
Tactic: refine monotone_nat_of_le_succ fun n => ?_
-- Lean 4 proof step from Mathlib.Probability.BorelCantelli (goal)
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 : ℕ
⊢ LE.le (α := ℝ) (∑ x ∈ Finset.range n, μ.real (s (x + 1))) (∑ x ∈ Finset.range (n + 1), μ.real (s (x + 1)))
have h : 0 ≤ μ.real (s (n + 1))
Tactic: rw [← sub_nonneg, Finset.sum_range_succ_sub_sum]