case inl
α : Type u_1
mα : MeasurableSpace α
inst✝¹ : SemilatticeSup α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
h✝ : IsEmpty α
⊢ Tendsto (fun x => ↑↑μ (Iic x)) atTop (𝓝 (↑↑μ univ))

case inr
α : Type u_1
mα : MeasurableSpace α
inst✝¹ : SemilatticeSup α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
h✝ : Nonempty α
⊢ Tendsto (fun x => ↑↑μ (Iic x)) atTop (𝓝 (↑↑μ univ))
α : Type u_1
mα : MeasurableSpace α
inst✝¹ : SemilatticeSup α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
⊢ Tendsto (fun x => ↑↑μ (Iic x)) atTop (𝓝 (↑↑μ univ))
cases isEmpty_or_nonempty α
case inr
α : Type u_1
mα : MeasurableSpace α
inst✝¹ : SemilatticeSup α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
h✝ : Nonempty α
h_mono : Monotone fun x => ↑↑μ (Iic x)
⊢ Tendsto (fun x => ↑↑μ (Iic x)) atTop (𝓝 (↑↑μ univ))
case inr
α : Type u_1
mα : MeasurableSpace α
inst✝¹ : SemilatticeSup α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
h✝ : Nonempty α
⊢ Tendsto (fun x => ↑↑μ (Iic x)) atTop (𝓝 (↑↑μ univ))
have h_mono : Monotone fun x => μ (Iic x) := fun i j hij => measure_mono (Iic_subset_Iic.mpr hij)
case h.e'_5.h.e'_3
α : Type u_1
mα : MeasurableSpace α
inst✝¹ : SemilatticeSup α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
h✝ : Nonempty α
h_mono : Monotone fun x => ↑↑μ (Iic x)
⊢ ↑↑μ univ = ⨆ (i : α), ↑↑μ (Iic i)
case inr
α : Type u_1
mα : MeasurableSpace α
inst✝¹ : SemilatticeSup α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
h✝ : Nonempty α
h_mono : Monotone fun x => ↑↑μ (Iic x)
⊢ Tendsto (fun x => ↑↑μ (Iic x)) atTop (𝓝 (↑↑μ univ))
convert tendsto_atTop_iSup h_mono
case h.e'_5.h.e'_3.intro.intro
α : Type u_1
mα : MeasurableSpace α
inst✝¹ : SemilatticeSup α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
h✝ : Nonempty α
h_mono : Monotone fun x => ↑↑μ (Iic x)
xs : ℕ → α
hxs_mono : Monotone xs
hxs_tendsto : Tendsto xs atTop atTop
⊢ ↑↑μ univ = ⨆ (i : α), ↑↑μ (Iic i)
case h.e'_5.h.e'_3
α : Type u_1
mα : MeasurableSpace α
inst✝¹ : SemilatticeSup α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
h✝ : Nonempty α
h_mono : Monotone fun x => ↑↑μ (Iic x)
⊢ ↑↑μ univ = ⨆ (i : α), ↑↑μ (Iic i)
obtain ⟨xs, hxs_mono, hxs_tendsto⟩ := exists_seq_monotone_tendsto_atTop_atTop α
case h.e'_5.h.e'_3.intro.intro
α : Type u_1
mα : MeasurableSpace α
inst✝¹ : SemilatticeSup α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
h✝ : Nonempty α
h_mono : Monotone fun x => ↑↑μ (Iic x)
xs : ℕ → α
hxs_mono : Monotone xs
hxs_tendsto : Tendsto xs atTop atTop
h_univ : univ = ⋃ (n : ℕ), Iic (xs n)
⊢ ↑↑μ univ = ⨆ (i : α), ↑↑μ (Iic i)
case h.e'_5.h.e'_3.intro.intro
α : Type u_1
mα : MeasurableSpace α
inst✝¹ : SemilatticeSup α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
h✝ : Nonempty α
h_mono : Monotone fun x => ↑↑μ (Iic x)
xs : ℕ → α
hxs_mono : Monotone xs
hxs_tendsto : Tendsto xs atTop atTop
⊢ ↑↑μ univ = ⨆ (i : α), ↑↑μ (Iic i)
have h_univ : (univ : Set α) = ⋃ n, Iic (xs n) := by
  ext1 x
  simp only [mem_univ, mem_iUnion, mem_Iic, true_iff_iff]
  obtain ⟨n, hn⟩ := tendsto_atTop_atTop.mp hxs_tendsto x
  exact ⟨n, hn n le_rfl⟩
