awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
x : α
ε : ℝ
⊢ MeasurableSet (ball x ε)

Tactic:
Metric.isOpen_ball.measurableSet

Premises used: IsOpen.measurableSet, Metric.isOpen_ball
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
x : α
ε : ℝ
⊢ MeasurableSet (closedBall x ε)

Tactic:
Metric.isClosed_closedBall.measurableSet

Premises used: Metric.isClosed_closedBall, IsClosed.measurableSet
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
s : Set α
⊢ Measurable (β := ℝ) fun (x : α) ↦ infDist x s

Tactic:
(continuous_infDist_pt s).measurable

Premises used: Continuous.measurable, Metric.continuous_infDist_pt
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
⊢ Measurable (β := ℝ) fun (x : β) ↦ Metric.infDist (f x) s

Tactic:
measurable_infDist.comp hf

Premises used: Measurable.comp, Metric.infDist, ENNReal.toReal, measurable_infDist, NNReal.toReal
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
s : Set α
⊢ Measurable (β := ℝ≥0) fun (x : α) ↦ infNndist x s

Tactic:
(continuous_infNndist_pt s).measurable

Premises used: Metric.continuous_infNndist_pt, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
⊢ Measurable (β := ℝ≥0) fun (x : β) ↦ Metric.infNndist (f x) s

Tactic:
measurable_infNndist.comp hf

Premises used: Measurable.comp, ENNReal.toNNReal, Metric.infNndist, measurable_infNndist, WithTop.untopD, WithTop.recTopCoe
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : SecondCountableTopology α
⊢ Measurable (β := ℝ) fun (p : α × α) ↦ dist p.1 p.2

Tactic:
continuous_dist.measurable

Premises used: continuous_dist, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
inst_4 : SecondCountableTopology α
f g : β → α
hf : Measurable f
hg : Measurable g
⊢ Measurable (β := ℝ) fun (b : β) ↦ Dist.dist (f b) (g b)

Tactic:
continuous_dist.measurable2 hf hg

Premises used: continuous_dist, Continuous.measurable2
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
inst_4 : SecondCountableTopology α
f g : β → α
μ : Measure β
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ AEMeasurable (β := ℝ) (fun (b : β) ↦ Dist.dist (f b) (g b)) μ

Tactic:
continuous_dist.aemeasurable2 hf hg

Premises used: continuous_dist, Continuous.aemeasurable2
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : SecondCountableTopology α
⊢ Measurable (β := ℝ≥0) fun (p : α × α) ↦ nndist p.1 p.2

Tactic:
continuous_nndist.measurable

Premises used: Continuous.measurable, continuous_nndist
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
inst_4 : SecondCountableTopology α
f g : β → α
hf : Measurable f
hg : Measurable g
⊢ Measurable (β := ℝ≥0) fun (b : β) ↦ NNDist.nndist (f b) (g b)

Tactic:
continuous_nndist.measurable2 hf hg

Premises used: Continuous.measurable2, continuous_nndist
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
x : α
ε : ℝ≥0∞
⊢ MeasurableSet (eball x ε)

Tactic:
Metric.isOpen_eball.measurableSet

Premises used: Metric.isOpen_eball, IsOpen.measurableSet
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
x : α
funProp : inst_1 ≤ inst_1
funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (a : α) ↦ edist x a
⊢ Measurable (edist x)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
x : α
funProp : inst_1 ≤ inst_1
funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (y : α) ↦ edist y x
⊢ Measurable (β := ℝ≥0∞) fun (y : α) ↦ edist y x

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
s : Set α
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ infEDist x s

Tactic:
continuous_infEDist.measurable

Premises used: Continuous.measurable, Metric.continuous_infEDist
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
⊢ Measurable (β := ℝ≥0∞) fun (x : β) ↦ infEDist (f x) s

Tactic:
measurable_infEDist.comp hf

Premises used: iInf, Measurable.comp, measurable_infEDist, Metric.infEDist
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (cthickening R s) : ℝ≥0∞) (∞ : ℝ≥0∞)
rw :
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (cthickening r s) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (δ : ℝ), ⋂ (_ : 0 < δ), cthickening δ s)) : Filter ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (cthickening r s) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)

Tactic:
rw [closure_eq_iInter_cthickening]

Premises used: Metric.closure_eq_iInter_cthickening
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (cthickening R s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (cthickening r s) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (δ : ℝ), ⋂ (_ : 0 < δ), cthickening δ s)) : Filter ℝ≥0∞)

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

Premises used: Metric.cthickening_mono, MeasureTheory.tendsto_measure_biInter_gt, IsClosed.nullMeasurableSet, Metric.isClosed_cthickening
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (cthickening R s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (cthickening r s) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (δ : ℝ), ⋂ (_ : 0 < δ), cthickening δ s)) : Filter ℝ≥0∞)

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

Premises used: Metric.cthickening_mono, MeasureTheory.tendsto_measure_biInter_gt, IsClosed.nullMeasurableSet, Metric.isClosed_cthickening
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (cthickening R s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (cthickening r s) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)

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
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (cthickening R s) : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (cthickening r s) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)
apply :
  EventuallyEq (β := ℝ≥0∞) (𝓝[≤] 0)
    (fun (x : ℝ) ↦ (μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s))
    fun (r : ℝ) ↦ (μ : (a : Set α) → ℝ≥0∞) (cthickening r s)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (cthickening r s) : ℝ≥0∞)) (𝓝[≤] 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)

Tactic:
apply Tendsto.congr' _ tendsto_const_nhds

