awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : MeasurableSpace X
inst_3 : OpensMeasurableSpace X
F : Type u_3
inst_4 : FunLike F X ℝ≥0
inst_5 : ContinuousMapClass F X ℝ≥0
f : F
⊢ Continuous[instTopologicalSpace, _] fun (μ : ProbabilityMeasure X) ↦
    ∫⁻ (x : X), (↑((f : (a : X) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure X)

Tactic:
continuous_iff_forall_continuousMap_continuous_lintegral.1 continuous_id ⟨f, map_continuous f⟩

Premises used: ContinuousMap.mk, continuous_id, Iff.mp, ContinuousMapClass.map_continuous, MeasureTheory.ProbabilityMeasure.continuous_iff_forall_continuousMap_continuous_lintegral, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : MeasurableSpace X
inst_3 : OpensMeasurableSpace X
F : Type u_3
inst_4 : FunLike F X ℝ
inst_5 : ContinuousMapClass F X ℝ
f : F
⊢ Continuous[instTopologicalSpace, _] fun (μ : ProbabilityMeasure X) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂(↑μ : Measure X)

Tactic:
continuous_iff_forall_continuousMap_continuous_integral.1 continuous_id ⟨f, map_continuous f⟩

Premises used: ContinuousMap.mk, MeasureTheory.ProbabilityMeasure.continuous_iff_forall_continuousMap_continuous_integral, continuous_id, Iff.mp, ContinuousMapClass.map_continuous, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : BorelSpace Ω
⊢ T2Space.{u_1} (ProbabilityMeasure Ω)

Tactic:
(toFiniteMeasure_isEmbedding Ω).t2Space

Premises used: MeasureTheory.ProbabilityMeasure.toFiniteMeasure_isEmbedding, Topology.IsEmbedding.t2Space
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
zero : ¬μ.mass = 0
⊢ IsProbabilityMeasure (μ.mass⁻¹ • (↑μ : Measure Ω))

Tactic:
⟨?_⟩

Premises used: MeasureTheory.IsProbabilityMeasure.mk
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
zero : ¬μ.mass = 0
refine : Eq (α := ℝ≥0∞) ((μ.mass⁻¹ • (↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ IsProbabilityMeasure (μ.mass⁻¹ • (↑μ : Measure Ω))

Tactic:
refine ⟨?_⟩
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
zero : ¬μ.mass = 0
simp :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞)
      (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) =
    1
⊢ Eq (α := ℝ≥0∞) ((μ.mass⁻¹ • (↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
simp only [Measure.coe_smul, Pi.smul_apply, Measure.nnreal_smul_coe_apply,
          ENNReal.coe_inv zero, ennreal_mass]

Premises used: ENNReal.coe_inv, MeasureTheory.Measure.coe_smul, MeasureTheory.Measure.nnreal_smul_coe_apply, MeasureTheory.FiniteMeasure.ennreal_mass, Pi.smul_apply
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
zero : ¬μ.mass = 0
⊢ Ne (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← Ne, ← ENNReal.coe_ne_zero, ennreal_mass] at zero

Premises used: Ne, ENNReal.coe_ne_zero, MeasureTheory.FiniteMeasure.ennreal_mass
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
zero : Ne (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞)
      (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) =
    1

Tactic:
ENNReal.inv_mul_cancel zero μ.prop.measure_univ_lt_top.ne

Premises used: ENNReal.inv_mul_cancel, MeasureTheory.IsFiniteMeasure.measure_univ_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
zero : Ne (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞)
      (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) =
    1

Tactic:
exact ENNReal.inv_mul_cancel zero μ.prop.measure_univ_lt_top.ne

Premises used: ENNReal.inv_mul_cancel, MeasureTheory.IsFiniteMeasure.measure_univ_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
s : Set Ω
inl :
  ((0 : FiniteMeasure Ω) : (a : Set Ω) → ℝ≥0) s =
    HMul.hMul (β := ℝ≥0) (mass.{u_1} (Ω := Ω) 0) (((normalize 0 : ProbabilityMeasure Ω) : (a : Set Ω) → ℝ≥0) s : ℝ≥0)
inr : ∀ (h : μ ≠ 0), (μ : (a : Set Ω) → ℝ≥0) s = HMul.hMul (β := ℝ≥0) μ.mass ((μ.normalize : (a : Set Ω) → ℝ≥0) s : ℝ≥0)
⊢ (μ : (a : Set Ω) → ℝ≥0) s = HMul.hMul (β := ℝ≥0) μ.mass ((μ.normalize : (a : Set Ω) → ℝ≥0) s : ℝ≥0)

Tactic:
obtain rfl | h := eq_or_ne μ 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
s : Set Ω
⊢ ((0 : FiniteMeasure Ω) : (a : Set Ω) → ℝ≥0) s =
    HMul.hMul (β := ℝ≥0) (mass.{u_1} (Ω := Ω) 0) (((normalize 0 : ProbabilityMeasure Ω) : (a : Set Ω) → ℝ≥0) s : ℝ≥0)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
s : Set Ω
h rwa rwa₁ rwa₂ rwa₃ : μ ≠ 0
⊢ μ.mass ≠ 0

Tactic:
rwa [μ.mass_nonzero_iff]

Premises used: MeasureTheory.FiniteMeasure.mass_nonzero_iff
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
s : Set Ω
h : μ ≠ 0
⊢ μ.mass ≠ 0

Tactic:
have mass_nonzero : μ.mass ≠ 0 := by rwa [μ.mass_nonzero_iff]
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
s : Set Ω
h : μ ≠ 0
mass_nonzero : μ.mass ≠ 0
inr :
  (μ : (a : Set Ω) → ℝ≥0) s =
    HMul.hMul (β := ℝ≥0) μ.mass
      ((Subtype.mk (p := fun (μ : Measure Ω) ↦ IsProbabilityMeasure μ) (μ.mass⁻¹ • (↑μ : Measure Ω)) ⋯ :
            (a : Set Ω) → ℝ≥0)
          s :
        ℝ≥0)
⊢ (μ : (a : Set Ω) → ℝ≥0) s = HMul.hMul (β := ℝ≥0) μ.mass ((μ.normalize : (a : Set Ω) → ℝ≥0) s : ℝ≥0)

Tactic:
simp only [normalize, dif_neg mass_nonzero]

Premises used: dif_neg, MeasureTheory.FiniteMeasure.normalize
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
s : Set Ω
h : μ ≠ 0
mass_nonzero : μ.mass ≠ 0
⊢ (μ : (a : Set Ω) → ℝ≥0) s =
    HMul.hMul (β := ℝ≥0) μ.mass
      ((Subtype.mk (p := fun (μ : Measure Ω) ↦ IsProbabilityMeasure μ) (μ.mass⁻¹ • (↑μ : Measure Ω)) ⋯ :
            (a : Set Ω) → ℝ≥0)
          s :
        ℝ≥0)

Tactic:
simp [mul_inv_cancel_left₀ mass_nonzero, coeFn_def]

Premises used: mul_inv_cancel_left₀, MeasureTheory.FiniteMeasure.coeFn_def
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
h :
  ∀ (s : Set Ω),
    MeasurableSet s →
      Eq (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s : ℝ≥0)
        ((μ.mass • μ.normalize.toFiniteMeasure : (a : Set Ω) → ℝ≥0) s : ℝ≥0)
⊢ μ = μ.mass • μ.normalize.toFiniteMeasure

Tactic:
apply eq_of_forall_apply_eq

Premises used: MeasureTheory.FiniteMeasure.eq_of_forall_apply_eq
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
s : Set Ω
_s_mble : MeasurableSet s
h :
  HMul.hMul (β := ℝ≥0) μ.mass ((μ.normalize : (a : Set Ω) → ℝ≥0) s : ℝ≥0) =
    (μ.mass • μ.normalize.toFiniteMeasure : (a : Set Ω) → ℝ≥0) s
h₁ :
  HMul.hMul (β := ℝ≥0) μ.mass ((μ.normalize : (a : Set Ω) → ℝ≥0) s : ℝ≥0) =
    HSMul.hSMul (β := ℝ≥0) μ.mass ((μ.normalize.toFiniteMeasure : (a : Set Ω) → ℝ≥0) s : ℝ≥0)
h₂ :
  HMul.hMul (β := ℝ≥0) μ.mass ((μ.normalize : (a : Set Ω) → ℝ≥0) s : ℝ≥0) =
    HMul.hMul (β := ℝ≥0) μ.mass ((μ.normalize.toFiniteMeasure : (a : Set Ω) → ℝ≥0) s : ℝ≥0)
h₃ h₄ :
  HMul.hMul (β := ℝ≥0) μ.mass ((μ.normalize : (a : Set Ω) → ℝ≥0) s : ℝ≥0) =
    HMul.hMul (β := ℝ≥0) μ.mass ((μ.normalize : (a : Set Ω) → ℝ≥0) s : ℝ≥0)
⊢ Eq (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s : ℝ≥0) ((μ.mass • μ.normalize.toFiniteMeasure : (a : Set Ω) → ℝ≥0) s : ℝ≥0)

Tactic:
rw [μ.self_eq_mass_mul_normalize s, smul_apply, smul_eq_mul,
    ProbabilityMeasure.coeFn_comp_toFiniteMeasure_eq_coeFn]

Premises used: MeasureTheory.ProbabilityMeasure.coeFn_comp_toFiniteMeasure_eq_coeFn, MeasureTheory.FiniteMeasure.self_eq_mass_mul_normalize, MeasureTheory.FiniteMeasure.smul_apply, smul_eq_mul
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
s : Set Ω
⊢ (μ.normalize : (a : Set Ω) → ℝ≥0) s = HMul.hMul (β := ℝ≥0) μ.mass⁻¹ ((μ : (a : Set Ω) → ℝ≥0) s : ℝ≥0)

Tactic:
simp only [μ.self_eq_mass_mul_normalize, μ.mass_nonzero_iff.mpr nonzero, inv_mul_cancel_left₀,
    Ne, not_false_iff]

Premises used: Iff.mpr, MeasureTheory.FiniteMeasure.mass_nonzero_iff, inv_mul_cancel_left₀, MeasureTheory.FiniteMeasure.self_eq_mass_mul_normalize, Ne, not_false_iff
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
nth_rw : μ.normalize.toFiniteMeasure = μ.mass⁻¹ • μ.mass • μ.normalize.toFiniteMeasure
⊢ μ.normalize.toFiniteMeasure = μ.mass⁻¹ • μ

Tactic:
nth_rw 3 [μ.self_eq_mass_smul_normalize]

Premises used: MeasureTheory.FiniteMeasure.self_eq_mass_smul_normalize
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
rw : μ.normalize.toFiniteMeasure = (μ.mass⁻¹ • μ.mass) • μ.normalize.toFiniteMeasure
⊢ μ.normalize.toFiniteMeasure = μ.mass⁻¹ • μ.mass • μ.normalize.toFiniteMeasure

Tactic:
rw [← smul_assoc]

Premises used: smul_assoc
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
⊢ μ.normalize.toFiniteMeasure = (μ.mass⁻¹ • μ.mass) • μ.normalize.toFiniteMeasure

Tactic:
simp only [μ.mass_nonzero_iff.mpr nonzero, smul_eq_mul, inv_mul_cancel₀, Ne,
    not_false_iff, one_smul]

Premises used: Iff.mpr, MeasureTheory.FiniteMeasure.mass_nonzero_iff, Ne, one_smul, smul_eq_mul, not_false_iff, inv_mul_cancel₀
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
h :
  ∀ (s : Set Ω) (_s_mble : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((↑μ.normalize : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
      ((μ.mass⁻¹ • (↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (↑μ.normalize : Measure Ω) = μ.mass⁻¹ • (↑μ : Measure Ω)

Tactic:
ext1 s _s_mble
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
s : Set Ω
_s_mble : MeasurableSet s
h :
  HMul.hMul (β := ℝ≥0∞) (↑μ.mass⁻¹ : ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) =
    (μ.mass⁻¹ • (↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s
⊢ Eq (α := ℝ≥0∞) (((↑μ.normalize : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ.mass⁻¹ • (↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [← μ.normalize.ennreal_coeFn_eq_coeFn_toMeasure s, μ.normalize_eq_of_nonzero nonzero s,
    ENNReal.coe_mul, ennreal_coeFn_eq_coeFn_toMeasure]

Premises used: MeasureTheory.FiniteMeasure.normalize_eq_of_nonzero, MeasureTheory.ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasure, MeasureTheory.FiniteMeasure.ennreal_coeFn_eq_coeFn_toMeasure, ENNReal.coe_mul, MeasureTheory.FiniteMeasure.normalize
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
s : Set Ω
_s_mble : MeasurableSet s
⊢ HMul.hMul (β := ℝ≥0∞) (↑μ.mass⁻¹ : ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) =
    (μ.mass⁻¹ • (↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s

Tactic:
Measure.coe_nnreal_smul_apply _ _ _

Premises used: MeasureTheory.Measure.coe_nnreal_smul_apply
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
s : Set Ω
_s_mble : MeasurableSet s
⊢ HMul.hMul (β := ℝ≥0∞) (↑μ.mass⁻¹ : ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) =
    (μ.mass⁻¹ • (↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s

Tactic:
exact Measure.coe_nnreal_smul_apply _ _ _

Premises used: MeasureTheory.Measure.coe_nnreal_smul_apply
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
h :
  ∀ (s : Set Ω),
    MeasurableSet s →
      Eq (α := ℝ≥0) ((μ.toFiniteMeasure.normalize : (a : Set Ω) → ℝ≥0) s : ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s : ℝ≥0)
⊢ μ.toFiniteMeasure.normalize = μ

Tactic:
apply ProbabilityMeasure.eq_of_forall_apply_eq

Premises used: MeasureTheory.ProbabilityMeasure.eq_of_forall_apply_eq
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
s : Set Ω
_s_mble : MeasurableSet s
h :
  HMul.hMul (β := ℝ≥0) μ.toFiniteMeasure.mass⁻¹ ((μ.toFiniteMeasure : (a : Set Ω) → ℝ≥0) s : ℝ≥0) =
    (μ : (a : Set Ω) → ℝ≥0) s
⊢ Eq (α := ℝ≥0) ((μ.toFiniteMeasure.normalize : (a : Set Ω) → ℝ≥0) s : ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s : ℝ≥0)

Tactic:
rw [μ.toFiniteMeasure.normalize_eq_of_nonzero μ.toFiniteMeasure_nonzero s]

Premises used: MeasureTheory.ProbabilityMeasure.toFiniteMeasure_nonzero, MeasureTheory.FiniteMeasure.normalize_eq_of_nonzero, MeasureTheory.ProbabilityMeasure.toFiniteMeasure
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
s : Set Ω
_s_mble : MeasurableSet s
⊢ HMul.hMul (β := ℝ≥0) μ.toFiniteMeasure.mass⁻¹ ((μ.toFiniteMeasure : (a : Set Ω) → ℝ≥0) s : ℝ≥0) =
    (μ : (a : Set Ω) → ℝ≥0) s

Tactic:
simp only [ProbabilityMeasure.mass_toFiniteMeasure, inv_one, one_mul, μ.coeFn_toFiniteMeasure]

Premises used: MeasureTheory.ProbabilityMeasure.mass_toFiniteMeasure, inv_one, MeasureTheory.ProbabilityMeasure.coeFn_toFiniteMeasure, one_mul
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
nonzero : μ ≠ 0
f : Ω → E
rw :
  Eq.{u_2 + 1} (α := E)
    (∫ (x : Ω), f x ∂HSMul.hSMul (α := ℝ≥0∞) ((((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (↑μ : Measure Ω))
    (∫ (ω : Ω), f ω ∂μ.mass⁻¹ • (↑μ : Measure Ω))
⊢ average (↑μ : Measure Ω) f = ∫ (ω : Ω), f ω ∂(↑μ.normalize : Measure Ω)

Tactic:
rw [μ.toMeasure_normalize_eq_of_nonzero nonzero, average]

Premises used: MeasureTheory.average, MeasureTheory.FiniteMeasure.toMeasure_normalize_eq_of_nonzero
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
nonzero : μ ≠ 0
f : Ω → E
e_μ : (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)⁻¹ = (↑μ.mass⁻¹ : ℝ≥0∞)
⊢ Eq.{u_2 + 1} (α := E)
    (∫ (x : Ω), f x ∂HSMul.hSMul (α := ℝ≥0∞) ((((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (↑μ : Measure Ω))
    (∫ (ω : Ω), f ω ∂μ.mass⁻¹ • (↑μ : Measure Ω))

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
nonzero : μ ≠ 0
f : Ω → E
⊢ (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)⁻¹ = (↑μ.mass⁻¹ : ℝ≥0∞)

Tactic:
simp [ENNReal.coe_inv (μ.mass_nonzero_iff.mpr nonzero), ennreal_mass]

Premises used: Iff.mpr, ENNReal.coe_inv, MeasureTheory.FiniteMeasure.mass_nonzero_iff, MeasureTheory.FiniteMeasure.ennreal_mass
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst_1 : TopologicalSpace Ω
f : Ω →ᵇ ℝ≥0
nth_rw : (μ.mass • μ.normalize.toFiniteMeasure).testAgainstNN f = μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f
⊢ μ.testAgainstNN f = μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f

Tactic:
nth_rw 1 [μ.self_eq_mass_smul_normalize]

Premises used: MeasureTheory.FiniteMeasure.self_eq_mass_smul_normalize
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
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
rw₁ rw₂ : μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f = μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f
⊢ (μ.mass • μ.normalize.toFiniteMeasure).testAgainstNN f = μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f

Tactic:
rw [μ.normalize.toFiniteMeasure.smul_testAgainstNN_apply μ.mass f, smul_eq_mul]

Premises used: MeasureTheory.FiniteMeasure.mass, MeasureTheory.FiniteMeasure.smul_testAgainstNN_apply, MeasureTheory.ProbabilityMeasure.toFiniteMeasure, smul_eq_mul, MeasureTheory.FiniteMeasure.normalize
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst_1 : TopologicalSpace Ω
nonzero : μ ≠ 0
f : Ω →ᵇ ℝ≥0
⊢ μ.normalize.toFiniteMeasure.testAgainstNN f = μ.mass⁻¹ * μ.testAgainstNN f

Tactic:
simp [μ.testAgainstNN_eq_mass_mul, inv_mul_cancel_left₀ <| μ.mass_nonzero_iff.mpr nonzero]

Premises used: Iff.mpr, MeasureTheory.FiniteMeasure.mass_nonzero_iff, MeasureTheory.FiniteMeasure.testAgainstNN_eq_mass_mul, inv_mul_cancel_left₀
-- 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
pos : ∀ (h_mass : μ.mass = 0), Tendsto (fun (i : γ) ↦ (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))
neg : ∀ (h_mass : ¬μ.mass = 0), Tendsto (fun (i : γ) ↦ (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))
⊢ Tendsto (fun (i : γ) ↦ (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))

Tactic:
by_cases h_mass : μ.mass = 0

Premises used: MeasureTheory.FiniteMeasure.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
h_mass : μ.mass = 0
pos :
  ∀ (mass_lim : Tendsto (β := ℝ≥0) (fun (i : γ) ↦ (μs i).mass) F (𝓝 0)),
    Tendsto (β := ℝ≥0) (fun (i : γ) ↦ (μs i).testAgainstNN f) F (𝓝 0)
⊢ Tendsto (fun (i : γ) ↦ (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))

Tactic:
simp only [μ.mass_zero_iff.mp h_mass, zero_testAgainstNN_apply, zero_mass] at mass_lim ⊢

Premises used: MeasureTheory.FiniteMeasure.zero_testAgainstNN_apply, MeasureTheory.FiniteMeasure.zero_mass, Iff.mp, MeasureTheory.FiniteMeasure.mass_zero_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 (fun (i : γ) ↦ (μs i).normalize) F (𝓝 μ.normalize)
f : Ω →ᵇ ℝ≥0
h_mass : μ.mass = 0
mass_lim : Tendsto (β := ℝ≥0) (fun (i : γ) ↦ (μs i).mass) F (𝓝 0)
⊢ Tendsto (β := ℝ≥0) (fun (i : γ) ↦ (μs i).testAgainstNN f) F (𝓝 0)

Tactic:
tendsto_zero_testAgainstNN_of_tendsto_zero_mass mass_lim f

Premises used: MeasureTheory.FiniteMeasure.tendsto_zero_testAgainstNN_of_tendsto_zero_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)
f : Ω →ᵇ ℝ≥0
h_mass : μ.mass = 0
mass_lim : Tendsto (β := ℝ≥0) (fun (i : γ) ↦ (μs i).mass) F (𝓝 0)
⊢ Tendsto (β := ℝ≥0) (fun (i : γ) ↦ (μs i).testAgainstNN f) F (𝓝 0)

Tactic:
exact tendsto_zero_testAgainstNN_of_tendsto_zero_mass mass_lim f

Premises used: MeasureTheory.FiniteMeasure.tendsto_zero_testAgainstNN_of_tendsto_zero_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
h_mass : ¬μ.mass = 0
neg :
  Tendsto (fun (i : γ) ↦ (μs i).mass * (μs i).normalize.toFiniteMeasure.testAgainstNN f) F
    (𝓝 (μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f))
⊢ Tendsto (fun (i : γ) ↦ (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))

Tactic:
simp_rw [fun i ↦ (μs i).testAgainstNN_eq_mass_mul f, μ.testAgainstNN_eq_mass_mul f]

Premises used: MeasureTheory.FiniteMeasure.testAgainstNN_eq_mass_mul
-- 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
h_mass : ¬μ.mass = 0
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))
⊢ 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

Premises used: MeasureTheory.ProbabilityMeasure.tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds