awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
aux : Tendsto (β := ProbabilityMeasure X) (fun (x : X) ↦ diracProba x) (𝓝 x) (𝓝 (diracProba x))
⊢ Tendsto (β := ProbabilityMeasure X) diracProba L (𝓝 (diracProba x))

Tactic:
aux.comp h

Premises used: MeasureTheory.diracProba, Filter.Tendsto.comp
-- 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)
aux : Tendsto (β := ProbabilityMeasure X) (fun (x : X) ↦ diracProba x) (𝓝 x) (𝓝 (diracProba x))
⊢ Tendsto (β := ProbabilityMeasure X) diracProba L (𝓝 (diracProba x))

Tactic:
exact aux.comp h

Premises used: Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_2
inst : MeasurableSpace X
μ : (↑(range diracProba) : Type u_2)
⊢ diracProba (diracProbaInverse μ) = (↑μ : ProbabilityMeasure X)

Tactic:
(mem_range.mp μ.prop).choose_spec

Premises used: Exists.choose_spec, Set.mem_range, MeasureTheory.diracProbaInverse, Subtype.prop, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
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
a :
  Eq.{u_1 + 1} (α := ProbabilityMeasure X) ((fun (x : X) ↦ (diracProba x : ProbabilityMeasure X)) (diracProbaInverse μ))
    ((fun (x : X) ↦ (diracProba x : ProbabilityMeasure X)) x)
⊢ diracProbaInverse μ = x

Tactic:
apply injective_diracProba (X := X)

Premises used: MeasureTheory.injective_diracProba
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
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
a : diracProba (diracProbaInverse μ) = (↑μ : ProbabilityMeasure X)
⊢ Eq.{u_1 + 1} (α := ProbabilityMeasure X) ((fun (x : X) ↦ (diracProba x : ProbabilityMeasure X)) (diracProbaInverse μ))
    ((fun (x : X) ↦ (diracProba x : ProbabilityMeasure X)) x)

Tactic:
simp only [← h]
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
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
⊢ diracProba (diracProbaInverse μ) = (↑μ : ProbabilityMeasure X)

Tactic:
(mem_range.mp μ.prop).choose_spec

Premises used: Exists.choose_spec, Set.mem_range, MeasureTheory.diracProbaInverse, Subtype.prop, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
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
⊢ diracProba (diracProbaInverse μ) = (↑μ : ProbabilityMeasure X)

Tactic:
exact (mem_range.mp μ.prop).choose_spec

Premises used: Exists.choose_spec, Set.mem_range, Subtype.prop, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : T0Space X
x : X
⊢ Membership.mem (γ := Set (ProbabilityMeasure X)) (range diracProba) (diracProba x)

Tactic:
mem_range_self x

Premises used: Set.mem_range_self
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : T0Space X
x : X
⊢ Membership.mem (γ := Set (ProbabilityMeasure X)) (range diracProba) (diracProba x)

Tactic:
exact mem_range_self x

Premises used: Set.mem_range_self
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : T0Space X
x : X
h :
  Eq (α := ProbabilityMeasure X)
    (↑((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) :
      ProbabilityMeasure X)
    (diracProba 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

Tactic:
apply diracProbaInverse_eq

Premises used: MeasureTheory.diracProbaInverse_eq
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : T0Space X
x : X
⊢ Eq (α := ProbabilityMeasure X)
    (↑((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) :
      ProbabilityMeasure X)
    (diracProba x)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : T0Space X
μ : (↑(range diracProba) : Type u_1)
⊢ (↑((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 }))
          (diracProbaInverse μ)) :
      ProbabilityMeasure X) =
    (↑μ : ProbabilityMeasure X)

Tactic:
simp only [diracProba_diracProbaInverse]

Premises used: MeasureTheory.diracProba_diracProbaInverse
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : T0Space X
h :
  ∀ (μ : (↑(range diracProba) : Type u_1)),
    (diracProba ∘ (⇑(Equiv.symm diracProbaEquiv) : (a : (↑(range diracProba) : Type u_1)) → X)) μ =
      (↑μ : ProbabilityMeasure 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)

Tactic:
funext μ
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : T0Space X
μ : (↑(range diracProba) : Type u_1)
⊢ (diracProba ∘ (⇑(Equiv.symm diracProbaEquiv) : (a : (↑(range diracProba) : Type u_1)) → X)) μ =
    (↑μ : ProbabilityMeasure X)

Tactic:
simp [diracProbaEquiv]

Premises used: MeasureTheory.diracProbaEquiv
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
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) (β := 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 μ)
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
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) (β := 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

Premises used: Equiv.symm_comp_self, Filter.tendsto_map'_iff, MeasureTheory.diracProbaEquiv
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
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 (β := 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

Premises used: Filter.tendsto_map'_iff, Filter.map_map, Equiv.self_comp_symm, Filter.map_id
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
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)
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 (𝓝 μ)
⊢ 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 (𝓝 μ)

Tactic:
simp only [← key, diracProba_comp_diracProbaEquiv_symm_eq_val]

Premises used: MeasureTheory.diracProba_comp_diracProbaEquiv_symm_eq_val
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
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 (fun (x : (↑(range diracProba) : Type u_1)) ↦ (↑x : ProbabilityMeasure X)) F (𝓝 (↑μ : ProbabilityMeasure X)) ↔
    Tendsto (fun (μ : (↑(range diracProba) : Type u_1)) ↦ μ) F (𝓝 μ)

Tactic:
tendsto_subtype_rng.symm

Premises used: tendsto_subtype_rng, Iff.symm
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
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)
h :
  diracProba ((Equiv.symm diracProbaEquiv : (a : (↑(range diracProba) : Type u_1)) → X) μ) = (↑μ : ProbabilityMeasure 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 (𝓝 μ)

Tactic:
convert! tendsto_subtype_rng.symm

Premises used: tendsto_subtype_rng, Iff.symm
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
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)
⊢ diracProba ((Equiv.symm diracProbaEquiv : (a : (↑(range diracProba) : Type u_1)) → X) μ) = (↑μ : ProbabilityMeasure X)

