awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto (ProbabilityMeasure.toFiniteMeasure ∘ fun (i : γ) ↦ (μs i).normalize) F (𝓝 μ.normalize.toFiniteMeasure)
mass_lim : Tendsto (fun (i : γ) ↦ (μs i).mass) F (𝓝 μ.mass)
f : Ω →ᵇ ℝ≥0
h_mass : ¬μ.mass = 0
neg :
  ∀
    (μs_lim :
      ∀ (f : Ω →ᵇ ℝ≥0),
        Tendsto
          (fun (i : γ) ↦ testAgainstNN ((ProbabilityMeasure.toFiniteMeasure ∘ fun (i : γ) ↦ (μs i).normalize) i) f) F
          (𝓝 (μ.normalize.toFiniteMeasure.testAgainstNN f)))
    (mass_lim : Tendsto (fun (i : γ) ↦ (μs i).mass) F (𝓝 μ.mass)) (f : Ω →ᵇ ℝ≥0) (h_mass : ¬μ.mass = 0),
    Tendsto (fun (i : γ) ↦ (μs i).mass * (μs i).normalize.toFiniteMeasure.testAgainstNN f) F
      (𝓝 (μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f))
⊢ Tendsto (fun (i : γ) ↦ (μs i).mass * (μs i).normalize.toFiniteMeasure.testAgainstNN f) F
    (𝓝 (μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f))

Tactic:
rw [tendsto_iff_forall_testAgainstNN_tendsto] at μs_lim

Premises used: MeasureTheory.FiniteMeasure.tendsto_iff_forall_testAgainstNN_tendsto
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim :
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : γ) ↦ testAgainstNN ((ProbabilityMeasure.toFiniteMeasure ∘ fun (i : γ) ↦ (μs i).normalize) i) f) F
      (𝓝 (μ.normalize.toFiniteMeasure.testAgainstNN f))
mass_lim : Tendsto (fun (i : γ) ↦ (μs i).mass) F (𝓝 μ.mass)
f : Ω →ᵇ ℝ≥0
h_mass : ¬μ.mass = 0
⊢ Tendsto (fun (i : γ) ↦ ((μs i).mass, (μs i).normalize.toFiniteMeasure.testAgainstNN f)) F
    (𝓝 (μ.mass, μ.normalize.toFiniteMeasure.testAgainstNN f))

Tactic:
have lim_pair :
    Tendsto (fun i ↦ (⟨(μs i).mass, (μs i).normalize.toFiniteMeasure.testAgainstNN f⟩ : ℝ≥0 × ℝ≥0))
      F (𝓝 ⟨μ.mass, μ.normalize.toFiniteMeasure.testAgainstNN f⟩) :=
    (Prod.tendsto_iff _ _).mpr ⟨mass_lim, μs_lim f⟩
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim :
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : γ) ↦ testAgainstNN ((ProbabilityMeasure.toFiniteMeasure ∘ fun (i : γ) ↦ (μs i).normalize) i) f) F
      (𝓝 (μ.normalize.toFiniteMeasure.testAgainstNN f))
mass_lim : Tendsto (fun (i : γ) ↦ (μs i).mass) F (𝓝 μ.mass)
f : Ω →ᵇ ℝ≥0
h_mass : ¬μ.mass = 0
lim_pair :
  Tendsto (fun (i : γ) ↦ ((μs i).mass, (μs i).normalize.toFiniteMeasure.testAgainstNN f)) F
    (𝓝 (μ.mass, μ.normalize.toFiniteMeasure.testAgainstNN f))
⊢ Tendsto (fun (i : γ) ↦ (μs i).mass * (μs i).normalize.toFiniteMeasure.testAgainstNN f) F
    (𝓝 (μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f))

Tactic:
exact tendsto_mul.comp lim_pair

Premises used: tendsto_mul, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto μs F (𝓝 μ)
nonzero : μ ≠ 0
f : Ω →ᵇ ℝ≥0
⊢ Tendsto (fun (i : γ) ↦ (μs i).mass) F (𝓝 μ.mass)

