awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst_1 : TopologicalSpace Ω
f : Ω →ᵇ ℝ≥0
⊢ μ.testAgainstNN f = μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f
have nth_rw : (μ.mass • μ.normalize.toFiniteMeasure).testAgainstNN f = μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f
Tactic: nth_rw 1 [μ.self_eq_mass_smul_normalize]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst_1 : TopologicalSpace Ω
f : Ω →ᵇ ℝ≥0
⊢ (μ.mass • μ.normalize.toFiniteMeasure).testAgainstNN f = μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f
have rw : μ.mass • μ.normalize.toFiniteMeasure.testAgainstNN f = μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f
Tactic: rw [μ.normalize.toFiniteMeasure.smul_testAgainstNN_apply μ.mass f, smul_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst_1 : TopologicalSpace Ω
f : Ω →ᵇ ℝ≥0
rw : μ.mass • μ.normalize.toFiniteMeasure.testAgainstNN f = μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f
⊢ (μ.mass • μ.normalize.toFiniteMeasure).testAgainstNN f = μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f
have rw₁ : μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f = μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f
Tactic: rw [μ.normalize.toFiniteMeasure.smul_testAgainstNN_apply μ.mass f, smul_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
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))
have pos : ∀ (h_mass : μ.mass = 0), Tendsto (fun (i : γ) ↦ (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))
Tactic: by_cases h_mass : μ.mass = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
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
pos : ∀ (h_mass : μ.mass = 0), Tendsto (fun (i : γ) ↦ (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))
⊢ Tendsto (fun (i : γ) ↦ (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))
have neg : ∀ (h_mass : ¬μ.mass = 0), Tendsto (fun (i : γ) ↦ (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))
Tactic: by_cases h_mass : μ.mass = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
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
h_mass : μ.mass = 0
⊢ Tendsto (fun (i : γ) ↦ (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))
have pos : ∀ (mass_lim : Tendsto (β := ℝ≥0) (fun (i : γ) ↦ (μs i).mass) F (𝓝 0)),
  Tendsto (β := ℝ≥0) (fun (i : γ) ↦ (μs i).testAgainstNN f) F (𝓝 0)
Tactic: simp only [μ.mass_zero_iff.mp h_mass, zero_testAgainstNN_apply, zero_mass] at mass_lim ⊢
Cleared hypotheses: mass_lim
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
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
h_mass : ¬μ.mass = 0
⊢ Tendsto (fun (i : γ) ↦ (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))
have neg : Tendsto (fun (i : γ) ↦ (μs i).mass * (μs i).normalize.toFiniteMeasure.testAgainstNN f) F
  (𝓝 (μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f))
Tactic: simp_rw [fun i ↦ (μs i).testAgainstNN_eq_mass_mul f, μ.testAgainstNN_eq_mass_mul f]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
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
h_mass : ¬μ.mass = 0
⊢ Tendsto (fun (i : γ) ↦ (μs i).mass * (μs i).normalize.toFiniteMeasure.testAgainstNN f) F
    (𝓝 (μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f))
have neg : ∀
  (μ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),
  Tendsto (fun (i : γ) ↦ (μs i).mass * (μs i).normalize.toFiniteMeasure.testAgainstNN f) F
    (𝓝 (μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f))
Tactic: rw [ProbabilityMeasure.tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds] at μs_lim
Cleared hypotheses: μs_lim, mass_lim, f, h_mass
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
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
⊢ Tendsto (fun (i : γ) ↦ (μs i).mass * (μs i).normalize.toFiniteMeasure.testAgainstNN f) F
    (𝓝 (μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f))
have 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))
Tactic: rw [tendsto_iff_forall_testAgainstNN_tendsto] at μs_lim
Cleared hypotheses: μs_lim, mass_lim, f, h_mass
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (hypothesis)
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))
have lim_pair : 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⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (hypothesis)
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).normalize.toFiniteMeasure.testAgainstNN f) F
    (𝓝 (μ.normalize.toFiniteMeasure.testAgainstNN f))
