α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeSup α
inst✝¹ : NoMaxOrder α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
a : α
this : Nonempty α
⊢ Tendsto (fun x => ↑↑μ (Ico a x)) atTop (𝓝 (↑↑μ (Ici a)))
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeSup α
inst✝¹ : NoMaxOrder α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
a : α
⊢ Tendsto (fun x => ↑↑μ (Ico a x)) atTop (𝓝 (↑↑μ (Ici a)))
haveI : Nonempty α := ⟨a⟩
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeSup α
inst✝¹ : NoMaxOrder α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
a : α
this : Nonempty α
h_mono : Monotone fun x => ↑↑μ (Ico a x)
⊢ Tendsto (fun x => ↑↑μ (Ico a x)) atTop (𝓝 (↑↑μ (Ici a)))
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeSup α
inst✝¹ : NoMaxOrder α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
a : α
this : Nonempty α
⊢ Tendsto (fun x => ↑↑μ (Ico a x)) atTop (𝓝 (↑↑μ (Ici a)))
have h_mono : Monotone fun x => μ (Ico a x) := fun i j hij =>
  measure_mono (Ico_subset_Ico_right hij)
case h.e'_5.h.e'_3
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeSup α
inst✝¹ : NoMaxOrder α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
a : α
this : Nonempty α
h_mono : Monotone fun x => ↑↑μ (Ico a x)
⊢ ↑↑μ (Ici a) = ⨆ (i : α), ↑↑μ (Ico a i)
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeSup α
inst✝¹ : NoMaxOrder α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
a : α
this : Nonempty α
h_mono : Monotone fun x => ↑↑μ (Ico a x)
⊢ Tendsto (fun x => ↑↑μ (Ico a x)) atTop (𝓝 (↑↑μ (Ici a)))
convert tendsto_atTop_iSup h_mono
case h.e'_5.h.e'_3.intro.intro
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeSup α
inst✝¹ : NoMaxOrder α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
a : α
this : Nonempty α
h_mono : Monotone fun x => ↑↑μ (Ico a x)
xs : ℕ → α
hxs_mono : Monotone xs
hxs_tendsto : Tendsto xs atTop atTop
⊢ ↑↑μ (Ici a) = ⨆ (i : α), ↑↑μ (Ico a i)
case h.e'_5.h.e'_3
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeSup α
inst✝¹ : NoMaxOrder α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
a : α
this : Nonempty α
h_mono : Monotone fun x => ↑↑μ (Ico a x)
⊢ ↑↑μ (Ici a) = ⨆ (i : α), ↑↑μ (Ico a 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✝¹ : NoMaxOrder α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
a : α
this : Nonempty α
h_mono : Monotone fun x => ↑↑μ (Ico a x)
xs : ℕ → α
hxs_mono : Monotone xs
hxs_tendsto : Tendsto xs atTop atTop
h_Ici : Ici a = ⋃ (n : ℕ), Ico a (xs n)
⊢ ↑↑μ (Ici a) = ⨆ (i : α), ↑↑μ (Ico a i)
case h.e'_5.h.e'_3.intro.intro
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeSup α
inst✝¹ : NoMaxOrder α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
a : α
this : Nonempty α
h_mono : Monotone fun x => ↑↑μ (Ico a x)
xs : ℕ → α
hxs_mono : Monotone xs
hxs_tendsto : Tendsto xs atTop atTop
⊢ ↑↑μ (Ici a) = ⨆ (i : α), ↑↑μ (Ico a i)
have h_Ici : Ici a = ⋃ n, Ico a (xs n) := by
  ext1 x
  simp only [mem_Ici, mem_iUnion, mem_Ico, exists_and_left, iff_self_and]
  intro
  obtain ⟨y, hxy⟩ := NoMaxOrder.exists_gt x
  obtain ⟨n, hn⟩ := tendsto_atTop_atTop.mp hxs_tendsto y
  exact ⟨n, hxy.trans_le (hn n le_rfl)⟩
case h.e'_5.h.e'_3.intro.intro
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeSup α
inst✝¹ : NoMaxOrder α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
a : α
this : Nonempty α
h_mono : Monotone fun x => ↑↑μ (Ico a x)
xs : ℕ → α
hxs_mono : Monotone xs
hxs_tendsto : Tendsto xs atTop atTop
h_Ici : Ici a = ⋃ (n : ℕ), Ico a (xs n)
⊢ Directed (fun x x_1 => x ⊆ x_1) fun n => Ico a (xs n)
case h.e'_5.h.e'_3.intro.intro
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeSup α
inst✝¹ : NoMaxOrder α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
a : α
this : Nonempty α
h_mono : Monotone fun x => ↑↑μ (Ico a x)
xs : ℕ → α
hxs_mono : Monotone xs
hxs_tendsto : Tendsto xs atTop atTop
h_Ici : Ici a = ⋃ (n : ℕ), Ico a (xs n)
⊢ ↑↑μ (Ici a) = ⨆ (i : α), ↑↑μ (Ico a i)
rw [h_Ici, 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✝¹ : NoMaxOrder α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
a : α
this : Nonempty α
h_mono : Monotone fun x => ↑↑μ (Ico a x)
xs : ℕ → α
hxs_mono : Monotone xs
hxs_tendsto : Tendsto xs atTop atTop
h_Ici : Ici a = ⋃ (n : ℕ), Ico a (xs n)
⊢ Directed (fun x x_1 => x ⊆ x_1) fun n => Ico a (xs n)
exact Monotone.directed_le fun i j hij => Ico_subset_Ico_right (hxs_mono hij)
case h
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeSup α
inst✝¹ : NoMaxOrder α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
a : α
this : Nonempty α
h_mono : Monotone fun x => ↑↑μ (Ico a x)
xs : ℕ → α
hxs_mono : Monotone xs
hxs_tendsto : Tendsto xs atTop atTop
x : α
⊢ x ∈ Ici a ↔ x ∈ ⋃ (n : ℕ), Ico a (xs n)
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeSup α
inst✝¹ : NoMaxOrder α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
a : α
this : Nonempty α
h_mono : Monotone fun x => ↑↑μ (Ico a x)
xs : ℕ → α
hxs_mono : Monotone xs
hxs_tendsto : Tendsto xs atTop atTop
⊢ Ici a = ⋃ (n : ℕ), Ico a (xs n)
ext1 x
case h
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeSup α
inst✝¹ : NoMaxOrder α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
a : α
this : Nonempty α
h_mono : Monotone fun x => ↑↑μ (Ico a x)
xs : ℕ → α
hxs_mono : Monotone xs
hxs_tendsto : Tendsto xs atTop atTop
x : α
⊢ a ≤ x → ∃ x_1, x < xs x_1
case h
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeSup α
inst✝¹ : NoMaxOrder α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
a : α
this : Nonempty α
h_mono : Monotone fun x => ↑↑μ (Ico a x)
xs : ℕ → α
hxs_mono : Monotone xs
hxs_tendsto : Tendsto xs atTop atTop
x : α
⊢ x ∈ Ici a ↔ x ∈ ⋃ (n : ℕ), Ico a (xs n)
simp only [mem_Ici, mem_iUnion, mem_Ico, exists_and_left, iff_self_and]
case h
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeSup α
inst✝¹ : NoMaxOrder α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
a : α
this : Nonempty α
h_mono : Monotone fun x => ↑↑μ (Ico a x)
xs : ℕ → α
hxs_mono : Monotone xs
hxs_tendsto : Tendsto xs atTop atTop
x : α
a✝ : a ≤ x
⊢ ∃ x_1, x < xs x_1
case h
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeSup α
inst✝¹ : NoMaxOrder α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
a : α
this : Nonempty α
h_mono : Monotone fun x => ↑↑μ (Ico a x)
xs : ℕ → α
hxs_mono : Monotone xs
hxs_tendsto : Tendsto xs atTop atTop
x : α
⊢ a ≤ x → ∃ x_1, x < xs x_1
intro
case h.intro
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeSup α
inst✝¹ : NoMaxOrder α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
a : α
this : Nonempty α
h_mono : Monotone fun x => ↑↑μ (Ico a x)
xs : ℕ → α
hxs_mono : Monotone xs
hxs_tendsto : Tendsto xs atTop atTop
x : α
a✝ : a ≤ x
y : α
hxy : x < y
⊢ ∃ x_1, x < xs x_1
case h
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeSup α
inst✝¹ : NoMaxOrder α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
a : α
this : Nonempty α
h_mono : Monotone fun x => ↑↑μ (Ico a x)
xs : ℕ → α
hxs_mono : Monotone xs
hxs_tendsto : Tendsto xs atTop atTop
x : α
a✝ : a ≤ x
⊢ ∃ x_1, x < xs x_1
obtain ⟨y, hxy⟩ := NoMaxOrder.exists_gt x
case h.intro.intro
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeSup α
inst✝¹ : NoMaxOrder α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
a : α
this : Nonempty α
h_mono : Monotone fun x => ↑↑μ (Ico a x)
xs : ℕ → α
hxs_mono : Monotone xs
hxs_tendsto : Tendsto xs atTop atTop
x : α
a✝ : a ≤ x
y : α
hxy : x < y
n : ℕ
hn : ∀ (a : ℕ), n ≤ a → y ≤ xs a
⊢ ∃ x_1, x < xs x_1
case h.intro
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeSup α
inst✝¹ : NoMaxOrder α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
a : α
this : Nonempty α
h_mono : Monotone fun x => ↑↑μ (Ico a x)
xs : ℕ → α
hxs_mono : Monotone xs
hxs_tendsto : Tendsto xs atTop atTop
x : α
a✝ : a ≤ x
y : α
hxy : x < y
⊢ ∃ x_1, x < xs x_1
obtain ⟨n, hn⟩ := tendsto_atTop_atTop.mp hxs_tendsto y
no goals
case h.intro.intro
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeSup α
inst✝¹ : NoMaxOrder α
inst✝ : IsCountablyGenerated atTop
μ : Measure α
a : α
this : Nonempty α
h_mono : Monotone fun x => ↑↑μ (Ico a x)
xs : ℕ → α
hxs_mono : Monotone xs
hxs_tendsto : Tendsto xs atTop atTop
x : α
a✝ : a ≤ x
y : α
hxy : x < y
n : ℕ
hn : ∀ (a : ℕ), n ≤ a → y ≤ xs a
⊢ ∃ x_1, x < xs x_1
exact ⟨n, hxy.trans_le (hn n le_rfl)⟩