case intro.intro.intro
Ω : Type u_1
inst✝³ : PseudoEMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : SigmaFinite μ
s : Set Ω
Rs : ℕ → ℝ
left✝ : StrictAnti Rs
Rs_pos : ∀ (n : ℕ), 0 < Rs n
Rs_lim : Tendsto Rs atTop (𝓝 0)
⊢ ∃ rs, Tendsto rs atTop (𝓝 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ ↑↑μ (frontier (Metric.thickening (rs n) s)) = 0
Ω : Type u_1
inst✝³ : PseudoEMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : SigmaFinite μ
s : Set Ω
⊢ ∃ rs, Tendsto rs atTop (𝓝 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ ↑↑μ (frontier (Metric.thickening (rs n) s)) = 0
rcases exists_seq_strictAnti_tendsto (0 : ℝ) with ⟨Rs, ⟨_, ⟨Rs_pos, Rs_lim⟩⟩⟩
case intro.intro.intro
Ω : Type u_1
inst✝³ : PseudoEMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : SigmaFinite μ
s : Set Ω
Rs : ℕ → ℝ
left✝ : StrictAnti Rs
Rs_pos : ∀ (n : ℕ), 0 < Rs n
Rs_lim : Tendsto Rs atTop (𝓝 0)
obs : ∀ (n : ℕ), ∃ r, r ∈ Ioo 0 (Rs n) ∧ ↑↑μ (frontier (Metric.thickening r s)) = 0
⊢ ∃ rs, Tendsto rs atTop (𝓝 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ ↑↑μ (frontier (Metric.thickening (rs n) s)) = 0
case intro.intro.intro
Ω : Type u_1
inst✝³ : PseudoEMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : SigmaFinite μ
s : Set Ω
Rs : ℕ → ℝ
left✝ : StrictAnti Rs
Rs_pos : ∀ (n : ℕ), 0 < Rs n
Rs_lim : Tendsto Rs atTop (𝓝 0)
⊢ ∃ rs, Tendsto rs atTop (𝓝 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ ↑↑μ (frontier (Metric.thickening (rs n) s)) = 0
have obs := fun n : ℕ => exists_null_frontier_thickening μ s (Rs_pos n)
case intro.intro.intro.refine'_1
Ω : Type u_1
inst✝³ : PseudoEMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : SigmaFinite μ
s : Set Ω
Rs : ℕ → ℝ
left✝ : StrictAnti Rs
Rs_pos : ∀ (n : ℕ), 0 < Rs n
Rs_lim : Tendsto Rs atTop (𝓝 0)
obs : ∀ (n : ℕ), ∃ r, r ∈ Ioo 0 (Rs n) ∧ ↑↑μ (frontier (Metric.thickening r s)) = 0
⊢ Tendsto (fun n => Exists.choose (_ : ∃ r, r ∈ Ioo 0 (Rs n) ∧ ↑↑μ (frontier (Metric.thickening r s)) = 0)) atTop (𝓝 0)

case intro.intro.intro.refine'_2
Ω : Type u_1
inst✝³ : PseudoEMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : SigmaFinite μ
s : Set Ω
Rs : ℕ → ℝ
left✝ : StrictAnti Rs
Rs_pos : ∀ (n : ℕ), 0 < Rs n
Rs_lim : Tendsto Rs atTop (𝓝 0)
obs : ∀ (n : ℕ), ∃ r, r ∈ Ioo 0 (Rs n) ∧ ↑↑μ (frontier (Metric.thickening r s)) = 0
⊢ ∀ (n : ℕ),
    0 < (fun n => Exists.choose (_ : ∃ r, r ∈ Ioo 0 (Rs n) ∧ ↑↑μ (frontier (Metric.thickening r s)) = 0)) n ∧
      ↑↑μ
          (frontier
            (Metric.thickening
              ((fun n => Exists.choose (_ : ∃ r, r ∈ Ioo 0 (Rs n) ∧ ↑↑μ (frontier (Metric.thickening r s)) = 0)) n)
              s)) =
        0
case intro.intro.intro
Ω : Type u_1
inst✝³ : PseudoEMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : SigmaFinite μ
s : Set Ω
Rs : ℕ → ℝ
left✝ : StrictAnti Rs
Rs_pos : ∀ (n : ℕ), 0 < Rs n
Rs_lim : Tendsto Rs atTop (𝓝 0)
obs : ∀ (n : ℕ), ∃ r, r ∈ Ioo 0 (Rs n) ∧ ↑↑μ (frontier (Metric.thickening r s)) = 0
⊢ ∃ rs, Tendsto rs atTop (𝓝 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ ↑↑μ (frontier (Metric.thickening (rs n) s)) = 0
refine' ⟨fun n : ℕ => (obs n).choose, ⟨_, _⟩⟩
no goals
case intro.intro.intro.refine'_1
Ω : Type u_1
inst✝³ : PseudoEMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : SigmaFinite μ
s : Set Ω
Rs : ℕ → ℝ
left✝ : StrictAnti Rs
Rs_pos : ∀ (n : ℕ), 0 < Rs n
Rs_lim : Tendsto Rs atTop (𝓝 0)
obs : ∀ (n : ℕ), ∃ r, r ∈ Ioo 0 (Rs n) ∧ ↑↑μ (frontier (Metric.thickening r s)) = 0
⊢ Tendsto (fun n => Exists.choose (_ : ∃ r, r ∈ Ioo 0 (Rs n) ∧ ↑↑μ (frontier (Metric.thickening r s)) = 0)) atTop (𝓝 0)
exact tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds Rs_lim
  (fun n => (obs n).choose_spec.1.1.le) fun n => (obs n).choose_spec.1.2.le
no goals
case intro.intro.intro.refine'_2
Ω : Type u_1
inst✝³ : PseudoEMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : SigmaFinite μ
s : Set Ω
Rs : ℕ → ℝ
left✝ : StrictAnti Rs
Rs_pos : ∀ (n : ℕ), 0 < Rs n
Rs_lim : Tendsto Rs atTop (𝓝 0)
obs : ∀ (n : ℕ), ∃ r, r ∈ Ioo 0 (Rs n) ∧ ↑↑μ (frontier (Metric.thickening r s)) = 0
⊢ ∀ (n : ℕ),
    0 < (fun n => Exists.choose (_ : ∃ r, r ∈ Ioo 0 (Rs n) ∧ ↑↑μ (frontier (Metric.thickening r s)) = 0)) n ∧
      ↑↑μ
          (frontier
            (Metric.thickening
              ((fun n => Exists.choose (_ : ∃ r, r ∈ Ioo 0 (Rs n) ∧ ↑↑μ (frontier (Metric.thickening r s)) = 0)) n)
              s)) =
        0
exact fun n => ⟨(obs n).choose_spec.1.1, (obs n).choose_spec.2⟩