-- Mathlib/MeasureTheory/Measure/DiracProba.lean
lemma not_tendsto_diracProba_of_not_tendsto [CompletelyRegularSpace X] {x : X} (L : Filter X)
    (h : ¬ Tendsto id L (𝓝 x)) :
    ¬ Tendsto diracProba L (𝓝 (diracProba x))

Proof state:
case h
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : CompletelyRegularSpace X
x✝ : X
L : Filter X
h : ¬Tendsto id L (𝓝 x✝)
U : Set X
U_nhd : U ∈ 𝓝 x✝
hU : ∃ᶠ (x : X) in L, x ∉ U
Uint_nhd : interior U ∈ 𝓝 x✝
f : X →ᵇ ℝ≥0
fx_eq_one : f x✝ = 1
f_vanishes_outside : ∀ y ∈ (interior U)ᶜ, f y = 0
x : X
x_notin_U : x ∉ U
⊢ ↑(f x) ∉ Ioi 0

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

Result:
case h
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : CompletelyRegularSpace X
x✝ : X
L : Filter X
h : ¬Tendsto id L (𝓝 x✝)
U : Set X
U_nhd : U ∈ 𝓝 x✝
hU : ∃ᶠ (x : X) in L, x ∉ U
Uint_nhd : interior U ∈ 𝓝 x✝
f : X →ᵇ ℝ≥0
fx_eq_one : f x✝ = 1
f_vanishes_outside : ∀ y ∈ (interior U)ᶜ, f y = 0
x : X
x_notin_U : x ∉ U
⊢ ↑0 ∉ Ioi 0

Proof state:
case h
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : CompletelyRegularSpace X
x : X
L : Filter X
h : ¬Tendsto id L (𝓝 x)
U : Set X
U_nhd : U ∈ 𝓝 x
hU : ∃ᶠ (x : X) in L, x ∉ U
Uint_nhd : interior U ∈ 𝓝 x
f : X →ᵇ ℝ≥0
fx_eq_one : f x = 1
f_vanishes_outside : ∀ y ∈ (interior U)ᶜ, f y = 0
⊢ ∀ x ∉ U, ↑(f x) ∉ Ioi 0

Tactic:
intro x x_notin_U

Result:
case h
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : CompletelyRegularSpace X
x✝ : X
L : Filter X
h : ¬Tendsto id L (𝓝 x✝)
U : Set X
U_nhd : U ∈ 𝓝 x✝
hU : ∃ᶠ (x : X) in L, x ∉ U
Uint_nhd : interior U ∈ 𝓝 x✝
f : X →ᵇ ℝ≥0
fx_eq_one : f x✝ = 1
f_vanishes_outside : ∀ y ∈ (interior U)ᶜ, f y = 0
x : X
x_notin_U : x ∉ U
⊢ ↑(f x) ∉ Ioi 0

Proof state:
case intro.intro.intro.intro
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : CompletelyRegularSpace X
x : X
L : Filter X
h : ¬Tendsto id L (𝓝 x)
U : Set X
U_nhd : U ∈ 𝓝 x
hU : ∃ᶠ (x : X) in L, x ∉ U
Uint_nhd : interior U ∈ 𝓝 x
f : X →ᵇ ℝ≥0
fx_eq_one : f x = 1
f_vanishes_outside : ∀ y ∈ (interior U)ᶜ, f y = 0
⊢ ∃ x_1, ¬Tendsto (fun i => ∫⁻ (ω : X), ↑(x_1 ω) ∂↑(diracProba i)) L (𝓝 (∫⁻ (ω : X), ↑(x_1 ω) ∂↑(diracProba x)))

Tactic:
use f

Result:
case h
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : CompletelyRegularSpace X
x : X
L : Filter X
h : ¬Tendsto id L (𝓝 x)
U : Set X
U_nhd : U ∈ 𝓝 x
hU : ∃ᶠ (x : X) in L, x ∉ U
Uint_nhd : interior U ∈ 𝓝 x
f : X →ᵇ ℝ≥0
fx_eq_one : f x = 1
f_vanishes_outside : ∀ y ∈ (interior U)ᶜ, f y = 0
⊢ ¬Tendsto (fun i => ∫⁻ (ω : X), ↑(f ω) ∂↑(diracProba i)) L (𝓝 (∫⁻ (ω : X), ↑(f ω) ∂↑(diracProba x)))

Proof state:
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : CompletelyRegularSpace X
x : X
L : Filter X
h : ¬Tendsto id L (𝓝 x)
U : Set X
U_nhd : U ∈ 𝓝 x
hU : ∃ᶠ (x : X) in L, x ∉ U
Uint_nhd : interior U ∈ 𝓝 x
⊢ ?m.19610 ∉ (interior ?m.19374)ᶜ

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

Result:
no goals