Tactic:
apply_rangeSplitting (fun x ↦ diracProba x) μ

Premises used: MeasureTheory.diracProba, MeasureTheory.diracProbaInverse, Classical.choose, Set.rangeSplitting, Set.apply_rangeSplitting
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
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)
⊢ diracProba ((Equiv.symm diracProbaEquiv : (a : (↑(range diracProba) : Type u_1)) → X) μ) = (↑μ : ProbabilityMeasure X)

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

Premises used: MeasureTheory.diracProba, Set.apply_rangeSplitting
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : T0Space X
⊢ Continuous[inst_1, instTopologicalSpaceSubtype] (⇑diracProbaEquiv : (a : X) → (↑(range diracProba) : Type u_1))

Tactic:
Continuous.subtype_mk continuous_diracProba mem_range_self

Premises used: Set.mem_range_self, Continuous.subtype_mk, MeasureTheory.continuous_diracProba
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : T0Space X
inst_4 : CompletelyRegularSpace X
apply :
  ∀ (x : (↑(range diracProba) : Type u_1)),
    ContinuousAt (Y := X) (⇑(Equiv.symm diracProbaEquiv) : (a : (↑(range diracProba) : Type u_1)) → X) x
⊢ Continuous[instTopologicalSpaceSubtype, inst_1]
    (⇑(Equiv.symm diracProbaEquiv) : (a : (↑(range diracProba) : Type u_1)) → X)

Tactic:
apply continuous_iff_continuousAt.mpr

Premises used: Iff.mpr, continuous_iff_continuousAt
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
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)
apply :
  Tendsto (⇑(Equiv.symm diracProbaEquiv) : (a : (↑(range diracProba) : Type u_1)) → X) (𝓝 μ) (𝓝 (diracProbaInverse μ))
⊢ ContinuousAt (Y := X) (⇑(Equiv.symm diracProbaEquiv) : (a : (↑(range diracProba) : Type u_1)) → X) μ

Tactic:
apply continuousAt_of_tendsto_nhds (y := diracProbaInverse μ)

Premises used: continuousAt_of_tendsto_nhds
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
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)
⊢ Tendsto (⇑(Equiv.symm diracProbaEquiv) : (a : (↑(range diracProba) : Type u_1)) → X) (𝓝 μ) (𝓝 (diracProbaInverse μ))

Tactic:
(tendsto_diracProbaEquivSymm_iff_tendsto _).mpr fun _ mem_nhds ↦ mem_nhds

Premises used: Iff.mpr, MeasureTheory.diracProbaInverse, MeasureTheory.tendsto_diracProbaEquivSymm_iff_tendsto, Classical.choose
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
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)
⊢ Tendsto (⇑(Equiv.symm diracProbaEquiv) : (a : (↑(range diracProba) : Type u_1)) → X) (𝓝 μ) (𝓝 (diracProbaInverse μ))

Tactic:
exact (tendsto_diracProbaEquivSymm_iff_tendsto _).mpr fun _ mem_nhds ↦ mem_nhds

Premises used: Iff.mpr, MeasureTheory.tendsto_diracProbaEquivSymm_iff_tendsto
-- Module: Mathlib.MeasureTheory.Measure.DiracProba
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
inst_3 : T0Space X
inst_4 : CompletelyRegularSpace X
⊢ IsEmbedding (Y := ProbabilityMeasure X) fun (x : X) ↦ diracProba x

Tactic:
IsEmbedding.subtypeVal.comp diracProbaHomeomorph.isEmbedding

Premises used: Homeomorph.isEmbedding, MeasureTheory.diracProba, Topology.IsEmbedding.comp, MeasureTheory.diracProbaHomeomorph, Topology.IsEmbedding.subtypeVal
-- Module: Mathlib.MeasureTheory.Measure.Doubling
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
⊢ ∃ (C : ℝ≥0),
    ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
      ∀ (x : α),
        (μ : (a : Set α) → ℝ≥0∞) (closedBall x (2 * ε)) ≤
          HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)

Tactic:
exists_measure_closedBall_le_mul''

Premises used: IsUnifLocDoublingMeasure.exists_measure_closedBall_le_mul''
-- Module: Mathlib.MeasureTheory.Measure.Doubling
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
⊢ ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∀ (x : α),
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x (2 * ε)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑(doublingConstant μ) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)

Tactic:
Classical.choose_spec <| exists_measure_closedBall_le_mul μ

Premises used: IsUnifLocDoublingMeasure.exists_measure_closedBall_le_mul, Classical.choose_spec, IsUnifLocDoublingMeasure.doublingConstant
-- Module: Mathlib.MeasureTheory.Measure.Doubling
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
this :
  ∀ (n : ℕ),
    ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
      ∀ (x : α),
        (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) 2 n * ε)) ≤
          HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ n) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
rcases :
  ∀ (n : ℕ) (hn : K < HPow.hPow (α := ℝ) 2 n),
    ∃ (C : ℝ≥0),
      ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
        ∀ (x : α),
          ∀ t ≤ K,
            (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
              HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
⊢ ∃ (C : ℝ≥0),
    ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
      ∀ (x : α),
        ∀ t ≤ K,
          (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
            HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)

Tactic:
rcases pow_unbounded_of_one_lt K one_lt_two with ⟨n, hn⟩

Premises used: one_lt_two, pow_unbounded_of_one_lt