α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeInf α
inst✝¹ : NoMinOrder α
inst✝ : IsCountablyGenerated atBot
μ : Measure α
a : α
this : Nonempty α
⊢ Tendsto (fun x => ↑↑μ (Ioc x a)) atBot (𝓝 (↑↑μ (Iic a)))
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeInf α
inst✝¹ : NoMinOrder α
inst✝ : IsCountablyGenerated atBot
μ : Measure α
a : α
⊢ Tendsto (fun x => ↑↑μ (Ioc x a)) atBot (𝓝 (↑↑μ (Iic a)))
haveI : Nonempty α := ⟨a⟩
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeInf α
inst✝¹ : NoMinOrder α
inst✝ : IsCountablyGenerated atBot
μ : Measure α
a : α
this : Nonempty α
h_mono : Antitone fun x => ↑↑μ (Ioc x a)
⊢ Tendsto (fun x => ↑↑μ (Ioc x a)) atBot (𝓝 (↑↑μ (Iic a)))
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeInf α
inst✝¹ : NoMinOrder α
inst✝ : IsCountablyGenerated atBot
μ : Measure α
a : α
this : Nonempty α
⊢ Tendsto (fun x => ↑↑μ (Ioc x a)) atBot (𝓝 (↑↑μ (Iic a)))
have h_mono : Antitone fun x => μ (Ioc x a) := fun i j hij =>
  measure_mono (Ioc_subset_Ioc_left hij)
case h.e'_5.h.e'_3
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeInf α
inst✝¹ : NoMinOrder α
inst✝ : IsCountablyGenerated atBot
μ : Measure α
a : α
this : Nonempty α
h_mono : Antitone fun x => ↑↑μ (Ioc x a)
⊢ ↑↑μ (Iic a) = ⨆ (i : α), ↑↑μ (Ioc i a)
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeInf α
inst✝¹ : NoMinOrder α
inst✝ : IsCountablyGenerated atBot
μ : Measure α
a : α
this : Nonempty α
h_mono : Antitone fun x => ↑↑μ (Ioc x a)
⊢ Tendsto (fun x => ↑↑μ (Ioc x a)) atBot (𝓝 (↑↑μ (Iic a)))
convert tendsto_atBot_iSup h_mono
case h.e'_5.h.e'_3.intro.intro
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeInf α
inst✝¹ : NoMinOrder α
inst✝ : IsCountablyGenerated atBot
μ : Measure α
a : α
this : Nonempty α
h_mono : Antitone fun x => ↑↑μ (Ioc x a)
xs : ℕ → α
hxs_mono : Antitone xs
hxs_tendsto : Tendsto xs atTop atBot
⊢ ↑↑μ (Iic a) = ⨆ (i : α), ↑↑μ (Ioc i a)
case h.e'_5.h.e'_3
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeInf α
inst✝¹ : NoMinOrder α
inst✝ : IsCountablyGenerated atBot
μ : Measure α
a : α
this : Nonempty α
h_mono : Antitone fun x => ↑↑μ (Ioc x a)
⊢ ↑↑μ (Iic a) = ⨆ (i : α), ↑↑μ (Ioc i a)
obtain ⟨xs, hxs_mono, hxs_tendsto⟩ := exists_seq_antitone_tendsto_atTop_atBot α
case h.e'_5.h.e'_3.intro.intro
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeInf α
inst✝¹ : NoMinOrder α
inst✝ : IsCountablyGenerated atBot
μ : Measure α
a : α
this : Nonempty α
h_mono : Antitone fun x => ↑↑μ (Ioc x a)
xs : ℕ → α
hxs_mono : Antitone xs
hxs_tendsto : Tendsto xs atTop atBot
h_Iic : Iic a = ⋃ (n : ℕ), Ioc (xs n) a
⊢ ↑↑μ (Iic a) = ⨆ (i : α), ↑↑μ (Ioc i a)
case h.e'_5.h.e'_3.intro.intro
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeInf α
inst✝¹ : NoMinOrder α
inst✝ : IsCountablyGenerated atBot
μ : Measure α
a : α
this : Nonempty α
h_mono : Antitone fun x => ↑↑μ (Ioc x a)
xs : ℕ → α
hxs_mono : Antitone xs
hxs_tendsto : Tendsto xs atTop atBot
⊢ ↑↑μ (Iic a) = ⨆ (i : α), ↑↑μ (Ioc i a)
have h_Iic : Iic a = ⋃ n, Ioc (xs n) a := by
  ext1 x
  simp only [mem_Iic, mem_iUnion, mem_Ioc, exists_and_right, iff_and_self]
  intro
  obtain ⟨y, hxy⟩ := NoMinOrder.exists_lt x
  obtain ⟨n, hn⟩ := tendsto_atTop_atBot.mp hxs_tendsto y
  exact ⟨n, (hn n le_rfl).trans_lt hxy⟩
