-- Mathlib/MeasureTheory/Constructions/BorelSpace/Metric.lean
theorem tendsto_measure_cthickening {μ : Measure α} {s : Set α}
    (hs : ∃ R > 0, μ (cthickening R s) ≠ ∞) :
    Tendsto (fun r => μ (cthickening r s)) (𝓝 0) (𝓝 (μ (closure s)))

Proof state:
α : Type u_1
inst✝² : PseudoEMetricSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, μ (cthickening R s) ≠ ⊤
A : Tendsto (fun r => μ (cthickening r s)) (𝓝[>] 0) (𝓝 (μ (closure s)))
B : Tendsto (fun r => μ (cthickening r s)) (𝓝[≤] 0) (𝓝 (μ (closure s)))
⊢ Tendsto (fun r => μ (cthickening r s)) (𝓝 0) (𝓝 (μ (closure s)))

Tactic:
convert B.sup A

Result:
case h.e'_4
α : Type u_1
inst✝² : PseudoEMetricSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, μ (cthickening R s) ≠ ⊤
A : Tendsto (fun r => μ (cthickening r s)) (𝓝[>] 0) (𝓝 (μ (closure s)))
B : Tendsto (fun r => μ (cthickening r s)) (𝓝[≤] 0) (𝓝 (μ (closure s)))
⊢ 𝓝 0 = 𝓝[≤] 0 ⊔ 𝓝[>] 0

Proof state:
α : Type u_1
inst✝² : PseudoEMetricSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, μ (cthickening R s) ≠ ⊤
A : Tendsto (fun r => μ (cthickening r s)) (𝓝[>] 0) (𝓝 (μ (closure s)))
⊢ Tendsto (fun r => μ (cthickening r s)) (𝓝 0) (𝓝 (μ (closure s)))

Tactic:
have B : Tendsto (fun r => μ (cthickening r s)) (𝓝[Iic 0] 0) (𝓝 (μ (closure s))) := by
  apply Tendsto.congr' _ tendsto_const_nhds
  filter_upwards [self_mem_nhdsWithin (α := ℝ)] with _ hr
  rw [cthickening_of_nonpos hr]

Result:
α : Type u_1
inst✝² : PseudoEMetricSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, μ (cthickening R s) ≠ ⊤
A : Tendsto (fun r => μ (cthickening r s)) (𝓝[>] 0) (𝓝 (μ (closure s)))
B : Tendsto (fun r => μ (cthickening r s)) (𝓝[≤] 0) (𝓝 (μ (closure s)))
⊢ Tendsto (fun r => μ (cthickening r s)) (𝓝 0) (𝓝 (μ (closure s)))

Proof state:
α : Type u_1
inst✝² : PseudoEMetricSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, μ (cthickening R s) ≠ ⊤
⊢ Tendsto (fun r => μ (cthickening r s)) (𝓝 0) (𝓝 (μ (closure s)))

Tactic:
have A : Tendsto (fun r => μ (cthickening r s)) (𝓝[Ioi 0] 0) (𝓝 (μ (closure s))) := by
  rw [closure_eq_iInter_cthickening]
  exact
    tendsto_measure_biInter_gt (fun r _ => isClosed_cthickening.nullMeasurableSet)
      (fun i j _ ij => cthickening_mono ij _) hs

Result:
α : Type u_1
inst✝² : PseudoEMetricSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, μ (cthickening R s) ≠ ⊤
A : Tendsto (fun r => μ (cthickening r s)) (𝓝[>] 0) (𝓝 (μ (closure s)))
⊢ Tendsto (fun r => μ (cthickening r s)) (𝓝 0) (𝓝 (μ (closure s)))

Proof state:
α : Type u_1
inst✝² : PseudoEMetricSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, μ (cthickening R s) ≠ ⊤
⊢ Tendsto (fun r => μ (cthickening r s)) (𝓝[>] 0) (𝓝 (μ (closure s)))

Tactic:
rw [closure_eq_iInter_cthickening]

Result:
α : Type u_1
inst✝² : PseudoEMetricSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, μ (cthickening R s) ≠ ⊤
⊢ Tendsto (fun r => μ (cthickening r s)) (𝓝[>] 0) (𝓝 (μ (⋂ δ, ⋂ (_ : 0 < δ), cthickening δ s)))

Proof state:
case h.e'_4
α : Type u_1
inst✝² : PseudoEMetricSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, μ (cthickening R s) ≠ ⊤
A : Tendsto (fun r => μ (cthickening r s)) (𝓝[>] 0) (𝓝 (μ (closure s)))
B : Tendsto (fun r => μ (cthickening r s)) (𝓝[≤] 0) (𝓝 (μ (closure s)))
⊢ 𝓝 0 = 𝓝[≤] 0 ⊔ 𝓝[>] 0

Tactic:
exact (nhdsLE_sup_nhdsGT 0).symm

Result:
no goals

Proof state:
α : Type u_1
inst✝² : PseudoEMetricSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, μ (cthickening R s) ≠ ⊤
A : Tendsto (fun r => μ (cthickening r s)) (𝓝[>] 0) (𝓝 (μ (closure s)))
⊢ (fun x => μ (closure s)) =ᶠ[𝓝[≤] 0] fun r => μ (cthickening r s)

Tactic:
filter_upwards [self_mem_nhdsWithin (α := ℝ)] with _ hr

Result:
case h
α : Type u_1
inst✝² : PseudoEMetricSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, μ (cthickening R s) ≠ ⊤
A : Tendsto (fun r => μ (cthickening r s)) (𝓝[>] 0) (𝓝 (μ (closure s)))
a✝ : ℝ
hr : a✝ ∈ Iic 0
⊢ μ (closure s) = μ (cthickening a✝ s)

Proof state:
α : Type u_1
inst✝² : PseudoEMetricSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, μ (cthickening R s) ≠ ⊤
⊢ Tendsto (fun r => μ (cthickening r s)) (𝓝[>] 0) (𝓝 (μ (⋂ δ, ⋂ (_ : 0 < δ), cthickening δ s)))

Tactic:
exact
  tendsto_measure_biInter_gt (fun r _ => isClosed_cthickening.nullMeasurableSet)
    (fun i j _ ij => cthickening_mono ij _) hs

Result:
no goals

Proof state:
α : Type u_1
inst✝² : PseudoEMetricSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, μ (cthickening R s) ≠ ⊤
A : Tendsto (fun r => μ (cthickening r s)) (𝓝[>] 0) (𝓝 (μ (closure s)))
⊢ Tendsto (fun r => μ (cthickening r s)) (𝓝[≤] 0) (𝓝 (μ (closure s)))

Tactic:
apply Tendsto.congr' _ tendsto_const_nhds

Result:
α : Type u_1
inst✝² : PseudoEMetricSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, μ (cthickening R s) ≠ ⊤
A : Tendsto (fun r => μ (cthickening r s)) (𝓝[>] 0) (𝓝 (μ (closure s)))
⊢ (fun x => μ (closure s)) =ᶠ[𝓝[≤] 0] fun r => μ (cthickening r s)

Proof state:
case h
α : Type u_1
inst✝² : PseudoEMetricSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, μ (cthickening R s) ≠ ⊤
A : Tendsto (fun r => μ (cthickening r s)) (𝓝[>] 0) (𝓝 (μ (closure s)))
a✝ : ℝ
hr : a✝ ∈ Iic 0
⊢ μ (closure s) = μ (cthickening a✝ s)

Tactic:
rw [cthickening_of_nonpos hr]

Result:
no goals