-- Mathlib/MeasureTheory/Measure/DiracProba.lean
lemma tendsto_diracProbaEquivSymm_iff_tendsto [T0Space X] [CompletelyRegularSpace X]
    {μ : range (diracProba (X := X))} (F : Filter (range (diracProba (X := X)))) :
    Tendsto diracProbaEquiv.symm F (𝓝 (diracProbaEquiv.symm μ)) ↔ Tendsto id F (𝓝 μ)

Proof state:
X : Type u_1
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : OpensMeasurableSpace X
inst✝¹ : T0Space X
inst✝ : CompletelyRegularSpace X
μ : ↑(range diracProba)
F : Filter ↑(range diracProba)
key :
  Tendsto (diracProba ∘ ⇑diracProbaEquiv.symm) F (𝓝 (diracProba (diracProbaEquiv.symm μ))) ↔
    Tendsto (⇑diracProbaEquiv.symm) F (𝓝 (diracProbaEquiv.symm μ))
⊢ Tendsto (fun μ => ↑μ) F (𝓝 (diracProba (diracProbaEquiv.symm μ))) ↔ Tendsto id F (𝓝 μ)

Tactic:
convert tendsto_subtype_rng.symm

Result:
case h.e'_1.h.e'_5.h.e'_3
X : Type u_1
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : OpensMeasurableSpace X
inst✝¹ : T0Space X
inst✝ : CompletelyRegularSpace X
μ : ↑(range diracProba)
F : Filter ↑(range diracProba)
key :
  Tendsto (diracProba ∘ ⇑diracProbaEquiv.symm) F (𝓝 (diracProba (diracProbaEquiv.symm μ))) ↔
    Tendsto (⇑diracProbaEquiv.symm) F (𝓝 (diracProbaEquiv.symm μ))
⊢ diracProba (diracProbaEquiv.symm μ) = ↑μ

Proof state:
X : Type u_1
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : OpensMeasurableSpace X
inst✝¹ : T0Space X
inst✝ : CompletelyRegularSpace X
μ : ↑(range diracProba)
F : Filter ↑(range diracProba)
⊢ Tendsto (⇑diracProbaEquiv.symm) F (𝓝 (diracProbaEquiv.symm μ)) ↔ Tendsto id F (𝓝 μ)

Tactic:
have key :=
  tendsto_diracProba_iff_tendsto (F.map diracProbaEquiv.symm) (x := diracProbaEquiv.symm μ)

Result:
X : Type u_1
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : OpensMeasurableSpace X
inst✝¹ : T0Space X
inst✝ : CompletelyRegularSpace X
μ : ↑(range diracProba)
F : Filter ↑(range diracProba)
key :
  Tendsto diracProba (map (⇑diracProbaEquiv.symm) F) (𝓝 (diracProba (diracProbaEquiv.symm μ))) ↔
    Tendsto id (map (⇑diracProbaEquiv.symm) F) (𝓝 (diracProbaEquiv.symm μ))
⊢ Tendsto (⇑diracProbaEquiv.symm) F (𝓝 (diracProbaEquiv.symm μ)) ↔ Tendsto id F (𝓝 μ)

Proof state:
X : Type u_1
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : OpensMeasurableSpace X
inst✝¹ : T0Space X
inst✝ : CompletelyRegularSpace X
μ : ↑(range diracProba)
F : Filter ↑(range diracProba)
key :
  Tendsto diracProba (map (⇑diracProbaEquiv.symm) F) (𝓝 (diracProba (diracProbaEquiv.symm μ))) ↔
    Tendsto id (map (⇑diracProbaEquiv.symm) F) (𝓝 (diracProbaEquiv.symm μ))
⊢ Tendsto (⇑diracProbaEquiv.symm) F (𝓝 (diracProbaEquiv.symm μ)) ↔ Tendsto id F (𝓝 μ)