Tactic:
have lim_mass := μs_lim.mass
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto μs F (𝓝 μ)
nonzero : μ ≠ 0
f : Ω →ᵇ ℝ≥0
lim_mass : Tendsto (fun (i : γ) ↦ (μs i).mass) F (𝓝 μ.mass)
⊢ {0}ᶜ ∈ 𝓝 μ.mass

Tactic:
have aux : {(0 : ℝ≥0)}ᶜ ∈ 𝓝 μ.mass :=
    isOpen_compl_singleton.mem_nhds (μ.mass_nonzero_iff.mpr nonzero)
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto μs F (𝓝 μ)
nonzero : μ ≠ 0
f : Ω →ᵇ ℝ≥0
lim_mass : Tendsto (fun (i : γ) ↦ (μs i).mass) F (𝓝 μ.mass)
aux : {0}ᶜ ∈ 𝓝 μ.mass
simp_rw : ∀ᶠ (i : γ) in F, (μs i).mass ≠ 0
⊢ ∀ᶠ (i : γ) in F, μs i ≠ 0

Tactic:
simp_rw [← mass_nonzero_iff]

Premises used: MeasureTheory.FiniteMeasure.mass_nonzero_iff
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto μs F (𝓝 μ)
nonzero : μ ≠ 0
f : Ω →ᵇ ℝ≥0
lim_mass : Tendsto (fun (i : γ) ↦ (μs i).mass) F (𝓝 μ.mass)
aux : {0}ᶜ ∈ 𝓝 μ.mass
⊢ ∀ᶠ (i : γ) in F, (μs i).mass ≠ 0

Tactic:
lim_mass aux

Premises used: Set.Mem, Filter.Eventually, setOf, Set.preimage, Set.singleton, Not
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto μs F (𝓝 μ)
nonzero : μ ≠ 0
f : Ω →ᵇ ℝ≥0
lim_mass : Tendsto (fun (i : γ) ↦ (μs i).mass) F (𝓝 μ.mass)
aux : {0}ᶜ ∈ 𝓝 μ.mass
⊢ ∀ᶠ (i : γ) in F, (μs i).mass ≠ 0

Tactic:
exact lim_mass aux
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto μs F (𝓝 μ)
nonzero : μ ≠ 0
f : Ω →ᵇ ℝ≥0
lim_mass : Tendsto (fun (i : γ) ↦ (μs i).mass) F (𝓝 μ.mass)
aux : {0}ᶜ ∈ 𝓝 μ.mass
⊢ ∀ᶠ (i : γ) in F, μs i ≠ 0

Tactic:
have eventually_nonzero : ∀ᶠ i in F, μs i ≠ 0 := by
    simp_rw [← mass_nonzero_iff]
    exact lim_mass aux
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto μs F (𝓝 μ)
nonzero : μ ≠ 0
f : Ω →ᵇ ℝ≥0
lim_mass : Tendsto (fun (i : γ) ↦ (μs i).mass) F (𝓝 μ.mass)
aux : {0}ᶜ ∈ 𝓝 μ.mass
eventually_nonzero : ∀ᶠ (i : γ) in F, μs i ≠ 0
h : ∀ (a : γ), μs a ≠ 0 → (μs a).normalize.toFiniteMeasure.testAgainstNN f = (μs a).mass⁻¹ * (μs a).testAgainstNN f
⊢ ∀ᶠ (i : γ) in F, (μs i).normalize.toFiniteMeasure.testAgainstNN f = (μs i).mass⁻¹ * (μs i).testAgainstNN f

Tactic:
filter_upwards [eventually_iff.mp eventually_nonzero]

