awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hnt : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hu : IsUniform X s ℙ μ
this : X ⁻¹' Set.univ = Set.univ
⊢ Eq (α := ℝ≥0∞) ((ℙ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((ℙ : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' Set.univ) : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: rw [← this, hu.measure_preimage hns hnt MeasurableSet.univ, Set.inter_univ,
      ENNReal.div_self hns hnt]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hnt : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hu : IsUniform X s ℙ μ
this : X ⁻¹' Set.univ = Set.univ
rw : Eq (α := ℝ≥0∞) ((ℙ : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' Set.univ) : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ℙ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
have rw₁ : HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ Set.univ) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) =
  1
Tactic: rw [← this, hu.measure_preimage hns hnt MeasurableSet.univ, Set.inter_univ,
      ENNReal.div_self hns hnt]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hnt : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hu : IsUniform X s ℙ μ
this : X ⁻¹' Set.univ = Set.univ
rw : Eq (α := ℝ≥0∞) ((ℙ : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' Set.univ) : ℝ≥0∞) (1 : ℝ≥0∞)
rw₁ :
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ Set.univ) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) =
    1
⊢ Eq (α := ℝ≥0∞) ((ℙ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
have rw₂ : HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) = 1
Tactic: rw [← this, hu.measure_preimage hns hnt MeasurableSet.univ, Set.inter_univ,
      ENNReal.div_self hns hnt]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hnt : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hu : IsUniform X s ℙ μ
this : X ⁻¹' Set.univ = Set.univ
rw : Eq (α := ℝ≥0∞) ((ℙ : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' Set.univ) : ℝ≥0∞) (1 : ℝ≥0∞)
rw₁ :
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ Set.univ) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) =
    1
rw₂ : HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) = 1
⊢ Eq (α := ℝ≥0∞) ((ℙ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
have rw₃ : Eq (α := ℝ≥0∞) 1 1
Tactic: rw [← this, hu.measure_preimage hns hnt MeasurableSet.univ, Set.inter_univ,
      ENNReal.div_self hns hnt]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
⊢ Measure.map X ℙ = μ[|toMeasurable μ s] ↔ Measure.map X ℙ = μ[|s]
have rw : Measure.map X ℙ = μ[|s] ↔ Measure.map X ℙ = μ[|s]
Tactic: rw [ProbabilityTheory.cond_toMeasurable_eq]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hnt : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hu : IsUniform X s ℙ μ
t : Set E := toMeasurable μ s
⊢ HasPDF X ℙ μ
have apply : Measure.map X ℙ =
  μ.withDensity (t.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞) 1))
Tactic: apply hasPDF_of_map_eq_withDensity (hu.aemeasurable hns hnt) (t.indicator ((μ t)⁻¹ • 1)) <|
    (measurable_one.aemeasurable.const_smul (μ t)⁻¹).indicator (measurableSet_toMeasurable μ s)
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hnt : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hu : IsUniform X s ℙ μ
t : Set E := toMeasurable μ s
⊢ Measure.map X ℙ =
    μ.withDensity (t.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞) 1))
have rw : μ[|s] = μ.withDensity (t.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞) 1))
Tactic: rw [hu, withDensity_indicator (measurableSet_toMeasurable μ s), withDensity_smul _ measurable_one,
    withDensity_one, restrict_toMeasurable hnt, measure_toMeasurable, ProbabilityTheory.cond]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hnt : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hu : IsUniform X s ℙ μ
t : Set E := toMeasurable μ s
rw :
  μ[|s] =
    μ.withDensity (t.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞) 1))
⊢ Measure.map X ℙ =
    μ.withDensity (t.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞) 1))
have rw₁ : μ[|s] =
  (μ.restrict (toMeasurable μ s)).withDensity
    (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞) 1)
Tactic: rw [hu, withDensity_indicator (measurableSet_toMeasurable μ s), withDensity_smul _ measurable_one,
    withDensity_one, restrict_toMeasurable hnt, measure_toMeasurable, ProbabilityTheory.cond]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hnt : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hu : IsUniform X s ℙ μ
t : Set E := toMeasurable μ s
rw :
  μ[|s] =
    μ.withDensity (t.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞) 1))
rw₁ :
  μ[|s] =
    (μ.restrict (toMeasurable μ s)).withDensity
      (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞) 1)
⊢ Measure.map X ℙ =
    μ.withDensity (t.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞) 1))
have rw₂ : μ[|s] = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞) ((μ.restrict (toMeasurable μ s)).withDensity 1)
Tactic: rw [hu, withDensity_indicator (measurableSet_toMeasurable μ s), withDensity_smul _ measurable_one,
    withDensity_one, restrict_toMeasurable hnt, measure_toMeasurable, ProbabilityTheory.cond]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hnt : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hu : IsUniform X s ℙ μ
t : Set E := toMeasurable μ s
rw :
  μ[|s] =
    μ.withDensity (t.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞) 1))