have lim_mass : Tendsto (fun (i : γ) ↦ (μs i).mass) F (𝓝 μ.mass)
Tactic: have lim_mass := μs_lim.mass
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (hypothesis)
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)
⊢ Tendsto (fun (i : γ) ↦ (μs i).normalize.toFiniteMeasure.testAgainstNN f) F
    (𝓝 (μ.normalize.toFiniteMeasure.testAgainstNN f))
have aux : {0}ᶜ ∈ 𝓝 μ.mass
Tactic: have aux : {(0 : ℝ≥0)}ᶜ ∈ 𝓝 μ.mass :=
    isOpen_compl_singleton.mem_nhds (μ.mass_nonzero_iff.mpr nonzero)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
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
have simp_rw : ∀ᶠ (i : γ) in F, (μs i).mass ≠ 0
Tactic: simp_rw [← mass_nonzero_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (hypothesis)
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
⊢ Tendsto (fun (i : γ) ↦ (μs i).normalize.toFiniteMeasure.testAgainstNN f) F
    (𝓝 (μ.normalize.toFiniteMeasure.testAgainstNN f))
have eventually_nonzero : ∀ᶠ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
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
have h : ∀ (a : γ), μs a ≠ 0 → (μs a).normalize.toFiniteMeasure.testAgainstNN f = (μs a).mass⁻¹ * (μs a).testAgainstNN f
Tactic: filter_upwards [eventually_iff.mp eventually_nonzero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (hypothesis)
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
⊢ Tendsto (fun (i : γ) ↦ (μs i).normalize.toFiniteMeasure.testAgainstNN f) F
    (𝓝 (μ.normalize.toFiniteMeasure.testAgainstNN f))
have eve : ∀ᶠ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
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).normalize.toFiniteMeasure.testAgainstNN f) F
    (𝓝 (μ.normalize.toFiniteMeasure.testAgainstNN f))
have simp_rw : Tendsto (fun (x : γ) ↦ (μs x).mass⁻¹ * (μs x).testAgainstNN f) F (𝓝 (μ.mass⁻¹ * μ.testAgainstNN f))
Tactic: simp_rw [tendsto_congr' eve, μ.normalize_testAgainstNN nonzero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
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))
have refine_1 : Tendsto (fun (n : γ) ↦ ((μs n).mass⁻¹, (μs n).testAgainstNN f).1) F (𝓝 (μ.mass⁻¹, μ.testAgainstNN f).1)
Tactic: refine (Prod.tendsto_iff _ _).mpr ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
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)
⊢ Tendsto (fun (i : γ) ↦ ((μs i).mass⁻¹, (μs i).testAgainstNN f)) F (𝓝 (μ.mass⁻¹, μ.testAgainstNN f))
have refine_2 : Tendsto (fun (n : γ) ↦ ((μs n).mass⁻¹, (μs n).testAgainstNN f).2) F (𝓝 (μ.mass⁻¹, μ.testAgainstNN f).2)
Tactic: refine (Prod.tendsto_iff _ _).mpr ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (hypothesis)
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 (x : γ) ↦ (μs x).mass⁻¹ * (μs x).testAgainstNN f) F (𝓝 (μ.mass⁻¹ * μ.testAgainstNN f))
have lim_pair : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
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)
⊢ Tendsto μs F (𝓝 μ)
have rw : ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun (i : γ) ↦ (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))
Tactic: rw [tendsto_iff_forall_testAgainstNN_tendsto]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
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
⊢ Tendsto (fun (i : γ) ↦ (μs i).normalize) F (𝓝 μ.normalize)
have rw : ∀ (f : Ω →ᵇ ℝ≥0),
  Tendsto (fun (i : γ) ↦ testAgainstNN ((ProbabilityMeasure.toFiniteMeasure ∘ fun (i : γ) ↦ (μs i).normalize) i) f) F
    (𝓝 (μ.normalize.toFiniteMeasure.testAgainstNN f))