Premises used: tendsto_const_nhds, Filter.Tendsto.congr'
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (cthickening R s) : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (cthickening r s) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)
h :
  ∀ (a : ℝ) (hr : Membership.mem (γ := Set ℝ) (Iic 0) a),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (cthickening a s) : ℝ≥0∞)
⊢ EventuallyEq (β := ℝ≥0∞) (𝓝[≤] 0)
    (fun (x : ℝ) ↦ (μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s))
    fun (r : ℝ) ↦ (μ : (a : Set α) → ℝ≥0∞) (cthickening r s)

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

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (cthickening R s) : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (cthickening r s) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)
a : ℝ
hr : Membership.mem (γ := Set ℝ) (Iic 0) a
h h₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (cthickening a s) : ℝ≥0∞)

Tactic:
rw [cthickening_of_nonpos hr]

Premises used: Metric.cthickening_of_nonpos
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (cthickening R s) : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (cthickening r s) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (cthickening r s) : ℝ≥0∞)) (𝓝[≤] 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)

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]
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (cthickening R s) : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (cthickening r s) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)
B :
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (cthickening r s) : ℝ≥0∞)) (𝓝[≤] 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (cthickening r s) : ℝ≥0∞)) (𝓝[≤] 0 ⊔ 𝓝[>] 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)

Tactic:
B.sup A

Premises used: Filter.Tendsto.sup
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (cthickening R s) : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (cthickening r s) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)
B :
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (cthickening r s) : ℝ≥0∞)) (𝓝[≤] 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)
h : Eq (α := Filter ℝ) (𝓝 0) (𝓝[≤] 0 ⊔ 𝓝[>] 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (cthickening r s) : ℝ≥0∞)) (𝓝 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)

Tactic:
convert! B.sup A

Premises used: Filter.Tendsto.sup
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (cthickening R s) : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (cthickening r s) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)
B :
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (cthickening r s) : ℝ≥0∞)) (𝓝[≤] 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)
⊢ Eq (α := Filter ℝ) (𝓝 0) (𝓝[≤] 0 ⊔ 𝓝[>] 0)

Tactic:
(nhdsLE_sup_nhdsGT 0).symm

Premises used: Set.Mem, setOf, nhdsLE_sup_nhdsGT, OfNat.ofNat, Eq.symm
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (cthickening R s) : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (cthickening r s) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)
B :
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (cthickening r s) : ℝ≥0∞)) (𝓝[≤] 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)
⊢ Eq (α := Filter ℝ) (𝓝 0) (𝓝[≤] 0 ⊔ 𝓝[>] 0)

Tactic:
exact (nhdsLE_sup_nhdsGT 0).symm

Premises used: nhdsLE_sup_nhdsGT, OfNat.ofNat, Eq.symm
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (cthickening R s) : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (cthickening r s) : ℝ≥0∞)) (𝓝 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)

Tactic:
tendsto_measure_cthickening hs

Premises used: tendsto_measure_cthickening
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (cthickening R s) : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
h : s = closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (cthickening r s) : ℝ≥0∞)) (𝓝 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)

Tactic:
convert! tendsto_measure_cthickening hs

Premises used: tendsto_measure_cthickening
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (cthickening R s) : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ s = closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s

Tactic:
h's.closure_eq.symm

Premises used: IsClosed.closure_eq, Eq.symm
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (cthickening R s) : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ s = closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s

Tactic:
exact h's.closure_eq.symm

Premises used: IsClosed.closure_eq, Eq.symm
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (thickening R s) : ℝ≥0∞) (∞ : ℝ≥0∞)
rw :
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (thickening r s) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (δ : ℝ), ⋂ (_ : 0 < δ), thickening δ s)) : Filter ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (thickening r s) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)

Tactic:
rw [closure_eq_iInter_thickening]

Premises used: Metric.closure_eq_iInter_thickening
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (thickening R s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (thickening r s) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (δ : ℝ), ⋂ (_ : 0 < δ), thickening δ s)) : Filter ℝ≥0∞)

Tactic:
tendsto_measure_biInter_gt (fun r _ => isOpen_thickening.nullMeasurableSet)
      (fun i j _ ij => thickening_mono ij _) hs

Premises used: MeasureTheory.tendsto_measure_biInter_gt, Metric.isOpen_thickening, IsOpen.nullMeasurableSet, Metric.thickening_mono
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (thickening R s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (thickening r s) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (δ : ℝ), ⋂ (_ : 0 < δ), thickening δ s)) : Filter ℝ≥0∞)

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

Premises used: MeasureTheory.tendsto_measure_biInter_gt, Metric.isOpen_thickening, IsOpen.nullMeasurableSet, Metric.thickening_mono
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (thickening R s) : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (thickening r s) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)

Tactic:
tendsto_measure_thickening hs

Premises used: tendsto_measure_thickening
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (thickening R s) : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
h : s = closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (thickening r s) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)

Tactic:
convert! tendsto_measure_thickening hs

Premises used: tendsto_measure_thickening
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (thickening R s) : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ s = closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s

Tactic:
h's.closure_eq.symm

Premises used: IsClosed.closure_eq, Eq.symm
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (thickening R s) : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ s = closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s

Tactic:
exact h's.closure_eq.symm

Premises used: IsClosed.closure_eq, Eq.symm
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : SecondCountableTopology α
⊢ Measurable (β := ℝ≥0∞) fun (p : α × α) ↦ edist p.1 p.2

Tactic:
continuous_edist.measurable

Premises used: continuous_edist, Continuous.measurable