case h.e'_5.h.e'_3.intro.intro
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeInf α
inst✝¹ : NoMinOrder α
inst✝ : IsCountablyGenerated atBot
μ : Measure α
a : α
this : Nonempty α
h_mono : Antitone fun x => ↑↑μ (Ioc x a)
xs : ℕ → α
hxs_mono : Antitone xs
hxs_tendsto : Tendsto xs atTop atBot
h_Iic : Iic a = ⋃ (n : ℕ), Ioc (xs n) a
⊢ Directed (fun x x_1 => x ⊆ x_1) fun n => Ioc (xs n) a
case h.e'_5.h.e'_3.intro.intro
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeInf α
inst✝¹ : NoMinOrder α
inst✝ : IsCountablyGenerated atBot
μ : Measure α
a : α
this : Nonempty α
h_mono : Antitone fun x => ↑↑μ (Ioc x a)
xs : ℕ → α
hxs_mono : Antitone xs
hxs_tendsto : Tendsto xs atTop atBot
h_Iic : Iic a = ⋃ (n : ℕ), Ioc (xs n) a
⊢ ↑↑μ (Iic a) = ⨆ (i : α), ↑↑μ (Ioc i a)
rw [h_Iic, measure_iUnion_eq_iSup, iSup_eq_iSup_subseq_of_antitone h_mono hxs_tendsto]
no goals
case h.e'_5.h.e'_3.intro.intro
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeInf α
inst✝¹ : NoMinOrder α
inst✝ : IsCountablyGenerated atBot
μ : Measure α
a : α
this : Nonempty α
h_mono : Antitone fun x => ↑↑μ (Ioc x a)
xs : ℕ → α
hxs_mono : Antitone xs
hxs_tendsto : Tendsto xs atTop atBot
h_Iic : Iic a = ⋃ (n : ℕ), Ioc (xs n) a
⊢ Directed (fun x x_1 => x ⊆ x_1) fun n => Ioc (xs n) a
exact Monotone.directed_le fun i j hij => Ioc_subset_Ioc_left (hxs_mono hij)
case h
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeInf α
inst✝¹ : NoMinOrder α
inst✝ : IsCountablyGenerated atBot
μ : Measure α
a : α
this : Nonempty α
h_mono : Antitone fun x => ↑↑μ (Ioc x a)
xs : ℕ → α
hxs_mono : Antitone xs
hxs_tendsto : Tendsto xs atTop atBot
x : α
⊢ x ∈ Iic a ↔ x ∈ ⋃ (n : ℕ), Ioc (xs n) a
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeInf α
inst✝¹ : NoMinOrder α
inst✝ : IsCountablyGenerated atBot
μ : Measure α
a : α
this : Nonempty α
h_mono : Antitone fun x => ↑↑μ (Ioc x a)
xs : ℕ → α
hxs_mono : Antitone xs
hxs_tendsto : Tendsto xs atTop atBot
⊢ Iic a = ⋃ (n : ℕ), Ioc (xs n) a
ext1 x
case h
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeInf α
inst✝¹ : NoMinOrder α
inst✝ : IsCountablyGenerated atBot
μ : Measure α
a : α
this : Nonempty α
h_mono : Antitone fun x => ↑↑μ (Ioc x a)
xs : ℕ → α
hxs_mono : Antitone xs
hxs_tendsto : Tendsto xs atTop atBot
x : α
⊢ x ≤ a → ∃ x_1, xs x_1 < x
case h
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeInf α
inst✝¹ : NoMinOrder α
inst✝ : IsCountablyGenerated atBot
μ : Measure α
a : α
this : Nonempty α
h_mono : Antitone fun x => ↑↑μ (Ioc x a)
xs : ℕ → α
hxs_mono : Antitone xs
hxs_tendsto : Tendsto xs atTop atBot
x : α
⊢ x ∈ Iic a ↔ x ∈ ⋃ (n : ℕ), Ioc (xs n) a
simp only [mem_Iic, mem_iUnion, mem_Ioc, exists_and_right, iff_and_self]
case h
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeInf α
inst✝¹ : NoMinOrder α
inst✝ : IsCountablyGenerated atBot
μ : Measure α
a : α
this : Nonempty α
h_mono : Antitone fun x => ↑↑μ (Ioc x a)
xs : ℕ → α
hxs_mono : Antitone xs
hxs_tendsto : Tendsto xs atTop atBot
x : α
a✝ : x ≤ a
⊢ ∃ x_1, xs x_1 < x
case h
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeInf α
inst✝¹ : NoMinOrder α
inst✝ : IsCountablyGenerated atBot
μ : Measure α
a : α
this : Nonempty α
h_mono : Antitone fun x => ↑↑μ (Ioc x a)
xs : ℕ → α
hxs_mono : Antitone xs
hxs_tendsto : Tendsto xs atTop atBot
x : α
⊢ x ≤ a → ∃ x_1, xs x_1 < x
intro
case h.intro
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeInf α
inst✝¹ : NoMinOrder α
inst✝ : IsCountablyGenerated atBot
μ : Measure α
a : α
this : Nonempty α
h_mono : Antitone fun x => ↑↑μ (Ioc x a)
xs : ℕ → α
hxs_mono : Antitone xs
hxs_tendsto : Tendsto xs atTop atBot
x : α
a✝ : x ≤ a
y : α
hxy : y < x
⊢ ∃ x_1, xs x_1 < x
case h
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeInf α
inst✝¹ : NoMinOrder α
inst✝ : IsCountablyGenerated atBot
μ : Measure α
a : α
this : Nonempty α
h_mono : Antitone fun x => ↑↑μ (Ioc x a)
xs : ℕ → α
hxs_mono : Antitone xs
hxs_tendsto : Tendsto xs atTop atBot
x : α
a✝ : x ≤ a
⊢ ∃ x_1, xs x_1 < x
obtain ⟨y, hxy⟩ := NoMinOrder.exists_lt x
case h.intro.intro
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeInf α
inst✝¹ : NoMinOrder α
inst✝ : IsCountablyGenerated atBot
μ : Measure α
a : α
this : Nonempty α
h_mono : Antitone fun x => ↑↑μ (Ioc x a)
xs : ℕ → α
hxs_mono : Antitone xs
hxs_tendsto : Tendsto xs atTop atBot
x : α
a✝ : x ≤ a
y : α
hxy : y < x
n : ℕ
hn : ∀ (a : ℕ), n ≤ a → xs a ≤ y
⊢ ∃ x_1, xs x_1 < x
case h.intro
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeInf α
inst✝¹ : NoMinOrder α
inst✝ : IsCountablyGenerated atBot
μ : Measure α
a : α
this : Nonempty α
h_mono : Antitone fun x => ↑↑μ (Ioc x a)
xs : ℕ → α
hxs_mono : Antitone xs
hxs_tendsto : Tendsto xs atTop atBot
x : α
a✝ : x ≤ a
y : α
hxy : y < x
⊢ ∃ x_1, xs x_1 < x
obtain ⟨n, hn⟩ := tendsto_atTop_atBot.mp hxs_tendsto y
no goals
case h.intro.intro
α : Type u_1
mα : MeasurableSpace α
inst✝² : SemilatticeInf α
inst✝¹ : NoMinOrder α
inst✝ : IsCountablyGenerated atBot
μ : Measure α
a : α
this : Nonempty α
h_mono : Antitone fun x => ↑↑μ (Ioc x a)
xs : ℕ → α
hxs_mono : Antitone xs
hxs_tendsto : Tendsto xs atTop atBot
x : α
a✝ : x ≤ a
y : α
hxy : y < x
n : ℕ
hn : ∀ (a : ℕ), n ≤ a → xs a ≤ y
⊢ ∃ x_1, xs x_1 < x
exact ⟨n, (hn n le_rfl).trans_lt hxy⟩