Premises used: Filter.eventually_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto μs F (𝓝 μ)
nonzero : μ ≠ 0
f : Ω →ᵇ ℝ≥0
lim_mass : Tendsto (fun (i : γ) ↦ (μs i).mass) F (𝓝 μ.mass)
aux : {0}ᶜ ∈ 𝓝 μ.mass
eventually_nonzero : ∀ᶠ (i : γ) in F, μs i ≠ 0
i : γ
hi : μs i ≠ 0
⊢ (μs i).normalize.toFiniteMeasure.testAgainstNN f = (μs i).mass⁻¹ * (μs i).testAgainstNN f

Tactic:
apply normalize_testAgainstNN _ hi

Premises used: MeasureTheory.FiniteMeasure.normalize_testAgainstNN
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto μs F (𝓝 μ)
nonzero : μ ≠ 0
f : Ω →ᵇ ℝ≥0
lim_mass : Tendsto (fun (i : γ) ↦ (μs i).mass) F (𝓝 μ.mass)
aux : {0}ᶜ ∈ 𝓝 μ.mass
eventually_nonzero : ∀ᶠ (i : γ) in F, μs i ≠ 0
⊢ ∀ᶠ (i : γ) in F, (μs i).normalize.toFiniteMeasure.testAgainstNN f = (μs i).mass⁻¹ * (μs i).testAgainstNN f

Tactic:
have eve : ∀ᶠ i in F,
      (μs i).normalize.toFiniteMeasure.testAgainstNN f =
        (μs i).mass⁻¹ * (μs i).testAgainstNN f := by
    filter_upwards [eventually_iff.mp eventually_nonzero]
    intro i hi
    apply normalize_testAgainstNN _ hi
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto μs F (𝓝 μ)
nonzero : μ ≠ 0
f : Ω →ᵇ ℝ≥0
lim_mass : Tendsto (fun (i : γ) ↦ (μs i).mass) F (𝓝 μ.mass)
aux : {0}ᶜ ∈ 𝓝 μ.mass
eventually_nonzero : ∀ᶠ (i : γ) in F, μs i ≠ 0
eve : ∀ᶠ (i : γ) in F, (μs i).normalize.toFiniteMeasure.testAgainstNN f = (μs i).mass⁻¹ * (μs i).testAgainstNN f
simp_rw : Tendsto (fun (x : γ) ↦ (μs x).mass⁻¹ * (μs x).testAgainstNN f) F (𝓝 (μ.mass⁻¹ * μ.testAgainstNN f))
⊢ Tendsto (fun (i : γ) ↦ (μs i).normalize.toFiniteMeasure.testAgainstNN f) F
    (𝓝 (μ.normalize.toFiniteMeasure.testAgainstNN f))