Tactic: rw [ProbabilityMeasure.tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds,
    tendsto_iff_forall_testAgainstNN_tendsto]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
nonzero : μ ≠ 0
⊢ Tendsto (fun (i : γ) ↦ (μs i).normalize) F (𝓝 μ.normalize) ∧ Tendsto (fun (i : γ) ↦ (μs i).mass) F (𝓝 μ.mass) ↔
    Tendsto μs F (𝓝 μ)
have mp : Tendsto (fun (i : γ) ↦ (μs i).normalize) F (𝓝 μ.normalize) ∧ Tendsto (fun (i : γ) ↦ (μs i).mass) F (𝓝 μ.mass) →
  Tendsto μs F (𝓝 μ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
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 (𝓝 μ)
⊢ Tendsto (fun (i : γ) ↦ (μs i).normalize) F (𝓝 μ.normalize) ∧ Tendsto (fun (i : γ) ↦ (μs i).mass) F (𝓝 μ.mass) ↔
    Tendsto μs F (𝓝 μ)
have mpr : Tendsto μs F (𝓝 μ) →
  Tendsto (fun (i : γ) ↦ (μs i).normalize) F (𝓝 μ.normalize) ∧ Tendsto (fun (i : γ) ↦ (μs i).mass) F (𝓝 μ.mass)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
inst_2 : TopologicalSpace Ω
inst_3 : OpensMeasurableSpace Ω
inst_4 : TopologicalSpace Ω'
inst_5 : BorelSpace Ω'
ι : Type u_3
L : Filter ι
νs : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
lim : Tendsto νs L (𝓝 ν)
f : Ω → Ω'
f_cont : Continuous[inst_2, inst_4] f
⊢ Tendsto (β := ProbabilityMeasure Ω') (fun (i : ι) ↦ (νs i).map ⋯) L (𝓝 (ν.map ⋯))
have rw : ∀
  (lim :
    ∀ (f : Ω →ᵇ ℝ≥0),
      Tendsto (fun (i : ι) ↦ ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(νs i) : Measure Ω)) L
        (𝓝 (∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑ν : Measure Ω))))
  {f : Ω → Ω'} (f_cont : Continuous[inst_2, inst_4] f) (f_1 : Ω' →ᵇ ℝ≥0),
  Tendsto (fun (i : ι) ↦ ∫⁻ (ω : Ω'), (↑((f_1 : (a : Ω') → ℝ≥0) ω) : ℝ≥0∞) ∂(↑((νs i).map sorry) : Measure Ω')) L
    (𝓝 (∫⁻ (ω : Ω'), (↑((f_1 : (a : Ω') → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(ν.map sorry) : Measure Ω')))
Tactic: rw [ProbabilityMeasure.tendsto_iff_forall_lintegral_tendsto] at lim ⊢
Cleared hypotheses: lim, f, f_cont
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
inst_2 : TopologicalSpace Ω
inst_3 : OpensMeasurableSpace Ω
inst_4 : TopologicalSpace Ω'
inst_5 : BorelSpace Ω'
ι : Type u_3
L : Filter ι
νs : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
lim :
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : ι) ↦ ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(νs i) : Measure Ω)) L
      (𝓝 (∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑ν : Measure Ω)))