Tactic:
rw [← (diracProbaEquiv (X := X)).symm_comp_self, ← tendsto_map'_iff] at key

Result:
X : Type u_1
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : OpensMeasurableSpace X
inst✝¹ : T0Space X
inst✝ : CompletelyRegularSpace X
μ : ↑(range diracProba)
F : Filter ↑(range diracProba)
key :
  Tendsto diracProba (map (⇑diracProbaEquiv.symm) F) (𝓝 (diracProba (diracProbaEquiv.symm μ))) ↔
    Tendsto (⇑diracProbaEquiv.symm) (map (⇑diracProbaEquiv) (map (⇑diracProbaEquiv.symm) F))
      (𝓝 (diracProbaEquiv.symm μ))
⊢ Tendsto (⇑diracProbaEquiv.symm) F (𝓝 (diracProbaEquiv.symm μ)) ↔ Tendsto id F (𝓝 μ)

Proof state:
X : Type u_1
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : OpensMeasurableSpace X
inst✝¹ : T0Space X
inst✝ : CompletelyRegularSpace X
μ : ↑(range diracProba)
F : Filter ↑(range diracProba)
key :
  Tendsto diracProba (map (⇑diracProbaEquiv.symm) F) (𝓝 (diracProba (diracProbaEquiv.symm μ))) ↔
    Tendsto (⇑diracProbaEquiv.symm) (map (⇑diracProbaEquiv) (map (⇑diracProbaEquiv.symm) F))
      (𝓝 (diracProbaEquiv.symm μ))
⊢ Tendsto (⇑diracProbaEquiv.symm) F (𝓝 (diracProbaEquiv.symm μ)) ↔ Tendsto id F (𝓝 μ)

Tactic:
simp only [tendsto_map'_iff, map_map, Equiv.self_comp_symm, map_id] at key

Result:
X : Type u_1
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : OpensMeasurableSpace X
inst✝¹ : T0Space X
inst✝ : CompletelyRegularSpace X
μ : ↑(range diracProba)
F : Filter ↑(range diracProba)
key :
  Tendsto (diracProba ∘ ⇑diracProbaEquiv.symm) F (𝓝 (diracProba (diracProbaEquiv.symm μ))) ↔
    Tendsto (⇑diracProbaEquiv.symm) F (𝓝 (diracProbaEquiv.symm μ))
⊢ Tendsto (⇑diracProbaEquiv.symm) F (𝓝 (diracProbaEquiv.symm μ)) ↔ Tendsto id F (𝓝 μ)

Proof state:
X : Type u_1
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : OpensMeasurableSpace X
inst✝¹ : T0Space X
inst✝ : CompletelyRegularSpace X
μ : ↑(range diracProba)
F : Filter ↑(range diracProba)
key :
  Tendsto (diracProba ∘ ⇑diracProbaEquiv.symm) F (𝓝 (diracProba (diracProbaEquiv.symm μ))) ↔
    Tendsto (⇑diracProbaEquiv.symm) F (𝓝 (diracProbaEquiv.symm μ))
⊢ Tendsto (⇑diracProbaEquiv.symm) F (𝓝 (diracProbaEquiv.symm μ)) ↔ Tendsto id F (𝓝 μ)

Tactic:
simp only [← key, diracProba_comp_diracProbaEquiv_symm_eq_val]

Result:
X : Type u_1
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : OpensMeasurableSpace X
inst✝¹ : T0Space X
inst✝ : CompletelyRegularSpace X
μ : ↑(range diracProba)
F : Filter ↑(range diracProba)
key :
  Tendsto (diracProba ∘ ⇑diracProbaEquiv.symm) F (𝓝 (diracProba (diracProbaEquiv.symm μ))) ↔
    Tendsto (⇑diracProbaEquiv.symm) F (𝓝 (diracProbaEquiv.symm μ))
⊢ Tendsto (fun μ => ↑μ) F (𝓝 (diracProba (diracProbaEquiv.symm μ))) ↔ Tendsto id F (𝓝 μ)

Proof state:
case h.e'_1.h.e'_5.h.e'_3
X : Type u_1
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : OpensMeasurableSpace X
inst✝¹ : T0Space X
inst✝ : CompletelyRegularSpace X
μ : ↑(range diracProba)
F : Filter ↑(range diracProba)
key :
  Tendsto (diracProba ∘ ⇑diracProbaEquiv.symm) F (𝓝 (diracProba (diracProbaEquiv.symm μ))) ↔
    Tendsto (⇑diracProbaEquiv.symm) F (𝓝 (diracProbaEquiv.symm μ))
⊢ diracProba (diracProbaEquiv.symm μ) = ↑μ

Tactic:
exact apply_rangeSplitting (fun x ↦ diracProba x) μ

Result:
no goals