Tactic:
simp_rw [tendsto_congr' eve, μ.normalize_testAgainstNN nonzero]

Premises used: MeasureTheory.FiniteMeasure.normalize_testAgainstNN, Filter.tendsto_congr'
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto μs F (𝓝 μ)
nonzero : μ ≠ 0
f : Ω →ᵇ ℝ≥0
lim_mass : Tendsto (fun (i : γ) ↦ (μs i).mass) F (𝓝 μ.mass)
aux : {0}ᶜ ∈ 𝓝 μ.mass
eventually_nonzero : ∀ᶠ (i : γ) in F, μs i ≠ 0
eve : ∀ᶠ (i : γ) in F, (μs i).normalize.toFiniteMeasure.testAgainstNN f = (μs i).mass⁻¹ * (μs i).testAgainstNN f
⊢ Tendsto (fun (i : γ) ↦ ((μs i).mass⁻¹, (μs i).testAgainstNN f)) F (𝓝 (μ.mass⁻¹, μ.testAgainstNN f))

Tactic:
(Prod.tendsto_iff _ _).mpr ⟨?_, ?_⟩

Premises used: Iff.mpr, Prod.tendsto_iff, And.intro
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto μs F (𝓝 μ)
nonzero : μ ≠ 0
f : Ω →ᵇ ℝ≥0
lim_mass : Tendsto (fun (i : γ) ↦ (μs i).mass) F (𝓝 μ.mass)
aux : {0}ᶜ ∈ 𝓝 μ.mass
eventually_nonzero : ∀ᶠ (i : γ) in F, μs i ≠ 0
eve : ∀ᶠ (i : γ) in F, (μs i).normalize.toFiniteMeasure.testAgainstNN f = (μs i).mass⁻¹ * (μs i).testAgainstNN f
refine_1 : Tendsto (fun (n : γ) ↦ ((μs n).mass⁻¹, (μs n).testAgainstNN f).1) F (𝓝 (μ.mass⁻¹, μ.testAgainstNN f).1)
refine_2 : Tendsto (fun (n : γ) ↦ ((μs n).mass⁻¹, (μs n).testAgainstNN f).2) F (𝓝 (μ.mass⁻¹, μ.testAgainstNN f).2)
⊢ Tendsto (fun (i : γ) ↦ ((μs i).mass⁻¹, (μs i).testAgainstNN f)) F (𝓝 (μ.mass⁻¹, μ.testAgainstNN f))

Tactic:
refine (Prod.tendsto_iff _ _).mpr ⟨?_, ?_⟩

Premises used: Iff.mpr, Prod.tendsto_iff, And.intro
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto μs F (𝓝 μ)
nonzero : μ ≠ 0
f : Ω →ᵇ ℝ≥0
lim_mass : Tendsto (fun (i : γ) ↦ (μs i).mass) F (𝓝 μ.mass)
aux : {0}ᶜ ∈ 𝓝 μ.mass
eventually_nonzero : ∀ᶠ (i : γ) in F, μs i ≠ 0
eve : ∀ᶠ (i : γ) in F, (μs i).normalize.toFiniteMeasure.testAgainstNN f = (μs i).mass⁻¹ * (μs i).testAgainstNN f
⊢ Tendsto (fun (n : γ) ↦ ((μs n).mass⁻¹, (μs n).testAgainstNN f).1) F (𝓝 (μ.mass⁻¹, μ.testAgainstNN f).1)

Tactic:
(continuousOn_inv₀.continuousAt aux).tendsto.comp lim_mass

Premises used: continuousOn_inv₀, ContinuousAt.tendsto, Filter.Tendsto.comp, ContinuousOn.continuousAt
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto μs F (𝓝 μ)
nonzero : μ ≠ 0
f : Ω →ᵇ ℝ≥0
lim_mass : Tendsto (fun (i : γ) ↦ (μs i).mass) F (𝓝 μ.mass)
aux : {0}ᶜ ∈ 𝓝 μ.mass
eventually_nonzero : ∀ᶠ (i : γ) in F, μs i ≠ 0
eve : ∀ᶠ (i : γ) in F, (μs i).normalize.toFiniteMeasure.testAgainstNN f = (μs i).mass⁻¹ * (μs i).testAgainstNN f
⊢ Tendsto (fun (n : γ) ↦ ((μs n).mass⁻¹, (μs n).testAgainstNN f).1) F (𝓝 (μ.mass⁻¹, μ.testAgainstNN f).1)

Tactic:
exact (continuousOn_inv₀.continuousAt aux).tendsto.comp lim_mass

Premises used: continuousOn_inv₀, ContinuousAt.tendsto, Filter.Tendsto.comp, ContinuousOn.continuousAt
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto μs F (𝓝 μ)
nonzero : μ ≠ 0
f : Ω →ᵇ ℝ≥0
lim_mass : Tendsto (fun (i : γ) ↦ (μs i).mass) F (𝓝 μ.mass)
aux : {0}ᶜ ∈ 𝓝 μ.mass
eventually_nonzero : ∀ᶠ (i : γ) in F, μs i ≠ 0
eve : ∀ᶠ (i : γ) in F, (μs i).normalize.toFiniteMeasure.testAgainstNN f = (μs i).mass⁻¹ * (μs i).testAgainstNN f
⊢ Tendsto (fun (n : γ) ↦ ((μs n).mass⁻¹, (μs n).testAgainstNN f).2) F (𝓝 (μ.mass⁻¹, μ.testAgainstNN f).2)

Tactic:
tendsto_iff_forall_testAgainstNN_tendsto.mp μs_lim f

Premises used: ENNReal.toNNReal, MeasureTheory.FiniteMeasure.testAgainstNN, Iff.mp, WithTop.untopD, WithTop.recTopCoe, MeasureTheory.FiniteMeasure.tendsto_iff_forall_testAgainstNN_tendsto
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto μs F (𝓝 μ)
nonzero : μ ≠ 0
f : Ω →ᵇ ℝ≥0
lim_mass : Tendsto (fun (i : γ) ↦ (μs i).mass) F (𝓝 μ.mass)
aux : {0}ᶜ ∈ 𝓝 μ.mass
eventually_nonzero : ∀ᶠ (i : γ) in F, μs i ≠ 0
eve : ∀ᶠ (i : γ) in F, (μs i).normalize.toFiniteMeasure.testAgainstNN f = (μs i).mass⁻¹ * (μs i).testAgainstNN f
⊢ Tendsto (fun (n : γ) ↦ ((μs n).mass⁻¹, (μs n).testAgainstNN f).2) F (𝓝 (μ.mass⁻¹, μ.testAgainstNN f).2)

Tactic:
exact tendsto_iff_forall_testAgainstNN_tendsto.mp μs_lim f

Premises used: Iff.mp, MeasureTheory.FiniteMeasure.tendsto_iff_forall_testAgainstNN_tendsto
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto μs F (𝓝 μ)
nonzero : μ ≠ 0
f : Ω →ᵇ ℝ≥0
lim_mass : Tendsto (fun (i : γ) ↦ (μs i).mass) F (𝓝 μ.mass)
aux : {0}ᶜ ∈ 𝓝 μ.mass
eventually_nonzero : ∀ᶠ (i : γ) in F, μs i ≠ 0
eve : ∀ᶠ (i : γ) in F, (μs i).normalize.toFiniteMeasure.testAgainstNN f = (μs i).mass⁻¹ * (μs i).testAgainstNN f
⊢ Tendsto (fun (i : γ) ↦ ((μs i).mass⁻¹, (μs i).testAgainstNN f)) F (𝓝 (μ.mass⁻¹, μ.testAgainstNN f))

Tactic:
have lim_pair :
    Tendsto (fun i ↦ (⟨(μs i).mass⁻¹, (μs i).testAgainstNN f⟩ : ℝ≥0 × ℝ≥0)) F
      (𝓝 ⟨μ.mass⁻¹, μ.testAgainstNN f⟩) := by
    refine (Prod.tendsto_iff _ _).mpr ⟨?_, ?_⟩
    · exact (continuousOn_inv₀.continuousAt aux).tendsto.comp lim_mass
    · exact tendsto_iff_forall_testAgainstNN_tendsto.mp μs_lim f
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto μs F (𝓝 μ)
nonzero : μ ≠ 0
f : Ω →ᵇ ℝ≥0
lim_mass : Tendsto (fun (i : γ) ↦ (μs i).mass) F (𝓝 μ.mass)
aux : {0}ᶜ ∈ 𝓝 μ.mass
eventually_nonzero : ∀ᶠ (i : γ) in F, μs i ≠ 0
eve : ∀ᶠ (i : γ) in F, (μs i).normalize.toFiniteMeasure.testAgainstNN f = (μs i).mass⁻¹ * (μs i).testAgainstNN f
lim_pair : Tendsto (fun (i : γ) ↦ ((μs i).mass⁻¹, (μs i).testAgainstNN f)) F (𝓝 (μ.mass⁻¹, μ.testAgainstNN f))
⊢ Tendsto (fun (x : γ) ↦ (μs x).mass⁻¹ * (μs x).testAgainstNN f) F (𝓝 (μ.mass⁻¹ * μ.testAgainstNN f))

Tactic:
tendsto_mul.comp lim_pair

Premises used: ENNReal.toNNReal, MeasureTheory.FiniteMeasure.testAgainstNN, tendsto_mul, WithTop.untopD, Filter.Tendsto.comp, WithTop.recTopCoe
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto μs F (𝓝 μ)
nonzero : μ ≠ 0
f : Ω →ᵇ ℝ≥0
lim_mass : Tendsto (fun (i : γ) ↦ (μs i).mass) F (𝓝 μ.mass)
aux : {0}ᶜ ∈ 𝓝 μ.mass
eventually_nonzero : ∀ᶠ (i : γ) in F, μs i ≠ 0
eve : ∀ᶠ (i : γ) in F, (μs i).normalize.toFiniteMeasure.testAgainstNN f = (μs i).mass⁻¹ * (μs i).testAgainstNN f
lim_pair : Tendsto (fun (i : γ) ↦ ((μs i).mass⁻¹, (μs i).testAgainstNN f)) F (𝓝 (μ.mass⁻¹, μ.testAgainstNN f))
⊢ Tendsto (fun (x : γ) ↦ (μs x).mass⁻¹ * (μs x).testAgainstNN f) F (𝓝 (μ.mass⁻¹ * μ.testAgainstNN f))

Tactic:
exact tendsto_mul.comp lim_pair

Premises used: tendsto_mul, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto (fun (i : γ) ↦ (μs i).normalize) F (𝓝 μ.normalize)
mass_lim : Tendsto (fun (i : γ) ↦ (μs i).mass) F (𝓝 μ.mass)
rw : ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun (i : γ) ↦ (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))
⊢ Tendsto μs F (𝓝 μ)