rw₁ :
  μ[|s] =
    (μ.restrict (toMeasurable μ s)).withDensity
      (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞) 1)
rw₂ :
  μ[|s] =
    HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞) ((μ.restrict (toMeasurable μ s)).withDensity 1)
⊢ Measure.map X ℙ =
    μ.withDensity (t.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞) 1))
have rw₃ : μ[|s] = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞) (μ.restrict (toMeasurable μ s))
Tactic: rw [hu, withDensity_indicator (measurableSet_toMeasurable μ s), withDensity_smul _ measurable_one,
    withDensity_one, restrict_toMeasurable hnt, measure_toMeasurable, ProbabilityTheory.cond]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hnt : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hu : IsUniform X s ℙ μ
t : Set E := toMeasurable μ s
rw :
  μ[|s] =
    μ.withDensity (t.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞) 1))
rw₁ :
  μ[|s] =
    (μ.restrict (toMeasurable μ s)).withDensity
      (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞) 1)
rw₂ :
  μ[|s] =
    HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞) ((μ.restrict (toMeasurable μ s)).withDensity 1)
rw₃ : μ[|s] = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞) (μ.restrict (toMeasurable μ s))
⊢ Measure.map X ℙ =
    μ.withDensity (t.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞) 1))
have rw₄ : μ[|s] = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞) (μ.restrict s)
Tactic: rw [hu, withDensity_indicator (measurableSet_toMeasurable μ s), withDensity_smul _ measurable_one,
    withDensity_one, restrict_toMeasurable hnt, measure_toMeasurable, ProbabilityTheory.cond]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hnt : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hu : IsUniform X s ℙ μ
t : Set E := toMeasurable μ s
rw :
  μ[|s] =
    μ.withDensity (t.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞) 1))
rw₁ :
  μ[|s] =
    (μ.restrict (toMeasurable μ s)).withDensity
      (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞) 1)
rw₂ :
  μ[|s] =
    HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞) ((μ.restrict (toMeasurable μ s)).withDensity 1)
rw₃ : μ[|s] = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞) (μ.restrict (toMeasurable μ s))
rw₄ : μ[|s] = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞) (μ.restrict s)
⊢ Measure.map X ℙ =
    μ.withDensity (t.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞) 1))
have rw₅ : μ[|s] = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s)
Tactic: rw [hu, withDensity_indicator (measurableSet_toMeasurable μ s), withDensity_smul _ measurable_one,
    withDensity_one, restrict_toMeasurable hnt, measure_toMeasurable, ProbabilityTheory.cond]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hnt : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hu : IsUniform X s ℙ μ
t : Set E := toMeasurable μ s
rw :
  μ[|s] =
    μ.withDensity (t.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞) 1))
rw₁ :
  μ[|s] =
    (μ.restrict (toMeasurable μ s)).withDensity
      (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞) 1)
rw₂ :
  μ[|s] =
    HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞) ((μ.restrict (toMeasurable μ s)).withDensity 1)
rw₃ : μ[|s] = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞) (μ.restrict (toMeasurable μ s))
rw₄ : μ[|s] = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞) (μ.restrict s)
rw₅ : μ[|s] = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s)
⊢ Measure.map X ℙ =
    μ.withDensity (t.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞) 1))
have rw₆ : HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s) =
  HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s)
Tactic: rw [hu, withDensity_indicator (measurableSet_toMeasurable μ s), withDensity_smul _ measurable_one,
    withDensity_one, restrict_toMeasurable hnt, measure_toMeasurable, ProbabilityTheory.cond]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hu : IsUniform X s ℙ μ
hμs :
  Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ pdf X ℙ μ =ᶠ[ae μ] 0
have inl : ∀ (H : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), pdf X ℙ μ =ᶠ[ae μ] 0
Tactic: rcases hμs with H | H
Cleared hypotheses: hμs
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hu : IsUniform X s ℙ μ
hμs :
  Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
inl : ∀ (H : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), pdf X ℙ μ =ᶠ[ae μ] 0
⊢ pdf X ℙ μ =ᶠ[ae μ] 0
have inr : ∀ (H : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)), pdf X ℙ μ =ᶠ[ae μ] 0
Tactic: rcases hμs with H | H
Cleared hypotheses: hμs
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (hypothesis)
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hu : IsUniform X s ℙ μ
H : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ pdf X ℙ μ =ᶠ[ae μ] 0
have hu₁ : Eq (α := Measure E) (Measure.map X ℙ) 0
Tactic: simp only [IsUniform, ProbabilityTheory.cond, H, ENNReal.inv_zero, restrict_eq_zero.mpr H,
    smul_zero] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (hypothesis)
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hu : IsUniform X s ℙ μ
H : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ pdf X ℙ μ =ᶠ[ae μ] 0
have hu₁ : Eq (α := Measure E) (Measure.map X ℙ) 0
Tactic: simp only [IsUniform, ProbabilityTheory.cond, H, ENNReal.inv_top, zero_smul] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hms : MeasurableSet s
hu : IsUniform X s ℙ μ
⊢ pdf X ℙ μ =ᶠ[ae μ] s.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1)
have pos : ∀ (hnt : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  pdf X ℙ μ =ᶠ[ae μ] s.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1)
Tactic: by_cases hnt : μ s = ∞
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hms : MeasurableSet s
hu : IsUniform X s ℙ μ
pos :
  ∀ (hnt : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    pdf X ℙ μ =ᶠ[ae μ] s.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1)