f : Ω → Ω'
f_cont : Continuous[inst_2, inst_4] f
g : Ω' →ᵇ ℝ≥0
⊢ Tendsto (fun (i : ι) ↦ ∫⁻ (ω : Ω'), (↑((g : (a : Ω') → ℝ≥0) ω) : ℝ≥0∞) ∂(↑((νs i).map ⋯) : Measure Ω')) L
    (𝓝 (∫⁻ (ω : Ω'), (↑((g : (a : Ω') → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(ν.map ⋯) : Measure Ω')))
have h : ∀ (x : ι),
  ∫⁻ (ω : Ω'), (↑((g : (a : Ω') → ℝ≥0) ω) : ℝ≥0∞) ∂(↑((νs x).map sorry) : Measure Ω') =
    ∫⁻ (ω : Ω),
      (↑((g.compContinuous { toFun := f, continuous_toFun := f_cont : C(Ω, Ω') } : (a : Ω) → ℝ≥0) ω) :
        ℝ≥0∞) ∂(↑(νs x) : Measure Ω)
Tactic: convert! lim (g.compContinuous ⟨f, f_cont⟩)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
inst_2 : TopologicalSpace Ω
inst_3 : OpensMeasurableSpace Ω
inst_4 : TopologicalSpace Ω'
inst_5 : BorelSpace Ω'
ι : Type u_3
L : Filter ι
νs : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
lim :
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : ι) ↦ ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(νs i) : Measure Ω)) L
      (𝓝 (∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑ν : Measure Ω)))
f : Ω → Ω'
f_cont : Continuous[inst_2, inst_4] f
g : Ω' →ᵇ ℝ≥0
h :
  ∀ (x : ι),
    ∫⁻ (ω : Ω'), (↑((g : (a : Ω') → ℝ≥0) ω) : ℝ≥0∞) ∂(↑((νs x).map ⋯) : Measure Ω') =
      ∫⁻ (ω : Ω),
        (↑((g.compContinuous { toFun := f, continuous_toFun := f_cont : C(Ω, Ω') } : (a : Ω) → ℝ≥0) ω) :
          ℝ≥0∞) ∂(↑(νs x) : Measure Ω)
⊢ Tendsto (fun (i : ι) ↦ ∫⁻ (ω : Ω'), (↑((g : (a : Ω') → ℝ≥0) ω) : ℝ≥0∞) ∂(↑((νs i).map ⋯) : Measure Ω')) L
    (𝓝 (∫⁻ (ω : Ω'), (↑((g : (a : Ω') → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(ν.map ⋯) : Measure Ω')))
have h₁ : ∫⁻ (ω : Ω'), (↑((g : (a : Ω') → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(ν.map sorry) : Measure Ω') =
  ∫⁻ (ω : Ω),
    (↑((g.compContinuous { toFun := f, continuous_toFun := f_cont : C(Ω, Ω') } : (a : Ω) → ℝ≥0) ω) :
      ℝ≥0∞) ∂(↑ν : Measure Ω)
Tactic: convert! lim (g.compContinuous ⟨f, f_cont⟩)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
inst_2 : TopologicalSpace Ω
inst_3 : OpensMeasurableSpace Ω
inst_4 : TopologicalSpace Ω'
inst_5 : BorelSpace Ω'
ι : Type u_3
L : Filter ι
νs : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
lim :
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : ι) ↦ ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(νs i) : Measure Ω)) L
      (𝓝 (∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑ν : Measure Ω)))
f : Ω → Ω'
f_cont : Continuous[inst_2, inst_4] f
g : Ω' →ᵇ ℝ≥0
x : ι
⊢ ∫⁻ (ω : Ω'), (↑((g : (a : Ω') → ℝ≥0) ω) : ℝ≥0∞) ∂(↑((νs x).map ⋯) : Measure Ω') =
    ∫⁻ (ω : Ω),
      (↑((g.compContinuous { toFun := f, continuous_toFun := f_cont : C(Ω, Ω') } : (a : Ω) → ℝ≥0) ω) :
        ℝ≥0∞) ∂(↑(νs x) : Measure Ω)
have h : ∫⁻ (ω : Ω'),
    (↑((g : (a : Ω') → ℝ≥0) ω) :
      ℝ≥0∞) ∂(↑(Subtype.mk (p := fun (μ : Measure Ω') ↦ IsProbabilityMeasure μ) (Measure.map f (↑(νs x) : Measure Ω))
          sorry) :
      Measure Ω') =
  ∫⁻ (ω : Ω), (↑((g : (a : Ω') → ℝ≥0) (f ω)) : ℝ≥0∞) ∂(↑(νs x) : Measure Ω)
Tactic: simp only [map, compContinuous_apply, ContinuousMap.coe_mk]