Tactic:
rw [tendsto_iff_forall_testAgainstNN_tendsto]

Premises used: MeasureTheory.FiniteMeasure.tendsto_iff_forall_testAgainstNN_tendsto
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto (fun (i : γ) ↦ (μs i).normalize) F (𝓝 μ.normalize)
mass_lim : Tendsto (fun (i : γ) ↦ (μs i).mass) F (𝓝 μ.mass)
⊢ ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun (i : γ) ↦ (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))

Tactic:
fun f ↦
    tendsto_testAgainstNN_of_tendsto_normalize_testAgainstNN_of_tendsto_mass μs_lim mass_lim f

Premises used: MeasureTheory.FiniteMeasure.tendsto_testAgainstNN_of_tendsto_normalize_testAgainstNN_of_tendsto_mass
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto (fun (i : γ) ↦ (μs i).normalize) F (𝓝 μ.normalize)
mass_lim : Tendsto (fun (i : γ) ↦ (μs i).mass) F (𝓝 μ.mass)
⊢ ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun (i : γ) ↦ (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))

Tactic:
exact fun f ↦
    tendsto_testAgainstNN_of_tendsto_normalize_testAgainstNN_of_tendsto_mass μs_lim mass_lim f

Premises used: MeasureTheory.FiniteMeasure.tendsto_testAgainstNN_of_tendsto_normalize_testAgainstNN_of_tendsto_mass
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto μs F (𝓝 μ)
nonzero : μ ≠ 0
rw :
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : γ) ↦ testAgainstNN ((ProbabilityMeasure.toFiniteMeasure ∘ fun (i : γ) ↦ (μs i).normalize) i) f) F
      (𝓝 (μ.normalize.toFiniteMeasure.testAgainstNN f))
