awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSingletonClass α
f : β → α
a₁ a₂ : α
μ : Measure β
hf : AEMeasurable f μ
ha : a₁ ≠ a₂
⊢ HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set β) → ℝ≥0∞) (f ⁻¹' {a₁}) : ℝ≥0∞) (dirac a₁) +
      HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set β) → ℝ≥0∞) (f ⁻¹' {a₂}) : ℝ≥0∞) (dirac a₂) =
    ∑ a ∈ Finset.cons a₁ {a₂} ⋯,
      HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set β) → ℝ≥0∞) (f ⁻¹' {a}) : ℝ≥0∞) (dirac a)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
K : Set X
K_closed : IsClosed[inst] K
x : X
x_notin_K : x ∉ K
obtain :
  ∀ (g : X → (↑unitInterval : Type)) (g_cont : Continuous[inst, _] g) (gx_zero : g x = 0) (g_one_on_K : EqOn g 1 K),
    ∃ (f : X →ᵇ ℝ≥0),
      Eq (α := ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0) ∧
        ∀ y ∈ K, Eq (α := ℝ≥0) ((f : (a : X) → ℝ≥0) y : ℝ≥0) (0 : ℝ≥0)
⊢ ∃ (f : X →ᵇ ℝ≥0),
    Eq (α := ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0) ∧
      ∀ y ∈ K, Eq (α := ℝ≥0) ((f : (a : X) → ℝ≥0) y : ℝ≥0) (0 : ℝ≥0)

Tactic:
obtain ⟨g, g_cont, gx_zero, g_one_on_K⟩ :=
    CompletelyRegularSpace.completely_regular x K K_closed x_notin_K

Premises used: CompletelyRegularSpace.completely_regular
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
K : Set X
K_closed : IsClosed[inst] K
x : X
x_notin_K : x ∉ K
g : X → (↑unitInterval : Type)
g_cont : Continuous[inst, _] g
gx_zero : g x = 0
g_one_on_K : EqOn g 1 K
⊢ ∀ (x y : X), dist (↑(g x) : ℝ).toNNReal (↑(g y) : ℝ).toNNReal ≤ 1

Tactic:
fun x y ↦ ((Real.lipschitzWith_toNNReal).dist_le_mul (g x) (g y)).trans ?_

Premises used: LipschitzWith.dist_le_mul, Real.lipschitzWith_toNNReal, LE.le.trans, Subtype.val
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
K : Set X
K_closed : IsClosed[inst] K
x : X
x_notin_K : x ∉ K
g : X → (↑unitInterval : Type)
g_cont : Continuous[inst, _] g
gx_zero : g x = 0
g_one_on_K : EqOn g 1 K
refine : ∀ (x y : X), (↑1 : ℝ) * dist (↑(g x) : ℝ) (↑(g y) : ℝ) ≤ 1
⊢ ∀ (x y : X), dist (↑(g x) : ℝ).toNNReal (↑(g y) : ℝ).toNNReal ≤ 1

Tactic:
refine fun x y ↦ ((Real.lipschitzWith_toNNReal).dist_le_mul (g x) (g y)).trans ?_

Premises used: LipschitzWith.dist_le_mul, Real.lipschitzWith_toNNReal, LE.le.trans, Subtype.val
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
K : Set X
K_closed : IsClosed[inst] K
x_1 : X
x_notin_K : x_1 ∉ K
g : X → (↑unitInterval : Type)
g_cont : Continuous[inst, _] g
gx_zero : g x_1 = 0
g_one_on_K : EqOn g 1 K
x y : X
⊢ (↑1 : ℝ) * dist (↑(g x) : ℝ) (↑(g y) : ℝ) ≤ 1

Tactic:
simpa using Real.dist_le_of_mem_Icc_01 (g x).prop (g y).prop

Premises used: Real.dist_le_of_mem_Icc_01, Subtype.prop
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
K : Set X
K_closed : IsClosed[inst] K
x : X
x_notin_K : x ∉ K
g : X → (↑unitInterval : Type)
g_cont : Continuous[inst, _] g
gx_zero : g x = 0
g_one_on_K : EqOn g 1 K
⊢ ∀ (x y : X), dist (↑(g x) : ℝ).toNNReal (↑(g y) : ℝ).toNNReal ≤ 1

Tactic:
have g_bdd : ∀ x y, dist (Real.toNNReal (g x)) (Real.toNNReal (g y)) ≤ 1 := by
    refine fun x y ↦ ((Real.lipschitzWith_toNNReal).dist_le_mul (g x) (g y)).trans ?_
    simpa using Real.dist_le_of_mem_Icc_01 (g x).prop (g y).prop
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
K : Set X
K_closed : IsClosed[inst] K
x : X
x_notin_K : x ∉ K
g : X → (↑unitInterval : Type)
g_cont : Continuous[inst, _] g
gx_zero : g x = 0
g_one_on_K : EqOn g 1 K
g_bdd : ∀ (x y : X), dist (↑(g x) : ℝ).toNNReal (↑(g y) : ℝ).toNNReal ≤ 1
g' : X →ᵇ ℝ≥0 := mkOfBound { toFun := fun (x : X) ↦ (↑(g x) : ℝ).toNNReal, continuous_toFun := ⋯ } 1 g_bdd
f : X →ᵇ ℝ≥0 := 1 - g'
⊢ Eq (α := ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)

Tactic:
simp [f, g', gx_zero]
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
K : Set X
K_closed : IsClosed[inst] K
x : X
x_notin_K : x ∉ K
g : X → (↑unitInterval : Type)
g_cont : Continuous[inst, _] g
gx_zero : g x = 0
g_one_on_K : EqOn g 1 K
g_bdd : ∀ (x y : X), dist (↑(g x) : ℝ).toNNReal (↑(g y) : ℝ).toNNReal ≤ 1
g' : X →ᵇ ℝ≥0 := mkOfBound { toFun := fun (x : X) ↦ (↑(g x) : ℝ).toNNReal, continuous_toFun := ⋯ } 1 g_bdd
f : X →ᵇ ℝ≥0 := 1 - g'
y : X
y_in_K : y ∈ K
⊢ Eq (α := ℝ≥0) ((f : (a : X) → ℝ≥0) y : ℝ≥0) (0 : ℝ≥0)

Tactic:
simp [f, g', g_one_on_K y_in_K, tsub_self]

Premises used: tsub_self
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
K : Set X
K_closed : IsClosed[inst] K
x : X
x_notin_K : x ∉ K
g : X → (↑unitInterval : Type)
g_cont : Continuous[inst, _] g
gx_zero : g x = 0
g_one_on_K : EqOn g 1 K
g_bdd : ∀ (x y : X), dist (↑(g x) : ℝ).toNNReal (↑(g y) : ℝ).toNNReal ≤ 1
g' : X →ᵇ ℝ≥0 := mkOfBound { toFun := fun (x : X) ↦ (↑(g x) : ℝ).toNNReal, continuous_toFun := ⋯ } 1 g_bdd
f : X →ᵇ ℝ≥0 := 1 - g'
⊢ ∃ (f : X →ᵇ ℝ≥0),
    Eq (α := ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0) ∧
      ∀ y ∈ K, Eq (α := ℝ≥0) ((f : (a : X) → ℝ≥0) y : ℝ≥0) (0 : ℝ≥0)

Tactic:
refine ⟨f, by simp [f, g', gx_zero], fun y y_in_K ↦ by simp [f, g', g_one_on_K y_in_K, tsub_self]⟩
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_2
inst : MeasurableSpace X
inst_1 : MeasurableSpace.SeparatesPoints X
x y : X
x_eq_y :
  Eq.{u_2 + 1} (α := ProbabilityMeasure X) ((fun (x : X) ↦ (diracProba x : ProbabilityMeasure X)) x)
    ((fun (x : X) ↦ (diracProba x : ProbabilityMeasure X)) y)
rw : Eq (α := Measure X) (Measure.dirac x) (Measure.dirac y)
⊢ x = y

Tactic:
rw [← dirac_eq_dirac_iff]

Premises used: MeasureTheory.dirac_eq_dirac_iff
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_2
inst : MeasurableSpace X
inst_1 : MeasurableSpace.SeparatesPoints X
x y : X
x_eq_y :
  Eq.{u_2 + 1} (α := ProbabilityMeasure X) ((fun (x : X) ↦ (diracProba x : ProbabilityMeasure X)) x)
    ((fun (x : X) ↦ (diracProba x : ProbabilityMeasure X)) y)
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (x_eq_y :
      Eq.{u_2 + 1} (α := Measure X) (↑((fun (x : X) ↦ (diracProba x : ProbabilityMeasure X)) x) : Measure X)
        (↑((fun (x : X) ↦ (diracProba x : ProbabilityMeasure X)) y) : Measure X)),
    Eq (α := Measure X) (Measure.dirac x) (Measure.dirac y)
⊢ Eq (α := Measure X) (Measure.dirac x) (Measure.dirac y)

Tactic:
rwa [Subtype.ext_iff] at x_eq_y

Premises used: Subtype.ext_iff
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : MeasurableSpace X
x : X
A : Set X
A_mble : MeasurableSet A
⊢ Eq (α := ℝ≥0∞) ((((↑(diracProba x) : Measure X) : Measure X) : (a : Set X) → ℝ≥0∞) A : ℝ≥0∞) (A.indicator 1 x : ℝ≥0∞)

Tactic:
Measure.dirac_apply' x A_mble

Premises used: MeasureTheory.Measure.dirac_apply'
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : MeasurableSpace X
x : X
A : Set X
x_in_A : x ∈ A
⊢ Eq (α := ℝ≥0∞) ((((↑(diracProba x) : Measure X) : Measure X) : (a : Set X) → ℝ≥0∞) A : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
Measure.dirac_apply_of_mem x_in_A

Premises used: MeasureTheory.Measure.dirac_apply_of_mem
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : MeasurableSingletonClass X
x : X
A : Set X
⊢ Eq (α := ℝ≥0∞) ((((↑(diracProba x) : Measure X) : Measure X) : (a : Set X) → ℝ≥0∞) A : ℝ≥0∞) (A.indicator 1 x : ℝ≥0∞)

Tactic:
Measure.dirac_apply _ _

Premises used: MeasureTheory.Measure.dirac_apply
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
rw : ∀ (x : X), ContinuousAt (Y := ProbabilityMeasure X) (fun (x : X) ↦ diracProba x) x
⊢ Continuous[inst_1, ProbabilityMeasure.instTopologicalSpace] fun (x : X) ↦ diracProba x

Tactic:
rw [continuous_iff_continuousAt]

Premises used: continuous_iff_continuousAt
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
apply :
  ∀ (x : X) (f : X →ᵇ ℝ≥0),
    Tendsto (fun (i : X) ↦ ∫⁻ (ω : X), (↑((f : (a : X) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(diracProba i) : Measure X)) (𝓝 x)
      (𝓝 (∫⁻ (ω : X), (↑((f : (a : X) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(diracProba x) : Measure X)))
⊢ ∀ (x : X), ContinuousAt (Y := ProbabilityMeasure X) (fun (x : X) ↦ diracProba x) x

Tactic:
apply fun x ↦ ProbabilityMeasure.tendsto_iff_forall_lintegral_tendsto.mpr fun f ↦ ?_

Premises used: Iff.mpr, MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_lintegral_tendsto
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
x : X
f : X →ᵇ ℝ≥0
⊢ Measurable (β := ℝ≥0∞) fun (X_1 : X) ↦ (↑((f : (a : X) → ℝ≥0) X_1) : ℝ≥0∞)

Tactic:
have f_mble : Measurable (fun X ↦ (f X : ℝ≥0∞)) :=
    measurable_coe_nnreal_ennreal_iff.mpr f.continuous.measurable
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
x : X
f : X →ᵇ ℝ≥0
f_mble : Measurable (β := ℝ≥0∞) fun (X_1 : X) ↦ (↑((f : (a : X) → ℝ≥0) X_1) : ℝ≥0∞)
simp : Tendsto (fun (ω : X) ↦ (↑((f : (a : X) → ℝ≥0) ω) : ℝ≥0∞)) (𝓝 x) (𝓝 (↑((f : (a : X) → ℝ≥0) x) : ℝ≥0∞))
⊢ Tendsto (fun (i : X) ↦ ∫⁻ (ω : X), (↑((f : (a : X) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(diracProba i) : Measure X)) (𝓝 x)
    (𝓝 (∫⁻ (ω : X), (↑((f : (a : X) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(diracProba x) : Measure X)))

Tactic:
simp only [diracProba, ProbabilityMeasure.coe_mk, lintegral_dirac' _ f_mble]

Premises used: MeasureTheory.ProbabilityMeasure.coe_mk, MeasureTheory.diracProba, MeasureTheory.lintegral_dirac'
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
x : X
f : X →ᵇ ℝ≥0
f_mble : Measurable (β := ℝ≥0∞) fun (X_1 : X) ↦ (↑((f : (a : X) → ℝ≥0) X_1) : ℝ≥0∞)
⊢ Tendsto (fun (ω : X) ↦ (↑((f : (a : X) → ℝ≥0) ω) : ℝ≥0∞)) (𝓝 x) (𝓝 (↑((f : (a : X) → ℝ≥0) x) : ℝ≥0∞))

Tactic:
(ENNReal.continuous_coe.comp f.continuous).continuousAt

Premises used: ENNReal.ofNNReal, ContinuousAt, Continuous.comp, BoundedContinuousFunction.continuous, WithTop.some, Continuous.continuousAt, ENNReal.continuous_coe
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
x : X
f : X →ᵇ ℝ≥0
f_mble : Measurable (β := ℝ≥0∞) fun (X_1 : X) ↦ (↑((f : (a : X) → ℝ≥0) X_1) : ℝ≥0∞)
⊢ Tendsto (fun (ω : X) ↦ (↑((f : (a : X) → ℝ≥0) ω) : ℝ≥0∞)) (𝓝 x) (𝓝 (↑((f : (a : X) → ℝ≥0) x) : ℝ≥0∞))

Tactic:
exact (ENNReal.continuous_coe.comp f.continuous).continuousAt

Premises used: Continuous.comp, BoundedContinuousFunction.continuous, Continuous.continuousAt, ENNReal.continuous_coe
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : CompletelyRegularSpace X
x : X
L : Filter X
h : ¬Tendsto id L (𝓝 x)
contrapose! : ∀ (h : ∀ (U : Set X) (_ : U ∈ 𝓝 x), ∀ᶠ (x : X) in L, x ∈ U), Tendsto id L (𝓝 x)
⊢ ∃ U ∈ 𝓝 x, ∃ᶠ (x : X) in L, x ∉ U

Tactic:
contrapose! h
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : CompletelyRegularSpace X
x : X
L : Filter X
h : ∀ (U : Set X) (_ : U ∈ 𝓝 x), ∀ᶠ (x : X) in L, x ∈ U
⊢ Tendsto id L (𝓝 x)

Tactic:
h

Premises used: Set.Mem, Filter.Eventually, setOf, Set.preimage, Filter.Tendsto
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : CompletelyRegularSpace X
x : X
L : Filter X
h : ∀ (U : Set X) (_ : U ∈ 𝓝 x), ∀ᶠ (x : X) in L, x ∈ U
⊢ Tendsto id L (𝓝 x)

Tactic:
exact h
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : CompletelyRegularSpace X
x : X
L : Filter X
h : ¬Tendsto id L (𝓝 x)
obtain :
  ∀ (U : Set X) (U_nhds : U ∈ 𝓝 x) (hU : ∃ᶠ (x : X) in L, x ∉ U),
    ¬Tendsto (β := ProbabilityMeasure X) diracProba L (𝓝 (diracProba x))
⊢ ¬Tendsto (β := ProbabilityMeasure X) diracProba L (𝓝 (diracProba x))

Tactic:
obtain ⟨U, U_nhds, hU⟩ : ∃ U, U ∈ 𝓝 x ∧ ∃ᶠ x in L, x ∉ U := by
    contrapose! h
    exact h

Premises used: nhds
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : CompletelyRegularSpace X
x : X
L : Filter X
h : ¬Tendsto id L (𝓝 x)
U : Set X
U_nhds : U ∈ 𝓝 x
hU : ∃ᶠ (x : X) in L, x ∉ U
⊢ interior U ∈ 𝓝 x

Tactic:
simpa only [interior_mem_nhds] using U_nhds

Premises used: interior_mem_nhds
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : CompletelyRegularSpace X
x : X
L : Filter X
h : ¬Tendsto id L (𝓝 x)
U : Set X
U_nhds : U ∈ 𝓝 x
hU : ∃ᶠ (x : X) in L, x ∉ U
⊢ interior U ∈ 𝓝 x

Tactic:
have Uint_nhds : interior U ∈ 𝓝 x := by simpa only [interior_mem_nhds] using U_nhds
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : CompletelyRegularSpace X
x : X
L : Filter X
h : ¬Tendsto id L (𝓝 x)
U : Set X
U_nhds : U ∈ 𝓝 x
hU : ∃ᶠ (x : X) in L, x ∉ U
Uint_nhds : interior U ∈ 𝓝 x
⊢ x ∉ (interior U)ᶜ

Tactic:
simpa only [mem_compl_iff, not_not] using mem_of_mem_nhds Uint_nhds

Premises used: Classical.not_not, mem_of_mem_nhds, Set.mem_compl_iff
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : CompletelyRegularSpace X
x : X
L : Filter X
h : ¬Tendsto id L (𝓝 x)
U : Set X
U_nhds : U ∈ 𝓝 x
hU : ∃ᶠ (x : X) in L, x ∉ U
Uint_nhds : interior U ∈ 𝓝 x
obtain :
  ∀ (f : X →ᵇ ℝ≥0) (fx_eq_one : Eq (α := ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0))
    (f_vanishes_outside : ∀ y ∈ (interior U)ᶜ, Eq (α := ℝ≥0) ((f : (a : X) → ℝ≥0) y : ℝ≥0) (0 : ℝ≥0)),
    ¬Tendsto (β := ProbabilityMeasure X) diracProba L (𝓝 (diracProba x))
⊢ ¬Tendsto (β := ProbabilityMeasure X) diracProba L (𝓝 (diracProba x))

Tactic:
obtain ⟨f, fx_eq_one, f_vanishes_outside⟩ :=
    CompletelyRegularSpace.exists_BCNN isOpen_interior.isClosed_compl
      (by simpa only [mem_compl_iff, not_not] using mem_of_mem_nhds Uint_nhds)

Premises used: isOpen_interior, IsOpen.isClosed_compl, CompletelyRegularSpace.exists_BCNN
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : CompletelyRegularSpace X
x : X
L : Filter X
h : ¬Tendsto id L (𝓝 x)
U : Set X
U_nhds : U ∈ 𝓝 x
hU : ∃ᶠ (x : X) in L, x ∉ U
Uint_nhds : interior U ∈ 𝓝 x
f : X →ᵇ ℝ≥0
fx_eq_one : Eq (α := ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)
f_vanishes_outside : ∀ y ∈ (interior U)ᶜ, Eq (α := ℝ≥0) ((f : (a : X) → ℝ≥0) y : ℝ≥0) (0 : ℝ≥0)
rw :
  ∃ (x_1 : X →ᵇ ℝ≥0),
    ¬Tendsto (fun (i : X) ↦ ∫⁻ (ω : X), (↑((x_1 : (a : X) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(diracProba i) : Measure X)) L
        (𝓝 (∫⁻ (ω : X), (↑((x_1 : (a : X) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(diracProba x) : Measure X)))
⊢ ¬Tendsto (β := ProbabilityMeasure X) diracProba L (𝓝 (diracProba x))

Tactic:
rw [ProbabilityMeasure.tendsto_iff_forall_lintegral_tendsto, not_forall]

Premises used: Classical.not_forall, MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_lintegral_tendsto
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : CompletelyRegularSpace X
x : X
L : Filter X
h : ¬Tendsto id L (𝓝 x)
U : Set X
U_nhds : U ∈ 𝓝 x
hU : ∃ᶠ (x : X) in L, x ∉ U
Uint_nhds : interior U ∈ 𝓝 x
f : X →ᵇ ℝ≥0
fx_eq_one : Eq (α := ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)
f_vanishes_outside : ∀ y ∈ (interior U)ᶜ, Eq (α := ℝ≥0) ((f : (a : X) → ℝ≥0) y : ℝ≥0) (0 : ℝ≥0)
h₁ :
  ¬Tendsto (fun (i : X) ↦ ∫⁻ (ω : X), (↑((f : (a : X) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(diracProba i) : Measure X)) L
      (𝓝 (∫⁻ (ω : X), (↑((f : (a : X) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(diracProba x) : Measure X)))
⊢ ∃ (x_1 : X →ᵇ ℝ≥0),
    ¬Tendsto (fun (i : X) ↦ ∫⁻ (ω : X), (↑((x_1 : (a : X) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(diracProba i) : Measure X)) L
        (𝓝 (∫⁻ (ω : X), (↑((x_1 : (a : X) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(diracProba x) : Measure X)))

Tactic:
use f
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : CompletelyRegularSpace X
x : X
L : Filter X
h : ¬Tendsto id L (𝓝 x)
U : Set X
U_nhds : U ∈ 𝓝 x
hU : ∃ᶠ (x : X) in L, x ∉ U
Uint_nhds : interior U ∈ 𝓝 x
f : X →ᵇ ℝ≥0
fx_eq_one : Eq (α := ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)
f_vanishes_outside : ∀ y ∈ (interior U)ᶜ, Eq (α := ℝ≥0) ((f : (a : X) → ℝ≥0) y : ℝ≥0) (0 : ℝ≥0)
h₁ : ¬Tendsto (fun (i : X) ↦ (↑((f : (a : X) → ℝ≥0) i) : ℝ≥0∞)) L (𝓝 (↑1 : ℝ≥0∞))
⊢ ¬Tendsto (fun (i : X) ↦ ∫⁻ (ω : X), (↑((f : (a : X) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(diracProba i) : Measure X)) L
      (𝓝 (∫⁻ (ω : X), (↑((f : (a : X) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(diracProba x) : Measure X)))

Tactic:
simp only [diracProba, ProbabilityMeasure.coe_mk, fx_eq_one,
             lintegral_dirac' _ (measurable_coe_nnreal_ennreal_iff.mpr f.continuous.measurable)]

Premises used: Iff.mpr, MeasureTheory.ProbabilityMeasure.coe_mk, MeasureTheory.diracProba, MeasureTheory.lintegral_dirac', BoundedContinuousFunction.continuous, Continuous.measurable, measurable_coe_nnreal_ennreal_iff
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : CompletelyRegularSpace X
x : X
L : Filter X
h : ¬Tendsto id L (𝓝 x)
U : Set X
U_nhds : U ∈ 𝓝 x
hU : ∃ᶠ (x : X) in L, x ∉ U
Uint_nhds : interior U ∈ 𝓝 x
f : X →ᵇ ℝ≥0
fx_eq_one : Eq (α := ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)
f_vanishes_outside : ∀ y ∈ (interior U)ᶜ, Eq (α := ℝ≥0) ((f : (a : X) → ℝ≥0) y : ℝ≥0) (0 : ℝ≥0)
h₁ : ∃ s ∈ 𝓝 (↑1 : ℝ≥0∞), ∃ᶠ (x : X) in L, (↑((f : (a : X) → ℝ≥0) x) : ℝ≥0∞) ∉ s
⊢ ¬Tendsto (fun (i : X) ↦ (↑((f : (a : X) → ℝ≥0) i) : ℝ≥0∞)) L (𝓝 (↑1 : ℝ≥0∞))

Tactic:
apply not_tendsto_iff_exists_frequently_notMem.mpr

Premises used: Iff.mpr, Filter.not_tendsto_iff_exists_frequently_notMem
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : CompletelyRegularSpace X
x : X
L : Filter X
h : ¬Tendsto id L (𝓝 x)
U : Set X
U_nhds : U ∈ 𝓝 x
hU : ∃ᶠ (x : X) in L, x ∉ U
Uint_nhds : interior U ∈ 𝓝 x
f : X →ᵇ ℝ≥0
fx_eq_one : Eq (α := ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)
f_vanishes_outside : ∀ y ∈ (interior U)ᶜ, Eq (α := ℝ≥0) ((f : (a : X) → ℝ≥0) y : ℝ≥0) (0 : ℝ≥0)
⊢ 0 < (↑1 : ℝ≥0∞)

Tactic:
simp only [ENNReal.coe_one, zero_lt_one]

Premises used: ENNReal.coe_one, zero_lt_one
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : CompletelyRegularSpace X
x : X
L : Filter X
h : ¬Tendsto id L (𝓝 x)
U : Set X
U_nhds : U ∈ 𝓝 x
hU : ∃ᶠ (x : X) in L, x ∉ U
Uint_nhds : interior U ∈ 𝓝 x
f : X →ᵇ ℝ≥0
fx_eq_one : Eq (α := ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)
f_vanishes_outside : ∀ y ∈ (interior U)ᶜ, Eq (α := ℝ≥0) ((f : (a : X) → ℝ≥0) y : ℝ≥0) (0 : ℝ≥0)
h₁ : ∀ x ∉ U, (↑((f : (a : X) → ℝ≥0) x) : ℝ≥0∞) ∉ Ioi 0
⊢ ∃ s ∈ 𝓝 (↑1 : ℝ≥0∞), ∃ᶠ (x : X) in L, (↑((f : (a : X) → ℝ≥0) x) : ℝ≥0∞) ∉ s

Tactic:
refine ⟨Ioi 0, Ioi_mem_nhds (by simp only [ENNReal.coe_one, zero_lt_one]),
          hU.mp (Eventually.of_forall ?_)⟩
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : CompletelyRegularSpace X
x_1 : X
L : Filter X
h : ¬Tendsto id L (𝓝 x_1)
U : Set X
U_nhds : U ∈ 𝓝 x_1
hU : ∃ᶠ (x : X) in L, x ∉ U
Uint_nhds : interior U ∈ 𝓝 x_1
f : X →ᵇ ℝ≥0
fx_eq_one : Eq (α := ℝ≥0) ((f : (a : X) → ℝ≥0) x_1 : ℝ≥0) (1 : ℝ≥0)
f_vanishes_outside : ∀ y ∈ (interior U)ᶜ, Eq (α := ℝ≥0) ((f : (a : X) → ℝ≥0) y : ℝ≥0) (0 : ℝ≥0)
x : X
x_notin_U : x ∉ U
h₁ : (↑0 : ℝ≥0∞) ∉ Ioi 0
⊢ (↑((f : (a : X) → ℝ≥0) x) : ℝ≥0∞) ∉ Ioi 0

Tactic:
rw [f_vanishes_outside x
        (compl_subset_compl.mpr (show interior U ⊆ U from interior_subset) x_notin_U)]

Premises used: Iff.mpr, interior_subset, Set.compl_subset_compl
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : CompletelyRegularSpace X
x_1 : X
L : Filter X
h : ¬Tendsto id L (𝓝 x_1)
U : Set X
U_nhds : U ∈ 𝓝 x_1
hU : ∃ᶠ (x : X) in L, x ∉ U
Uint_nhds : interior U ∈ 𝓝 x_1
f : X →ᵇ ℝ≥0
fx_eq_one : Eq (α := ℝ≥0) ((f : (a : X) → ℝ≥0) x_1 : ℝ≥0) (1 : ℝ≥0)
f_vanishes_outside : ∀ y ∈ (interior U)ᶜ, Eq (α := ℝ≥0) ((f : (a : X) → ℝ≥0) y : ℝ≥0) (0 : ℝ≥0)
x : X
x_notin_U : x ∉ U
⊢ (↑0 : ℝ≥0∞) ∉ Ioi 0

Tactic:
simp only [ENNReal.coe_zero, mem_Ioi, lt_self_iff_false, not_false_eq_true]

Premises used: Set.mem_Ioi, ENNReal.coe_zero, lt_self_iff_false, not_false_eq_true
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : CompletelyRegularSpace X
x : X
L : Filter X
mp : Tendsto (β := ProbabilityMeasure X) diracProba L (𝓝 (diracProba x)) → Tendsto id L (𝓝 x)
mpr : Tendsto id L (𝓝 x) → Tendsto (β := ProbabilityMeasure X) diracProba L (𝓝 (diracProba x))
⊢ Tendsto (β := ProbabilityMeasure X) diracProba L (𝓝 (diracProba x)) ↔ Tendsto id L (𝓝 x)

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : CompletelyRegularSpace X
x : X
L : Filter X
mp : ¬Tendsto id L (𝓝 x) → ¬Tendsto (β := ProbabilityMeasure X) diracProba L (𝓝 (diracProba x))
⊢ Tendsto (β := ProbabilityMeasure X) diracProba L (𝓝 (diracProba x)) → Tendsto id L (𝓝 x)

Tactic:
contrapose
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : CompletelyRegularSpace X
x : X
L : Filter X
⊢ ¬Tendsto id L (𝓝 x) → ¬Tendsto (β := ProbabilityMeasure X) diracProba L (𝓝 (diracProba x))

Tactic:
not_tendsto_diracProba_of_not_tendsto L

Premises used: MeasureTheory.not_tendsto_diracProba_of_not_tendsto
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : CompletelyRegularSpace X
x : X
L : Filter X
⊢ ¬Tendsto id L (𝓝 x) → ¬Tendsto (β := ProbabilityMeasure X) diracProba L (𝓝 (diracProba x))

Tactic:
exact not_tendsto_diracProba_of_not_tendsto L

Premises used: MeasureTheory.not_tendsto_diracProba_of_not_tendsto
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : CompletelyRegularSpace X
x : X
L : Filter X
h : Tendsto id L (𝓝 x)
⊢ ContinuousAt (Y := ProbabilityMeasure X) (fun (x : X) ↦ diracProba x) x

Tactic:
have aux := (@continuous_diracProba X _ _ _).continuousAt (x := x)