Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
⊢ Indep (limsup s atTop) (limsup s atTop)
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
⊢ Indep (limsup s atTop) (limsup s atTop)
let ns : ι → Set ι := Set.Iic
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
⊢ Indep (limsup s atTop) (limsup s atTop)
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
⊢ Indep (limsup s atTop) (limsup s atTop)
have hnsp : ∀ i, BddAbove (ns i) := fun i => bddAbove_Iic
case refine'_1
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
⊢ ∀ (t : Set ι), BddAbove t → tᶜ ∈ atTop

case refine'_2
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
⊢ Directed (fun x x_1 => x ≤ x_1) fun a => ns a

case refine'_3
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
⊢ ∀ (n : ι), ∃ a, n ∈ ns a
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
⊢ Indep (limsup s atTop) (limsup s atTop)
refine' indep_limsup_self h_le h_indep _ _ hnsp _
case refine'_1
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
⊢ ∀ (t : Set ι), (∃ x, x ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → a ≤ x}) → ∃ a, ∀ (b : ι), a ≤ b → ¬b ∈ t
case refine'_1
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
⊢ ∀ (t : Set ι), BddAbove t → tᶜ ∈ atTop
simp only [mem_atTop_sets, ge_iff_le, Set.mem_compl_iff, BddAbove, upperBounds, Set.Nonempty]
case refine'_1.intro
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → a ≤ x}
⊢ ∃ a, ∀ (b : ι), a ≤ b → ¬b ∈ t
case refine'_1
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
⊢ ∀ (t : Set ι), (∃ x, x ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → a ≤ x}) → ∃ a, ∀ (b : ι), a ≤ b → ¬b ∈ t
rintro t ⟨a, ha⟩
case refine'_1.intro.intro
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → a ≤ x}
b : ι
hb : a < b
⊢ ∃ a, ∀ (b : ι), a ≤ b → ¬b ∈ t
case refine'_1.intro
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → a ≤ x}
⊢ ∃ a, ∀ (b : ι), a ≤ b → ¬b ∈ t
obtain ⟨b, hb⟩ : ∃ b, a < b := exists_gt a
case refine'_1.intro.intro
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → a ≤ x}
b : ι
hb : a < b
c : ι
hc : b ≤ c
hct : c ∈ t
⊢ False
case refine'_1.intro.intro
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → a ≤ x}
b : ι
hb : a < b
⊢ ∃ a, ∀ (b : ι), a ≤ b → ¬b ∈ t
refine' ⟨b, fun c hc hct => _⟩
case refine'_1.intro.intro
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → a ≤ x}
b : ι
hb : a < b
c : ι
hc : b ≤ c
hct : c ∈ t
this : ∀ (i : ι), i ∈ t → i < c
⊢ False

case this
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → a ≤ x}
b : ι
hb : a < b
c : ι
hc : b ≤ c
hct : c ∈ t
⊢ ∀ (i : ι), i ∈ t → i < c
case refine'_1.intro.intro
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → a ≤ x}
b : ι
hb : a < b
c : ι
hc : b ≤ c
hct : c ∈ t
⊢ False
suffices : ∀ i ∈ t, i < c
case this
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → a ≤ x}
b : ι
hb : a < b
c : ι
hc : b ≤ c
hct : c ∈ t
⊢ ∀ (i : ι), i ∈ t → i < c
case refine'_1.intro.intro
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → a ≤ x}
b : ι
hb : a < b
c : ι
hc : b ≤ c
hct : c ∈ t
this : ∀ (i : ι), i ∈ t → i < c
⊢ False

case this
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → a ≤ x}
b : ι
hb : a < b
c : ι
hc : b ≤ c
hct : c ∈ t
⊢ ∀ (i : ι), i ∈ t → i < c
exact lt_irrefl c (this c hct)
no goals
case this
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → a ≤ x}
b : ι
hb : a < b
c : ι
hc : b ≤ c
hct : c ∈ t
⊢ ∀ (i : ι), i ∈ t → i < c
exact fun i hi => (ha hi).trans_lt (hb.trans_le hc)
no goals
case refine'_2
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
⊢ Directed (fun x x_1 => x ≤ x_1) fun a => ns a
exact Monotone.directed_le fun i j hij k hki => le_trans hki hij
no goals
case refine'_3
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
⊢ ∀ (n : ι), ∃ a, n ∈ ns a
exact fun n => ⟨n, le_rfl⟩