case h.e'_5.h.e'_3.intro.intro
α : Type u_1
mα : MeasurableSpace α
inst✝¹ : SemilatticeSup α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
h✝ : Nonempty α
h_mono : Monotone fun x => ↑↑μ (Iic x)
xs : ℕ → α
hxs_mono : Monotone xs
hxs_tendsto : Tendsto xs atTop atTop
h_univ : univ = ⋃ (n : ℕ), Iic (xs n)
⊢ Directed (fun x x_1 => x ⊆ x_1) fun n => Iic (xs n)
case h.e'_5.h.e'_3.intro.intro
α : Type u_1
mα : MeasurableSpace α
inst✝¹ : SemilatticeSup α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
h✝ : Nonempty α
h_mono : Monotone fun x => ↑↑μ (Iic x)
xs : ℕ → α
hxs_mono : Monotone xs
hxs_tendsto : Tendsto xs atTop atTop
h_univ : univ = ⋃ (n : ℕ), Iic (xs n)
⊢ ↑↑μ univ = ⨆ (i : α), ↑↑μ (Iic i)
rw [h_univ, measure_iUnion_eq_iSup, iSup_eq_iSup_subseq_of_monotone h_mono hxs_tendsto]
no goals
case h.e'_5.h.e'_3.intro.intro
α : Type u_1
mα : MeasurableSpace α
inst✝¹ : SemilatticeSup α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
h✝ : Nonempty α
h_mono : Monotone fun x => ↑↑μ (Iic x)
xs : ℕ → α
hxs_mono : Monotone xs
hxs_tendsto : Tendsto xs atTop atTop
h_univ : univ = ⋃ (n : ℕ), Iic (xs n)
⊢ Directed (fun x x_1 => x ⊆ x_1) fun n => Iic (xs n)
exact Monotone.directed_le fun i j hij => Iic_subset_Iic.mpr (hxs_mono hij)
case inl
α : Type u_1
mα : MeasurableSpace α
inst✝¹ : SemilatticeSup α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
h✝ : IsEmpty α
h1 : ∀ (x : α), Iic x = ∅
⊢ Tendsto (fun x => ↑↑μ (Iic x)) atTop (𝓝 (↑↑μ univ))
case inl
α : Type u_1
mα : MeasurableSpace α
inst✝¹ : SemilatticeSup α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
h✝ : IsEmpty α
⊢ Tendsto (fun x => ↑↑μ (Iic x)) atTop (𝓝 (↑↑μ univ))
have h1 : ∀ x : α, Iic x = ∅ := fun x => Subsingleton.elim _ _
case inl
α : Type u_1
mα : MeasurableSpace α
inst✝¹ : SemilatticeSup α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
h✝ : IsEmpty α
h1 : ∀ (x : α), Iic x = ∅
h2 : univ = ∅
⊢ Tendsto (fun x => ↑↑μ (Iic x)) atTop (𝓝 (↑↑μ univ))
case inl
α : Type u_1
mα : MeasurableSpace α
inst✝¹ : SemilatticeSup α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
h✝ : IsEmpty α
h1 : ∀ (x : α), Iic x = ∅
⊢ Tendsto (fun x => ↑↑μ (Iic x)) atTop (𝓝 (↑↑μ univ))
have h2 : (univ : Set α) = ∅ := Subsingleton.elim _ _
case inl
α : Type u_1
mα : MeasurableSpace α
inst✝¹ : SemilatticeSup α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
h✝ : IsEmpty α
h1 : ∀ (x : α), Iic x = ∅
h2 : univ = ∅
⊢ Tendsto (fun x => ↑↑μ ∅) atTop (𝓝 (↑↑μ ∅))
case inl
α : Type u_1
mα : MeasurableSpace α
inst✝¹ : SemilatticeSup α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
h✝ : IsEmpty α
h1 : ∀ (x : α), Iic x = ∅
h2 : univ = ∅
⊢ Tendsto (fun x => ↑↑μ (Iic x)) atTop (𝓝 (↑↑μ univ))
simp_rw [h1, h2]
no goals
case inl
α : Type u_1
mα : MeasurableSpace α
inst✝¹ : SemilatticeSup α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
h✝ : IsEmpty α
h1 : ∀ (x : α), Iic x = ∅
h2 : univ = ∅
⊢ Tendsto (fun x => ↑↑μ ∅) atTop (𝓝 (↑↑μ ∅))
exact tendsto_const_nhds
case h
α : Type u_1
mα : MeasurableSpace α
inst✝¹ : SemilatticeSup α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
h✝ : Nonempty α
h_mono : Monotone fun x => ↑↑μ (Iic x)
xs : ℕ → α
hxs_mono : Monotone xs
hxs_tendsto : Tendsto xs atTop atTop
x : α
⊢ x ∈ univ ↔ x ∈ ⋃ (n : ℕ), Iic (xs n)
α : Type u_1
mα : MeasurableSpace α
inst✝¹ : SemilatticeSup α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
h✝ : Nonempty α
h_mono : Monotone fun x => ↑↑μ (Iic x)
xs : ℕ → α
hxs_mono : Monotone xs
hxs_tendsto : Tendsto xs atTop atTop
⊢ univ = ⋃ (n : ℕ), Iic (xs n)
ext1 x
case h
α : Type u_1
mα : MeasurableSpace α
inst✝¹ : SemilatticeSup α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
h✝ : Nonempty α
h_mono : Monotone fun x => ↑↑μ (Iic x)
xs : ℕ → α
hxs_mono : Monotone xs
hxs_tendsto : Tendsto xs atTop atTop
x : α
⊢ ∃ i, x ≤ xs i
case h
α : Type u_1
mα : MeasurableSpace α
inst✝¹ : SemilatticeSup α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
h✝ : Nonempty α
h_mono : Monotone fun x => ↑↑μ (Iic x)
xs : ℕ → α
hxs_mono : Monotone xs
hxs_tendsto : Tendsto xs atTop atTop
x : α
⊢ x ∈ univ ↔ x ∈ ⋃ (n : ℕ), Iic (xs n)
simp only [mem_univ, mem_iUnion, mem_Iic, true_iff_iff]
case h.intro
α : Type u_1
mα : MeasurableSpace α
inst✝¹ : SemilatticeSup α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
h✝ : Nonempty α
h_mono : Monotone fun x => ↑↑μ (Iic x)
xs : ℕ → α
hxs_mono : Monotone xs
hxs_tendsto : Tendsto xs atTop atTop
x : α
n : ℕ
hn : ∀ (a : ℕ), n ≤ a → x ≤ xs a
⊢ ∃ i, x ≤ xs i
case h
α : Type u_1
mα : MeasurableSpace α
inst✝¹ : SemilatticeSup α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
h✝ : Nonempty α
h_mono : Monotone fun x => ↑↑μ (Iic x)
xs : ℕ → α
hxs_mono : Monotone xs
hxs_tendsto : Tendsto xs atTop atTop
x : α
⊢ ∃ i, x ≤ xs i
obtain ⟨n, hn⟩ := tendsto_atTop_atTop.mp hxs_tendsto x
no goals
case h.intro
α : Type u_1
mα : MeasurableSpace α
inst✝¹ : SemilatticeSup α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
h✝ : Nonempty α
h_mono : Monotone fun x => ↑↑μ (Iic x)
xs : ℕ → α
hxs_mono : Monotone xs
hxs_tendsto : Tendsto xs atTop atTop
x : α
n : ℕ
hn : ∀ (a : ℕ), n ≤ a → x ≤ xs a
⊢ ∃ i, x ≤ xs i
exact ⟨n, hn n le_rfl⟩