awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.DiracProba (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
⊢ Continuous[inst_1, ProbabilityMeasure.instTopologicalSpace] fun (x : X) ↦ diracProba x
have rw : ∀ (x : X), ContinuousAt (Y := ProbabilityMeasure X) (fun (x : X) ↦ diracProba x) x
Tactic: rw [continuous_iff_continuousAt]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.DiracProba (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
⊢ ∀ (x : X), ContinuousAt (Y := ProbabilityMeasure X) (fun (x : X) ↦ diracProba x) x
have 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)))
Tactic: apply fun x ↦ ProbabilityMeasure.tendsto_iff_forall_lintegral_tendsto.mpr fun f ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.DiracProba (hypothesis)
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
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)))
have f_mble : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.DiracProba (goal)
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 (i : X) ↦ ∫⁻ (ω : X), (↑((f : (a : X) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(diracProba i) : Measure X)) (𝓝 x)
    (𝓝 (∫⁻ (ω : X), (↑((f : (a : X) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(diracProba x) : Measure X)))
have simp : Tendsto (fun (ω : X) ↦ (↑((f : (a : X) → ℝ≥0) ω) : ℝ≥0∞)) (𝓝 x) (𝓝 (↑((f : (a : X) → ℝ≥0) x) : ℝ≥0∞))
Tactic: simp only [diracProba, ProbabilityMeasure.coe_mk, lintegral_dirac' _ f_mble]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.DiracProba (goal)
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 ∈ 𝓝 x, ∃ᶠ (x : X) in L, x ∉ U
have contrapose! : ∀ (h : ∀ (U : Set X) (_ : U ∈ 𝓝 x), ∀ᶠ (x : X) in L, x ∈ U), Tendsto id L (𝓝 x)
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.DiracProba (goal)
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)
⊢ ¬Tendsto (β := ProbabilityMeasure X) diracProba L (𝓝 (diracProba x))
have obtain : ∀ (U : Set X) (U_nhds : U ∈ 𝓝 x) (hU : ∃ᶠ (x : X) in L, x ∉ U),
  ¬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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.DiracProba (hypothesis)
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
⊢ ¬Tendsto (β := ProbabilityMeasure X) diracProba L (𝓝 (diracProba x))
have Uint_nhds : interior U ∈ 𝓝 x
Tactic: have Uint_nhds : interior U ∈ 𝓝 x := by simpa only [interior_mem_nhds] using U_nhds
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.DiracProba (goal)
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
⊢ ¬Tendsto (β := ProbabilityMeasure X) diracProba L (𝓝 (diracProba x))
have 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))
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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.DiracProba (goal)
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)
⊢ ¬Tendsto (β := ProbabilityMeasure X) diracProba L (𝓝 (diracProba x))
have 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)))
Tactic: rw [ProbabilityMeasure.tendsto_iff_forall_lintegral_tendsto, not_forall]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.DiracProba (goal)
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)
⊢ ∃ (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)))
have 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)))
Tactic: use f
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.DiracProba (goal)
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)
⊢ ¬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)))
have h₁ : ¬Tendsto (fun (i : X) ↦ (↑((f : (a : X) → ℝ≥0) i) : ℝ≥0∞)) L (𝓝 (↑1 : ℝ≥0∞))
Tactic: simp only [diracProba, ProbabilityMeasure.coe_mk, fx_eq_one,
             lintegral_dirac' _ (measurable_coe_nnreal_ennreal_iff.mpr f.continuous.measurable)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.DiracProba (goal)
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)
⊢ ¬Tendsto (fun (i : X) ↦ (↑((f : (a : X) → ℝ≥0) i) : ℝ≥0∞)) L (𝓝 (↑1 : ℝ≥0∞))
have h₁ : ∃ s ∈ 𝓝 (↑1 : ℝ≥0∞), ∃ᶠ (x : X) in L, (↑((f : (a : X) → ℝ≥0) x) : ℝ≥0∞) ∉ s
Tactic: apply not_tendsto_iff_exists_frequently_notMem.mpr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.DiracProba (goal)
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)
⊢ ∃ s ∈ 𝓝 (↑1 : ℝ≥0∞), ∃ᶠ (x : X) in L, (↑((f : (a : X) → ℝ≥0) x) : ℝ≥0∞) ∉ s
have h₁ : ∀ x ∉ U, (↑((f : (a : X) → ℝ≥0) x) : ℝ≥0∞) ∉ Ioi 0
Tactic: refine ⟨Ioi 0, Ioi_mem_nhds (by simp only [ENNReal.coe_one, zero_lt_one]),
          hU.mp (Eventually.of_forall ?_)⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.DiracProba (goal)
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
⊢ (↑((f : (a : X) → ℝ≥0) x) : ℝ≥0∞) ∉ Ioi 0
have h₁ : (↑0 : ℝ≥0∞) ∉ Ioi 0
Tactic: rw [f_vanishes_outside x
        (compl_subset_compl.mpr (show interior U ⊆ U from interior_subset) x_notin_U)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.DiracProba (goal)
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 (β := ProbabilityMeasure X) diracProba L (𝓝 (diracProba x)) ↔ Tendsto id L (𝓝 x)
have mp : Tendsto (β := ProbabilityMeasure X) diracProba L (𝓝 (diracProba x)) → Tendsto id L (𝓝 x)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.DiracProba (goal)
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)
⊢ Tendsto (β := ProbabilityMeasure X) diracProba L (𝓝 (diracProba x)) ↔ Tendsto id L (𝓝 x)
have mpr : Tendsto id L (𝓝 x) → Tendsto (β := ProbabilityMeasure X) diracProba L (𝓝 (diracProba x))
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.DiracProba (goal)
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 (β := ProbabilityMeasure X) diracProba L (𝓝 (diracProba x)) → Tendsto id L (𝓝 x)
have mp : ¬Tendsto id L (𝓝 x) → ¬Tendsto (β := ProbabilityMeasure X) diracProba L (𝓝 (diracProba x))
Tactic: contrapose
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.DiracProba (hypothesis)
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)
⊢ Tendsto (β := ProbabilityMeasure X) diracProba L (𝓝 (diracProba x))
have aux : ContinuousAt (Y := ProbabilityMeasure X) (fun (x : X) ↦ diracProba x) x
Tactic: have aux := (@continuous_diracProba X _ _ _).continuousAt (x := x)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.DiracProba (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : T0Space X
x : X
μ : (↑(range diracProba) : Type u_1)
h : (↑μ : ProbabilityMeasure X) = diracProba x
⊢ diracProbaInverse μ = x
have a : Eq.{u_1 + 1} (α := ProbabilityMeasure X) ((fun (x : X) ↦ (diracProba x : ProbabilityMeasure X)) (diracProbaInverse μ))
  ((fun (x : X) ↦ (diracProba x : ProbabilityMeasure X)) x)
Tactic: apply injective_diracProba (X := X)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.DiracProba (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : T0Space X
x : X
μ : (↑(range diracProba) : Type u_1)
h : (↑μ : ProbabilityMeasure X) = diracProba x
⊢ Eq.{u_1 + 1} (α := ProbabilityMeasure X) ((fun (x : X) ↦ (diracProba x : ProbabilityMeasure X)) (diracProbaInverse μ))
    ((fun (x : X) ↦ (diracProba x : ProbabilityMeasure X)) x)
have a : diracProba (diracProbaInverse μ) = (↑μ : ProbabilityMeasure X)
Tactic: simp only [← h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.DiracProba (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : T0Space X
x : X
⊢ diracProbaInverse
      ((fun (x : X) ↦
          (Subtype.mk (p := fun (x : ProbabilityMeasure X) ↦
              Membership.mem (γ := Set (ProbabilityMeasure X)) (range diracProba) x) (diracProba x) ⋯ :
            { x : ProbabilityMeasure X // Membership.mem (γ := Set (ProbabilityMeasure X)) (range diracProba) x }))
        x) =
    x
have h : Eq (α := ProbabilityMeasure X)
  (↑((fun (x : X) ↦
          (Subtype.mk (p := fun (x : ProbabilityMeasure X) ↦
              Membership.mem (γ := Set (ProbabilityMeasure X)) (range diracProba) x) (diracProba x) sorry :
            { x : ProbabilityMeasure X // Membership.mem (γ := Set (ProbabilityMeasure X)) (range diracProba) x }))
        x) :
    ProbabilityMeasure X)
  (diracProba x)
Tactic: apply diracProbaInverse_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.DiracProba (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : T0Space X
⊢ Eq.{u_1 + 1} (α := (↑(range diracProba) : Type u_1) → ProbabilityMeasure X)
    (diracProba ∘ (⇑(Equiv.symm diracProbaEquiv) : (a : (↑(range diracProba) : Type u_1)) → X))
    fun (μ : (↑(range diracProba) : Type u_1)) ↦ (↑μ : ProbabilityMeasure X)
have h : ∀ (μ : (↑(range diracProba) : Type u_1)),
  (diracProba ∘ (⇑(Equiv.symm diracProbaEquiv) : (a : (↑(range diracProba) : Type u_1)) → X)) μ =
    (↑μ : ProbabilityMeasure X)
Tactic: funext μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.DiracProba (hypothesis)
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : T0Space X
inst_4 : CompletelyRegularSpace X
μ : (↑(range diracProba) : Type u_1)
F : Filter (↑(range diracProba) : Type u_1)
⊢ Tendsto (β := X)
      ((⇑(Equiv.symm diracProbaEquiv) : (a : (↑(range diracProba) : Type u_1)) → X) :
        (a : (↑(range diracProba) : Type u_1)) → X)
      F (𝓝 ((Equiv.symm diracProbaEquiv : (a : (↑(range diracProba) : Type u_1)) → X) μ) : Filter X) ↔
    Tendsto id F (𝓝 μ)
have key : Tendsto (α := X) (β := ProbabilityMeasure X) (diracProba : (x : X) → ProbabilityMeasure X)
    (map (⇑(Equiv.symm diracProbaEquiv) : (a : (↑(range diracProba) : Type u_1)) → X) F : Filter X)
    (𝓝 (diracProba ((Equiv.symm diracProbaEquiv : (a : (↑(range diracProba) : Type u_1)) → X) μ)) :
      Filter (ProbabilityMeasure X)) ↔
  Tendsto (α := X) (β := X) (id : (a : X) → X)
    (map (⇑(Equiv.symm diracProbaEquiv) : (a : (↑(range diracProba) : Type u_1)) → X) F : Filter X)
    (𝓝 ((Equiv.symm diracProbaEquiv : (a : (↑(range diracProba) : Type u_1)) → X) μ) : Filter X)
Tactic: have key :=
    tendsto_diracProba_iff_tendsto (F.map diracProbaEquiv.symm) (x := diracProbaEquiv.symm μ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.DiracProba (hypothesis)
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : T0Space X
inst_4 : CompletelyRegularSpace X
μ : (↑(range diracProba) : Type u_1)
F : Filter (↑(range diracProba) : Type u_1)
key :
  Tendsto (α := X) (β := ProbabilityMeasure X) (diracProba : (x : X) → ProbabilityMeasure X)
      (map (⇑(Equiv.symm diracProbaEquiv) : (a : (↑(range diracProba) : Type u_1)) → X) F : Filter X)
      (𝓝 (diracProba ((Equiv.symm diracProbaEquiv : (a : (↑(range diracProba) : Type u_1)) → X) μ)) :
        Filter (ProbabilityMeasure X)) ↔
    Tendsto (α := X) (β := X) (id : (a : X) → X)
      (map (⇑(Equiv.symm diracProbaEquiv) : (a : (↑(range diracProba) : Type u_1)) → X) F : Filter X)
      (𝓝 ((Equiv.symm diracProbaEquiv : (a : (↑(range diracProba) : Type u_1)) → X) μ) : Filter X)
⊢ Tendsto (β := X)
      ((⇑(Equiv.symm diracProbaEquiv) : (a : (↑(range diracProba) : Type u_1)) → X) :
        (a : (↑(range diracProba) : Type u_1)) → X)
      F (𝓝 ((Equiv.symm diracProbaEquiv : (a : (↑(range diracProba) : Type u_1)) → X) μ) : Filter X) ↔
    Tendsto id F (𝓝 μ)
have key₁ : Tendsto (α := X) (β := ProbabilityMeasure X) (diracProba : (x : X) → ProbabilityMeasure X)
    (map (⇑(Equiv.symm diracProbaEquiv) : (a : (↑(range diracProba) : Type u_1)) → X) F : Filter X)
    (𝓝 (diracProba ((Equiv.symm diracProbaEquiv : (a : (↑(range diracProba) : Type u_1)) → X) μ)) :
      Filter (ProbabilityMeasure X)) ↔
  Tendsto (α := (↑(range diracProba) : Type u_1)) (β := X)
    ((⇑(Equiv.symm diracProbaEquiv) : (a : (↑(range diracProba) : Type u_1)) → X) :
      (a : (↑(range diracProba) : Type u_1)) → X)
    (map (α := X) (⇑diracProbaEquiv : (a : X) → (↑(range diracProba) : Type u_1))
      (map (⇑(Equiv.symm diracProbaEquiv) : (a : (↑(range diracProba) : Type u_1)) → X) F))
    (𝓝 ((Equiv.symm diracProbaEquiv : (a : (↑(range diracProba) : Type u_1)) → X) μ) : Filter X)
Tactic: rw [← (diracProbaEquiv (X := X)).symm_comp_self, ← tendsto_map'_iff] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.DiracProba (hypothesis)
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : T0Space X
inst_4 : CompletelyRegularSpace X
μ : (↑(range diracProba) : Type u_1)
F : Filter (↑(range diracProba) : Type u_1)
key :
  Tendsto (α := X) (β := ProbabilityMeasure X) (diracProba : (x : X) → ProbabilityMeasure X)
      (map (⇑(Equiv.symm diracProbaEquiv) : (a : (↑(range diracProba) : Type u_1)) → X) F : Filter X)
      (𝓝 (diracProba ((Equiv.symm diracProbaEquiv : (a : (↑(range diracProba) : Type u_1)) → X) μ)) :
        Filter (ProbabilityMeasure X)) ↔
    Tendsto (α := (↑(range diracProba) : Type u_1)) (β := X)
      ((⇑(Equiv.symm diracProbaEquiv) : (a : (↑(range diracProba) : Type u_1)) → X) :
        (a : (↑(range diracProba) : Type u_1)) → X)
      (map (α := X) (⇑diracProbaEquiv : (a : X) → (↑(range diracProba) : Type u_1))
        (map (⇑(Equiv.symm diracProbaEquiv) : (a : (↑(range diracProba) : Type u_1)) → X) F))
      (𝓝 ((Equiv.symm diracProbaEquiv : (a : (↑(range diracProba) : Type u_1)) → X) μ) : Filter X)
⊢ Tendsto (β := X)
      ((⇑(Equiv.symm diracProbaEquiv) : (a : (↑(range diracProba) : Type u_1)) → X) :
        (a : (↑(range diracProba) : Type u_1)) → X)
      F (𝓝 ((Equiv.symm diracProbaEquiv : (a : (↑(range diracProba) : Type u_1)) → X) μ) : Filter X) ↔
    Tendsto id F (𝓝 μ)
have key₁ : Tendsto (β := ProbabilityMeasure X)
    (diracProba ∘ (⇑(Equiv.symm diracProbaEquiv) : (a : (↑(range diracProba) : Type u_1)) → X) :
      (↑(range diracProba) : Type u_1) → ProbabilityMeasure X)
    F
    (𝓝 (diracProba ((Equiv.symm diracProbaEquiv : (a : (↑(range diracProba) : Type u_1)) → X) μ)) :
      Filter (ProbabilityMeasure X)) ↔
  Tendsto (β := X)
    ((⇑(Equiv.symm diracProbaEquiv) : (a : (↑(range diracProba) : Type u_1)) → X) :
      (a : (↑(range diracProba) : Type u_1)) → X)
    F (𝓝 ((Equiv.symm diracProbaEquiv : (a : (↑(range diracProba) : Type u_1)) → X) μ) : Filter X)
Tactic: simp only [tendsto_map'_iff, map_map, Equiv.self_comp_symm, map_id] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.DiracProba (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : T0Space X
inst_4 : CompletelyRegularSpace X
μ : (↑(range diracProba) : Type u_1)
F : Filter (↑(range diracProba) : Type u_1)
key :
  Tendsto (β := ProbabilityMeasure X)
      (diracProba ∘ (⇑(Equiv.symm diracProbaEquiv) : (a : (↑(range diracProba) : Type u_1)) → X) :
        (↑(range diracProba) : Type u_1) → ProbabilityMeasure X)
      F
      (𝓝 (diracProba ((Equiv.symm diracProbaEquiv : (a : (↑(range diracProba) : Type u_1)) → X) μ)) :
        Filter (ProbabilityMeasure X)) ↔
    Tendsto (β := X)
      ((⇑(Equiv.symm diracProbaEquiv) : (a : (↑(range diracProba) : Type u_1)) → X) :
        (a : (↑(range diracProba) : Type u_1)) → X)
      F (𝓝 ((Equiv.symm diracProbaEquiv : (a : (↑(range diracProba) : Type u_1)) → X) μ) : Filter X)
⊢ Tendsto (β := X)
      ((⇑(Equiv.symm diracProbaEquiv) : (a : (↑(range diracProba) : Type u_1)) → X) :
        (a : (↑(range diracProba) : Type u_1)) → X)
      F (𝓝 ((Equiv.symm diracProbaEquiv : (a : (↑(range diracProba) : Type u_1)) → X) μ) : Filter X) ↔
    Tendsto id F (𝓝 μ)
have simp : Tendsto (β := ProbabilityMeasure X) (fun (μ : (↑(range diracProba) : Type u_1)) ↦ (↑μ : ProbabilityMeasure X)) F
    (𝓝 (diracProba ((Equiv.symm diracProbaEquiv : (a : (↑(range diracProba) : Type u_1)) → X) μ)) :
      Filter (ProbabilityMeasure X)) ↔
  Tendsto id F (𝓝 μ)
Tactic: simp only [← key, diracProba_comp_diracProbaEquiv_symm_eq_val]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.DiracProba (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : T0Space X
inst_4 : CompletelyRegularSpace X
μ : (↑(range diracProba) : Type u_1)
F : Filter (↑(range diracProba) : Type u_1)
key :
  Tendsto (β := ProbabilityMeasure X)
      (diracProba ∘ (⇑(Equiv.symm diracProbaEquiv) : (a : (↑(range diracProba) : Type u_1)) → X) :
        (↑(range diracProba) : Type u_1) → ProbabilityMeasure X)
      F
      (𝓝 (diracProba ((Equiv.symm diracProbaEquiv : (a : (↑(range diracProba) : Type u_1)) → X) μ)) :
        Filter (ProbabilityMeasure X)) ↔
    Tendsto (β := X)
      ((⇑(Equiv.symm diracProbaEquiv) : (a : (↑(range diracProba) : Type u_1)) → X) :
        (a : (↑(range diracProba) : Type u_1)) → X)
      F (𝓝 ((Equiv.symm diracProbaEquiv : (a : (↑(range diracProba) : Type u_1)) → X) μ) : Filter X)
⊢ Tendsto (β := ProbabilityMeasure X) (fun (μ : (↑(range diracProba) : Type u_1)) ↦ (↑μ : ProbabilityMeasure X)) F
      (𝓝 (diracProba ((Equiv.symm diracProbaEquiv : (a : (↑(range diracProba) : Type u_1)) → X) μ)) :
        Filter (ProbabilityMeasure X)) ↔
    Tendsto id F (𝓝 μ)
have h : diracProba ((Equiv.symm diracProbaEquiv : (a : (↑(range diracProba) : Type u_1)) → X) μ) = (↑μ : ProbabilityMeasure X)
Tactic: convert! tendsto_subtype_rng.symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.DiracProba (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : T0Space X
inst_4 : CompletelyRegularSpace X
⊢ Continuous[instTopologicalSpaceSubtype, inst_1]
    (⇑(Equiv.symm diracProbaEquiv) : (a : (↑(range diracProba) : Type u_1)) → X)
have apply : ∀ (x : (↑(range diracProba) : Type u_1)),
  ContinuousAt (Y := X) (⇑(Equiv.symm diracProbaEquiv) : (a : (↑(range diracProba) : Type u_1)) → X) x
Tactic: apply continuous_iff_continuousAt.mpr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.DiracProba (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : T0Space X
inst_4 : CompletelyRegularSpace X
μ : (↑(range diracProba) : Type u_1)
⊢ ContinuousAt (Y := X) (⇑(Equiv.symm diracProbaEquiv) : (a : (↑(range diracProba) : Type u_1)) → X) μ
have apply : Tendsto (⇑(Equiv.symm diracProbaEquiv) : (a : (↑(range diracProba) : Type u_1)) → X) (𝓝 μ) (𝓝 (diracProbaInverse μ))
Tactic: apply continuousAt_of_tendsto_nhds (y := diracProbaInverse μ)