awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ν : ProbabilityMeasure Ω
s : Set Ω
rw : (↑((ν.toFiniteMeasure : (a : Set Ω) → ℝ≥0) s) : ℝ≥0∞) = ((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s
⊢ (↑((ν : (a : Set Ω) → ℝ≥0) s) : ℝ≥0∞) = ((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s
have rw₁ : Eq (α := ℝ≥0∞) (((↑ν.toFiniteMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
  (((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← coeFn_comp_toFiniteMeasure_eq_coeFn, FiniteMeasure.ennreal_coeFn_eq_coeFn_toMeasure,
    toMeasure_comp_toFiniteMeasure_eq_toMeasure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ν : ProbabilityMeasure Ω
s : Set Ω
rw : (↑((ν.toFiniteMeasure : (a : Set Ω) → ℝ≥0) s) : ℝ≥0∞) = ((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s
rw₁ :
  Eq (α := ℝ≥0∞) (((↑ν.toFiniteMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
    (((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (↑((ν : (a : Set Ω) → ℝ≥0) s) : ℝ≥0∞) = ((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s
have rw₂ : Eq (α := ℝ≥0∞) (((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← coeFn_comp_toFiniteMeasure_eq_coeFn, FiniteMeasure.ennreal_coeFn_eq_coeFn_toMeasure,
    toMeasure_comp_toFiniteMeasure_eq_toMeasure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ν : ProbabilityMeasure Ω
s : Set Ω
h : Eq (α := ℝ≥0) ((ν : (a : Set Ω) → ℝ≥0) s : ℝ≥0) (0 : ℝ≥0)
⊢ Eq (α := ℝ≥0∞) (((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : (↑((ν : (a : Set Ω) → ℝ≥0) s) : ℝ≥0∞) = 0
Tactic: rw [← ennreal_coeFn_eq_coeFn_toMeasure, h, ENNReal.coe_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ν : ProbabilityMeasure Ω
s : Set Ω
h : Eq (α := ℝ≥0) ((ν : (a : Set Ω) → ℝ≥0) s : ℝ≥0) (0 : ℝ≥0)
rw : (↑((ν : (a : Set Ω) → ℝ≥0) s) : ℝ≥0∞) = 0
⊢ Eq (α := ℝ≥0∞) (((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rw₁ : (↑0 : ℝ≥0∞) = 0
Tactic: rw [← ennreal_coeFn_eq_coeFn_toMeasure, h, ENNReal.coe_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ν : ProbabilityMeasure Ω
s : Set Ω
h : Eq (α := ℝ≥0) ((ν : (a : Set Ω) → ℝ≥0) s : ℝ≥0) (0 : ℝ≥0)
rw : (↑((ν : (a : Set Ω) → ℝ≥0) s) : ℝ≥0∞) = 0
rw₁ : (↑0 : ℝ≥0∞) = 0
⊢ Eq (α := ℝ≥0∞) (((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [← ennreal_coeFn_eq_coeFn_toMeasure, h, ENNReal.coe_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
s₁ s₂ : Set Ω
h : s₁ ⊆ s₂
⊢ LE.le (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s₁ : ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s₂ : ℝ≥0)
have rw : LE.le (α := ℝ≥0) ((μ.toFiniteMeasure : (a : Set Ω) → ℝ≥0) s₁ : ℝ≥0) ((μ.toFiniteMeasure : (a : Set Ω) → ℝ≥0) s₂ : ℝ≥0)
Tactic: rw [← coeFn_comp_toFiniteMeasure_eq_coeFn]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
s₁ s₂ : Set Ω
⊢ (μ : (a : Set Ω) → ℝ≥0) (s₁ ∪ s₂) ≤
    HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s₁ : ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s₂ : ℝ≥0)
have rw : (μ.toFiniteMeasure : (a : Set Ω) → ℝ≥0) (s₁ ∪ s₂) ≤
  HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((μ.toFiniteMeasure : (a : Set Ω) → ℝ≥0) s₁ : ℝ≥0)
    ((μ.toFiniteMeasure : (a : Set Ω) → ℝ≥0) s₂ : ℝ≥0)
Tactic: rw [← coeFn_comp_toFiniteMeasure_eq_coeFn]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ ν : ProbabilityMeasure Ω
h :
  ∀ (s : Set Ω),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
        (((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ = ν
have a : (↑μ : Measure Ω) = (↑ν : Measure Ω)
Tactic: apply toMeasure_injective
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ ν : ProbabilityMeasure Ω
h : ∀ (s : Set Ω), MeasurableSet s → Eq (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s : ℝ≥0) ((ν : (a : Set Ω) → ℝ≥0) s : ℝ≥0)
⊢ μ = ν
have h₁ : ∀ (s : Set Ω) (s_mble : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext1 s s_mble
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
⊢ Eq.{u_1 + 1} (α := Set (FiniteMeasure Ω)) (range toFiniteMeasure) {μ : FiniteMeasure Ω | μ.mass = 1}
have h : ∀ (μ : FiniteMeasure Ω),
  Membership.mem (γ := Set (FiniteMeasure Ω)) (range toFiniteMeasure) μ ↔
    Membership.mem (γ := Set (FiniteMeasure Ω)) {μ : FiniteMeasure Ω | μ.mass = 1} μ
Tactic: ext μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
⊢ (∃ (y : ProbabilityMeasure Ω), y.toFiniteMeasure = μ) ↔ μ.mass = 1
have h : ∀ (h : μ.mass = 1), ∃ (y : ProbabilityMeasure Ω), y.toFiniteMeasure = μ
Tactic: refine ⟨fun ⟨ν, hν⟩ ↦ by simp [← hν], fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
h : μ.mass = 1
⊢ ∃ (y : ProbabilityMeasure Ω), y.toFiniteMeasure = μ
have h₁ : toFiniteMeasure (Subtype.mk (p := fun (μ : Measure Ω) ↦ IsProbabilityMeasure μ) (↑μ : Measure Ω) sorry) = μ
Tactic: refine ⟨⟨μ, isProbabilityMeasure_iff_real.2 (by simpa using h)⟩, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
h : μ.mass = 1
⊢ toFiniteMeasure (Subtype.mk (p := fun (μ : Measure Ω) ↦ IsProbabilityMeasure μ) (↑μ : Measure Ω) ⋯) = μ
have h₁ : ∀ (s : Set Ω) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞)
    (((↑(toFiniteMeasure (Subtype.mk (p := fun (μ : Measure Ω) ↦ IsProbabilityMeasure μ) (↑μ : Measure Ω) sorry)) :
            Measure Ω) :
          (a : Set Ω) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
this :
  Eq.{u_1 + 1} (α := Set (Measure Ω)) {μ : Measure Ω | IsProbabilityMeasure μ}
    (preimage (β := ℝ≥0∞) (fun (μ : Measure Ω) ↦ (μ : (a : Set Ω) → ℝ≥0∞) univ) {1})
⊢ MeasurableSet.{u_1} (α := Measure Ω) {μ : Measure Ω | IsProbabilityMeasure μ}
have rw : MeasurableSet.{u_1} (α := Measure Ω) (preimage (β := ℝ≥0∞) (fun (μ : Measure Ω) ↦ (μ : (a : Set Ω) → ℝ≥0∞) univ) {1})
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
⊢ MeasurableSet.{u_1} (α := Measure Ω) {μ : Measure Ω | IsProbabilityMeasure μ}
have suffices : Eq.{u_1 + 1} (α := Set (Measure Ω)) {μ : Measure Ω | IsProbabilityMeasure μ}
  (preimage (β := ℝ≥0∞) (fun (μ : Measure Ω) ↦ (μ : (a : Set Ω) → ℝ≥0∞) univ) {1})
Tactic: suffices { μ : Measure Ω | IsProbabilityMeasure μ } = (fun μ => μ univ) ⁻¹' {1} by
    rw [this]
    exact Measure.measurable_coe MeasurableSet.univ (measurableSet_singleton 1)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
⊢ Eq.{u_1 + 1} (α := Set (Measure Ω)) {μ : Measure Ω | IsProbabilityMeasure μ}
    (preimage (β := ℝ≥0∞) (fun (μ : Measure Ω) ↦ (μ : (a : Set Ω) → ℝ≥0∞) univ) {1})
have h : ∀ (x : Measure Ω),
  Membership.mem (γ := Set (Measure Ω)) {μ : Measure Ω | IsProbabilityMeasure μ} x ↔
    Membership.mem (γ := Set (Measure Ω))
      (preimage (β := ℝ≥0∞) (fun (μ : Measure Ω) ↦ (μ : (a : Set Ω) → ℝ≥0∞) univ) {1}) x
Tactic: ext _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
⊢ Measurable (β := Measure (α × β)) fun (μ : Prod.{u_2, u_3} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦
    (↑μ.1 : Measure α).prod (↑μ.2 : Measure β)
have apply : ∀ (s : Set (α × β)),
  Membership.mem (γ := Set (Set (α × β)))
      (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s} {t : Set β | MeasurableSet t})
      s →
    Measurable (β := ℝ≥0∞) fun (a : Prod.{u_2, u_3} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦
      ((↑a.1 : Measure α).prod (↑a.2 : Measure β) : (a : Set (α × β)) → ℝ≥0∞) s
Tactic: apply Measurable.measure_of_isPiSystem_of_isProbabilityMeasure generateFrom_prod.symm
    isPiSystem_prod _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
⊢ ∀ (s : Set (α × β)),
    Membership.mem (γ := Set (Set (α × β)))
        (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s} {t : Set β | MeasurableSet t})
        s →
      Measurable (β := ℝ≥0∞) fun (a : Prod.{u_2, u_3} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦
        ((↑a.1 : Measure α).prod (↑a.2 : Measure β) : (a : Set (α × β)) → ℝ≥0∞) s
have simp : ∀ (s : Set (α × β)) (x : Set α),
  MeasurableSet x →
    ∀ (x_1 : Set β),
      MeasurableSet x_1 →
        x ×ˢ x_1 = s →
          Measurable (β := ℝ≥0∞) fun (a : Prod.{u_2, u_3} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦
            ((↑a.1 : Measure α).prod (↑a.2 : Measure β) : (a : Set (α × β)) → ℝ≥0∞) s
Tactic: simp only [mem_image2, mem_setOf_eq, forall_exists_index, and_imp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
s : Set (α × β)
u : Set α
Hu : MeasurableSet u
v : Set β
Hv : MeasurableSet v
Heq : u ×ˢ v = s
⊢ Measurable (β := ℝ≥0∞) fun (a : Prod.{u_2, u_3} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦
    ((↑a.1 : Measure α).prod (↑a.2 : Measure β) : (a : Set (α × β)) → ℝ≥0∞) s
have simp_rw : Measurable (β := ℝ≥0∞) fun (a : Prod.{u_2, u_3} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑a.1 : Measure α) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
    (((↑a.2 : Measure β) : (a : Set β) → ℝ≥0∞) v : ℝ≥0∞)
Tactic: simp_rw [← Heq, Measure.prod_prod]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
s : Set (α × β)
u : Set α
Hu : MeasurableSet u
v : Set β
Hv : MeasurableSet v
Heq : u ×ˢ v = s
⊢ Measurable (β := ℝ≥0∞) fun (a : Prod.{u_2, u_3} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑a.1 : Measure α) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
      (((↑a.2 : Measure β) : (a : Set β) → ℝ≥0∞) v : ℝ≥0∞)
have hf : Measurable (β := ℝ≥0∞) fun (a : Prod.{u_2, u_3} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦
  ((↑a.1 : Measure α) : (a : Set α) → ℝ≥0∞) u
Tactic: apply Measurable.mul
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
s : Set (α × β)
u : Set α
Hu : MeasurableSet u
v : Set β
Hv : MeasurableSet v
Heq : u ×ˢ v = s
hf :
  Measurable (β := ℝ≥0∞) fun (a : Prod.{u_2, u_3} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦
    ((↑a.1 : Measure α) : (a : Set α) → ℝ≥0∞) u
⊢ Measurable (β := ℝ≥0∞) fun (a : Prod.{u_2, u_3} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑a.1 : Measure α) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
      (((↑a.2 : Measure β) : (a : Set β) → ℝ≥0∞) v : ℝ≥0∞)
have hg : Measurable (β := ℝ≥0∞) fun (a : Prod.{u_2, u_3} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦
  ((↑a.2 : Measure β) : (a : Set β) → ℝ≥0∞) v
Tactic: apply Measurable.mul
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
⊢ Tendsto μs F (𝓝 μ) ↔
    ∀ (f : Ω →ᵇ ℝ≥0),
      Tendsto (fun (i : γ) ↦ ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
        (𝓝 (∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)))
have rw : Tendsto (toFiniteMeasure ∘ μs) F (𝓝 μ.toFiniteMeasure) ↔
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : γ) ↦ ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)))
Tactic: rw [tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
zero : ¬μ.mass = 0
⊢ IsProbabilityMeasure (μ.mass⁻¹ • (↑μ : Measure Ω))
have refine : Eq (α := ℝ≥0∞) ((μ.mass⁻¹ • (↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: refine ⟨?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
zero : ¬μ.mass = 0
⊢ Eq (α := ℝ≥0∞) ((μ.mass⁻¹ • (↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
have simp : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞)
    (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) =
  1
Tactic: simp only [Measure.coe_smul, Pi.smul_apply, Measure.nnreal_smul_coe_apply,
          ENNReal.coe_inv zero, ennreal_mass]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (hypothesis)
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
zero : ¬μ.mass = 0
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞)
      (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) =
    1
have zero₁ : Ne (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← Ne, ← ENNReal.coe_ne_zero, ennreal_mass] at zero
Cleared hypotheses: zero
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
s : Set Ω
⊢ (μ : (a : Set Ω) → ℝ≥0) s = HMul.hMul (β := ℝ≥0) μ.mass ((μ.normalize : (a : Set Ω) → ℝ≥0) s : ℝ≥0)
have inl : ((0 : FiniteMeasure Ω) : (a : Set Ω) → ℝ≥0) s =
  HMul.hMul (β := ℝ≥0) (mass.{u_1} (Ω := Ω) 0) (((normalize 0 : ProbabilityMeasure Ω) : (a : Set Ω) → ℝ≥0) s : ℝ≥0)
Tactic: obtain rfl | h := eq_or_ne μ 0
Cleared hypotheses: μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
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)
⊢ (μ : (a : Set Ω) → ℝ≥0) s = HMul.hMul (β := ℝ≥0) μ.mass ((μ.normalize : (a : Set Ω) → ℝ≥0) s : ℝ≥0)
have inr : ∀ (h : μ ≠ 0), (μ : (a : Set Ω) → ℝ≥0) s = HMul.hMul (β := ℝ≥0) μ.mass ((μ.normalize : (a : Set Ω) → ℝ≥0) s : ℝ≥0)
Tactic: obtain rfl | h := eq_or_ne μ 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (hypothesis)
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
s : Set Ω
h : μ ≠ 0
⊢ (μ : (a : Set Ω) → ℝ≥0) s = HMul.hMul (β := ℝ≥0) μ.mass ((μ.normalize : (a : Set Ω) → ℝ≥0) s : ℝ≥0)
have mass_nonzero : μ.mass ≠ 0
Tactic: have mass_nonzero : μ.mass ≠ 0 := by rwa [μ.mass_nonzero_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
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 ((μ.normalize : (a : Set Ω) → ℝ≥0) s : ℝ≥0)
have inr : (μ : (a : Set Ω) → ℝ≥0) s =
  HMul.hMul (β := ℝ≥0) μ.mass
    ((Subtype.mk (p := fun (μ : Measure Ω) ↦ IsProbabilityMeasure μ) (μ.mass⁻¹ • (↑μ : Measure Ω)) sorry :
          (a : Set Ω) → ℝ≥0)
        s :
      ℝ≥0)
Tactic: simp only [normalize, dif_neg mass_nonzero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
⊢ μ = μ.mass • μ.normalize.toFiniteMeasure
have h : ∀ (s : Set Ω),
  MeasurableSet s →
    Eq (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s : ℝ≥0) ((μ.mass • μ.normalize.toFiniteMeasure : (a : Set Ω) → ℝ≥0) s : ℝ≥0)
Tactic: apply eq_of_forall_apply_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
s : Set Ω
_s_mble : MeasurableSet s
⊢ Eq (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s : ℝ≥0) ((μ.mass • μ.normalize.toFiniteMeasure : (a : Set Ω) → ℝ≥0) s : ℝ≥0)
have h : HMul.hMul (β := ℝ≥0) μ.mass ((μ.normalize : (a : Set Ω) → ℝ≥0) s : ℝ≥0) =
  (μ.mass • μ.normalize.toFiniteMeasure : (a : Set Ω) → ℝ≥0) s
Tactic: rw [μ.self_eq_mass_mul_normalize s, smul_apply, smul_eq_mul,
    ProbabilityMeasure.coeFn_comp_toFiniteMeasure_eq_coeFn]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
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
⊢ Eq (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s : ℝ≥0) ((μ.mass • μ.normalize.toFiniteMeasure : (a : Set Ω) → ℝ≥0) s : ℝ≥0)
have h₁ : HMul.hMul (β := ℝ≥0) μ.mass ((μ.normalize : (a : Set Ω) → ℝ≥0) s : ℝ≥0) =
  HSMul.hSMul (β := ℝ≥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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
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)
⊢ Eq (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s : ℝ≥0) ((μ.mass • μ.normalize.toFiniteMeasure : (a : Set Ω) → ℝ≥0) s : ℝ≥0)
have h₂ : HMul.hMul (β := ℝ≥0) μ.mass ((μ.normalize : (a : Set Ω) → ℝ≥0) s : ℝ≥0) =
  HMul.hMul (β := ℝ≥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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
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)
⊢ Eq (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s : ℝ≥0) ((μ.mass • μ.normalize.toFiniteMeasure : (a : Set Ω) → ℝ≥0) s : ℝ≥0)
have h₃ : HMul.hMul (β := ℝ≥0) μ.mass ((μ.normalize : (a : Set Ω) → ℝ≥0) s : ℝ≥0) =
  HMul.hMul (β := ℝ≥0) μ.mass ((μ.normalize : (a : Set Ω) → ℝ≥0) s : ℝ≥0)
Tactic: rw [μ.self_eq_mass_mul_normalize s, smul_apply, smul_eq_mul,
    ProbabilityMeasure.coeFn_comp_toFiniteMeasure_eq_coeFn]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
⊢ μ.normalize.toFiniteMeasure = μ.mass⁻¹ • μ
have nth_rw : μ.normalize.toFiniteMeasure = μ.mass⁻¹ • μ.mass • μ.normalize.toFiniteMeasure
Tactic: nth_rw 3 [μ.self_eq_mass_smul_normalize]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
⊢ μ.normalize.toFiniteMeasure = μ.mass⁻¹ • μ.mass • μ.normalize.toFiniteMeasure
have rw : μ.normalize.toFiniteMeasure = (μ.mass⁻¹ • μ.mass) • μ.normalize.toFiniteMeasure
Tactic: rw [← smul_assoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
⊢ (↑μ.normalize : Measure Ω) = μ.mass⁻¹ • (↑μ : Measure Ω)
have h : ∀ (s : Set Ω) (_s_mble : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((↑μ.normalize : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ.mass⁻¹ • (↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext1 s _s_mble
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
s : Set Ω
_s_mble : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((↑μ.normalize : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ.mass⁻¹ • (↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
have h : HMul.hMul (β := ℝ≥0∞) (↑μ.mass⁻¹ : ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) =
  (μ.mass⁻¹ • (↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s
Tactic: rw [← μ.normalize.ennreal_coeFn_eq_coeFn_toMeasure s, μ.normalize_eq_of_nonzero nonzero s,
    ENNReal.coe_mul, ennreal_coeFn_eq_coeFn_toMeasure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
⊢ μ.toFiniteMeasure.normalize = μ
have h : ∀ (s : Set Ω),
  MeasurableSet s →
    Eq (α := ℝ≥0) ((μ.toFiniteMeasure.normalize : (a : Set Ω) → ℝ≥0) s : ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s : ℝ≥0)
Tactic: apply ProbabilityMeasure.eq_of_forall_apply_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
s : Set Ω
_s_mble : MeasurableSet s
⊢ Eq (α := ℝ≥0) ((μ.toFiniteMeasure.normalize : (a : Set Ω) → ℝ≥0) s : ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s : ℝ≥0)
have h : HMul.hMul (β := ℝ≥0) μ.toFiniteMeasure.mass⁻¹ ((μ.toFiniteMeasure : (a : Set Ω) → ℝ≥0) s : ℝ≥0) =
  (μ : (a : Set Ω) → ℝ≥0) s
Tactic: rw [μ.toFiniteMeasure.normalize_eq_of_nonzero μ.toFiniteMeasure_nonzero s]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
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
⊢ average (↑μ : Measure Ω) f = ∫ (ω : Ω), f ω ∂(↑μ.normalize : Measure Ω)
have rw : Eq.{u_2 + 1} (α := E)
  (∫ (x : Ω), f x ∂HSMul.hSMul (α := ℝ≥0∞) ((((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (↑μ : Measure Ω))
  (∫ (ω : Ω), f ω ∂μ.mass⁻¹ • (↑μ : Measure Ω))
Tactic: rw [μ.toMeasure_normalize_eq_of_nonzero nonzero, average]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
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
⊢ Eq.{u_2 + 1} (α := E)
    (∫ (x : Ω), f x ∂HSMul.hSMul (α := ℝ≥0∞) ((((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (↑μ : Measure Ω))
    (∫ (ω : Ω), f ω ∂μ.mass⁻¹ • (↑μ : Measure Ω))
have e_μ : (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)⁻¹ = (↑μ.mass⁻¹ : ℝ≥0∞)
Tactic: congr