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

Proof state:
case mpr
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)
aux : Tendsto (fun x => diracProba x) (𝓝 x) (𝓝 (diracProba x))
⊢ Tendsto diracProba L (𝓝 (diracProba x))

Tactic:
exact aux.comp h

Result:
no goals

Proof state:
case mpr
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:
have aux := (@continuous_diracProba X _ _ _).continuousAt (x := x)

Result:
case mpr
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)
aux : ContinuousAt (fun x => diracProba x) x
⊢ Tendsto diracProba L (𝓝 (diracProba x))

Proof state:
case mpr
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)
aux : ContinuousAt (fun x => diracProba x) x
⊢ Tendsto diracProba L (𝓝 (diracProba x))

Tactic:
simp only [ContinuousAt] at aux

Result:
case mpr
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)
aux : Tendsto (fun x => diracProba x) (𝓝 x) (𝓝 (diracProba 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
⊢ Tendsto diracProba L (𝓝 (diracProba x)) ↔ Tendsto id L (𝓝 x)

Tactic:
constructor

Result:
case mp
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : CompletelyRegularSpace X
x : X
L : Filter X
⊢ Tendsto diracProba L (𝓝 (diracProba x)) → Tendsto id L (𝓝 x)

case mpr
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : CompletelyRegularSpace X
x : X
L : Filter X
⊢ Tendsto id L (𝓝 x) → Tendsto diracProba L (𝓝 (diracProba x))

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

Tactic:
contrapose

Result:
case mp
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : CompletelyRegularSpace X
x : X
L : Filter X
⊢ ¬Tendsto id L (𝓝 x) → ¬Tendsto diracProba L (𝓝 (diracProba x))

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

Tactic:
exact not_tendsto_diracProba_of_not_tendsto L

Result:
no goals

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

Tactic:
intro h

Result:
case mpr
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))