⊢ pdf X ℙ μ =ᶠ[ae μ] s.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1)
have neg : ∀ (hnt : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  pdf X ℙ μ =ᶠ[ae μ] s.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1)
Tactic: by_cases hnt : μ s = ∞
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hms : MeasurableSet s
hu : IsUniform X s ℙ μ
hnt : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ pdf X ℙ μ =ᶠ[ae μ] s.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1)
have pos : ∀ (hns : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  pdf X ℙ μ =ᶠ[ae μ] s.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1)
Tactic: by_cases hns : μ s = 0
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hms : MeasurableSet s
hu : IsUniform X s ℙ μ
hnt : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
pos :
  ∀ (hns : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    pdf X ℙ μ =ᶠ[ae μ] s.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1)
⊢ pdf X ℙ μ =ᶠ[ae μ] s.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1)
have neg : ∀ (hns : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  pdf X ℙ μ =ᶠ[ae μ] s.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1)
Tactic: by_cases hns : μ s = 0
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hms : MeasurableSet s
hu : IsUniform X s ℙ μ
hnt : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hns : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ pdf X ℙ μ =ᶠ[ae μ] s.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1)
have h : ∀ (x_1 : E) (hx : x_1 ∉ s) (h'x : pdf X ℙ μ x_1 = 0 x_1),
  pdf X ℙ μ x_1 = s.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1) x_1
Tactic: filter_upwards [measure_eq_zero_iff_ae_notMem.mp hns,
      pdf_eq_zero_of_measure_eq_zero_or_top hu (Or.inl hns)] with x hx h'x
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (hypothesis)
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hms : MeasurableSet s
hu : IsUniform X s ℙ μ
hnt : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hns : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ pdf X ℙ μ =ᶠ[ae μ] s.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1)
have this : HasPDF X ℙ μ
Tactic: have : HasPDF X ℙ μ := hasPDF hns hnt hu
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (hypothesis)
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hms : MeasurableSet s
hu : IsUniform X s ℙ μ
hnt : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hns : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
this : HasPDF X ℙ μ
⊢ pdf X ℙ μ =ᶠ[ae μ] s.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1)
have this₁ : IsProbabilityMeasure ℙ
Tactic: have : IsProbabilityMeasure ℙ := isProbabilityMeasure hns hnt hu
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hms : MeasurableSet s
hu : IsUniform X s ℙ μ
hnt : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hns : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
this_1 : HasPDF X ℙ μ
this : IsProbabilityMeasure ℙ
⊢ pdf X ℙ μ =ᶠ[ae μ] s.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1)
have neg : Measure.map X ℙ =
  μ.withDensity (s.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1))
Tactic: apply (eq_of_map_eq_withDensity _ _).mp
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hms : MeasurableSet s
hu : IsUniform X s ℙ μ
hnt : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hns : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
this_1 : HasPDF X ℙ μ
this : IsProbabilityMeasure ℙ
neg :
  Measure.map X ℙ =
    μ.withDensity (s.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1))
⊢ pdf X ℙ μ =ᶠ[ae μ] s.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1)
have apply : AEMeasurable (s.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1)) μ
Tactic: apply (eq_of_map_eq_withDensity _ _).mp
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hms : MeasurableSet s
hu : IsUniform X s ℙ μ
hnt : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hns : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
this_1 : HasPDF X ℙ μ
this : IsProbabilityMeasure ℙ
⊢ Measure.map X ℙ =
    μ.withDensity (s.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1))
have neg : μ[|s] = μ.withDensity (s.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1))
Tactic: rw [hu, withDensity_indicator hms, withDensity_smul _ measurable_one, withDensity_one,
      ProbabilityTheory.cond]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hms : MeasurableSet s
hu : IsUniform X s ℙ μ
hnt : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hns : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
this_1 : HasPDF X ℙ μ
this : IsProbabilityMeasure ℙ
neg :
  μ[|s] =
    μ.withDensity (s.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1))
⊢ Measure.map X ℙ =
    μ.withDensity (s.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1))
have neg₁ : μ[|s] = (μ.restrict s).withDensity (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1)
Tactic: rw [hu, withDensity_indicator hms, withDensity_smul _ measurable_one, withDensity_one,
      ProbabilityTheory.cond]