Proof state:
case h
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : CompletelyRegularSpace X
x : X
L : Filter X
h : ¬Tendsto id L (𝓝 x)
U : Set X
U_nhd : U ∈ 𝓝 x
hU : ∃ᶠ (x : X) in L, x ∉ U
Uint_nhd : interior U ∈ 𝓝 x
f : X →ᵇ ℝ≥0
fx_eq_one : f x = 1
f_vanishes_outside : ∀ y ∈ (interior U)ᶜ, f y = 0
⊢ ¬Tendsto (fun i => ↑(f i)) L (𝓝 ↑1)

Tactic:
apply not_tendsto_iff_exists_frequently_nmem.mpr

Result:
case h
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : CompletelyRegularSpace X
x : X
L : Filter X
h : ¬Tendsto id L (𝓝 x)
U : Set X
U_nhd : U ∈ 𝓝 x
hU : ∃ᶠ (x : X) in L, x ∉ U
Uint_nhd : interior U ∈ 𝓝 x
f : X →ᵇ ℝ≥0
fx_eq_one : f x = 1
f_vanishes_outside : ∀ y ∈ (interior U)ᶜ, f y = 0
⊢ ∃ s ∈ 𝓝 ↑1, ∃ᶠ (x : X) in L, ↑(f x) ∉ s

Proof state:
case intro.intro
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : CompletelyRegularSpace X
x : X
L : Filter X
h : ¬Tendsto id L (𝓝 x)
U : Set X
U_nhd : U ∈ 𝓝 x
hU : ∃ᶠ (x : X) in L, x ∉ U
⊢ ¬Tendsto diracProba L (𝓝 (diracProba x))

Tactic:
have Uint_nhd : interior U ∈ 𝓝 x := by simpa only [interior_mem_nhds] using U_nhd

Result:
case intro.intro
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : CompletelyRegularSpace X
x : X
L : Filter X
h : ¬Tendsto id L (𝓝 x)
U : Set X
U_nhd : U ∈ 𝓝 x
hU : ∃ᶠ (x : X) in L, x ∉ U
Uint_nhd : interior U ∈ 𝓝 x
⊢ ¬Tendsto diracProba L (𝓝 (diracProba x))

Proof state:
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : CompletelyRegularSpace X
x : X
L : Filter X
h : ¬Tendsto id L (𝓝 x)
⊢ ¬Tendsto diracProba L (𝓝 (diracProba x))

Tactic:
obtain ⟨U, U_nhd, hU⟩ : ∃ U, U ∈ 𝓝 x ∧ ∃ᶠ x in L, x ∉ U := by
  by_contra! con
  apply h
  intro U U_nhd
  simpa only [not_frequently, not_not] using con U U_nhd

Result:
case intro.intro
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : CompletelyRegularSpace X
x : X
L : Filter X
h : ¬Tendsto id L (𝓝 x)
U : Set X
U_nhd : U ∈ 𝓝 x
hU : ∃ᶠ (x : X) in L, x ∉ U
⊢ ¬Tendsto diracProba L (𝓝 (diracProba x))

Proof state:
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : CompletelyRegularSpace X
x : X
L : Filter X
h : ¬Tendsto id L (𝓝 x)
⊢ ∃ U ∈ 𝓝 x, ∃ᶠ (x : X) in L, x ∉ U

Tactic:
by_contra! con

Result:
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : CompletelyRegularSpace X
x : X
L : Filter X
h : ¬Tendsto id L (𝓝 x)
con : ∀ U ∈ 𝓝 x, ¬∃ᶠ (x : X) in L, x ∉ U
⊢ False

Proof state:
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : CompletelyRegularSpace X
x : X
L : Filter X
h : ¬Tendsto id L (𝓝 x)
con : ∀ U ∈ 𝓝 x, ¬∃ᶠ (x : X) in L, x ∉ U
⊢ False

Tactic:
apply h

Result:
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : CompletelyRegularSpace X
x : X
L : Filter X
h : ¬Tendsto id L (𝓝 x)
con : ∀ U ∈ 𝓝 x, ¬∃ᶠ (x : X) in L, x ∉ U
⊢ Tendsto id L (𝓝 x)

Proof state:
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : CompletelyRegularSpace X
x : X
L : Filter X
h : ¬Tendsto id L (𝓝 x)
con : ∀ U ∈ 𝓝 x, ¬∃ᶠ (x : X) in L, x ∉ U
⊢ Tendsto id L (𝓝 x)

Tactic:
intro U U_nhd

Result:
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : CompletelyRegularSpace X
x : X
L : Filter X
h : ¬Tendsto id L (𝓝 x)
con : ∀ U ∈ 𝓝 x, ¬∃ᶠ (x : X) in L, x ∉ U
U : Set X
U_nhd : U ∈ 𝓝 x
⊢ U ∈ map id L