⊢ Tendsto (fun (i : γ) ↦ (μs i).normalize) F (𝓝 μ.normalize)

Tactic:
rw [ProbabilityMeasure.tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds,
    tendsto_iff_forall_testAgainstNN_tendsto]

Premises used: MeasureTheory.ProbabilityMeasure.tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds, MeasureTheory.FiniteMeasure.tendsto_iff_forall_testAgainstNN_tendsto
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto μs F (𝓝 μ)
nonzero : μ ≠ 0
⊢ ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : γ) ↦ testAgainstNN ((ProbabilityMeasure.toFiniteMeasure ∘ fun (i : γ) ↦ (μs i).normalize) i) f) F
      (𝓝 (μ.normalize.toFiniteMeasure.testAgainstNN f))

Tactic:
fun f ↦ tendsto_normalize_testAgainstNN_of_tendsto μs_lim nonzero f

Premises used: MeasureTheory.ProbabilityMeasure.toFiniteMeasure, MeasureTheory.FiniteMeasure.tendsto_normalize_testAgainstNN_of_tendsto
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto μs F (𝓝 μ)
nonzero : μ ≠ 0
⊢ ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : γ) ↦ testAgainstNN ((ProbabilityMeasure.toFiniteMeasure ∘ fun (i : γ) ↦ (μs i).normalize) i) f) F
      (𝓝 (μ.normalize.toFiniteMeasure.testAgainstNN f))

Tactic:
exact fun f ↦ tendsto_normalize_testAgainstNN_of_tendsto μs_lim nonzero f

Premises used: MeasureTheory.FiniteMeasure.tendsto_normalize_testAgainstNN_of_tendsto
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
nonzero : μ ≠ 0
mp :
  Tendsto (fun (i : γ) ↦ (μs i).normalize) F (𝓝 μ.normalize) ∧ Tendsto (fun (i : γ) ↦ (μs i).mass) F (𝓝 μ.mass) →
    Tendsto μs F (𝓝 μ)
mpr :
  Tendsto μs F (𝓝 μ) →
    Tendsto (fun (i : γ) ↦ (μs i).normalize) F (𝓝 μ.normalize) ∧ Tendsto (fun (i : γ) ↦ (μs i).mass) F (𝓝 μ.mass)
⊢ Tendsto (fun (i : γ) ↦ (μs i).normalize) F (𝓝 μ.normalize) ∧ Tendsto (fun (i : γ) ↦ (μs i).mass) F (𝓝 μ.mass) ↔
    Tendsto μs F (𝓝 μ)

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
nonzero : μ ≠ 0
normalized_lim : Tendsto (fun (i : γ) ↦ (μs i).normalize) F (𝓝 μ.normalize)
mass_lim : Tendsto (fun (i : γ) ↦ (μs i).mass) F (𝓝 μ.mass)
⊢ Tendsto μs F (𝓝 μ)

Tactic:
tendsto_of_tendsto_normalize_testAgainstNN_of_tendsto_mass normalized_lim mass_lim

Premises used: MeasureTheory.FiniteMeasure.tendsto_of_tendsto_normalize_testAgainstNN_of_tendsto_mass
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
nonzero : μ ≠ 0
normalized_lim : Tendsto (fun (i : γ) ↦ (μs i).normalize) F (𝓝 μ.normalize)
mass_lim : Tendsto (fun (i : γ) ↦ (μs i).mass) F (𝓝 μ.mass)
⊢ Tendsto μs F (𝓝 μ)

Tactic:
exact tendsto_of_tendsto_normalize_testAgainstNN_of_tendsto_mass normalized_lim mass_lim

Premises used: MeasureTheory.FiniteMeasure.tendsto_of_tendsto_normalize_testAgainstNN_of_tendsto_mass
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
nonzero : μ ≠ 0
μs_lim : Tendsto μs F (𝓝 μ)
⊢ Tendsto (fun (i : γ) ↦ (μs i).normalize) F (𝓝 μ.normalize) ∧ Tendsto (fun (i : γ) ↦ (μs i).mass) F (𝓝 μ.mass)

Tactic:
⟨tendsto_normalize_of_tendsto μs_lim nonzero, μs_lim.mass⟩

Premises used: Filter.Tendsto.mass, MeasureTheory.FiniteMeasure.tendsto_normalize_of_tendsto, And.intro