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
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))
neg₁ :
  μ[|s] = (μ.restrict s).withDensity (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] = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ.restrict s).withDensity 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))
neg₁ :
  μ[|s] = (μ.restrict s).withDensity (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1)
neg₂ : μ[|s] = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ.restrict s).withDensity 1)
⊢ Measure.map X ℙ =
    μ.withDensity (s.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1))
have neg₃ : μ[|s] = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s)
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))
neg₁ :
  μ[|s] = (μ.restrict s).withDensity (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1)
neg₂ : μ[|s] = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ.restrict s).withDensity 1)
neg₃ : μ[|s] = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s)
⊢ Measure.map X ℙ =
    μ.withDensity (s.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1))
have neg₄ : 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 hms, withDensity_smul _ measurable_one, withDensity_one,
      ProbabilityTheory.cond]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x_1 : ℝ) ↦ x_1 * (pdf X ℙ volume x_1).toReal) volume
have pos : ∀
  (hnt :
    Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x_1 : ℝ) ↦ x_1 * (pdf X ℙ volume x_1).toReal) volume
Tactic: by_cases hnt : volume s = 0 ∨ volume s = ∞
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
pos :
  ∀
    (hnt :
      Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
        Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x_1 : ℝ) ↦ x_1 * (pdf X ℙ volume x_1).toReal) volume
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x_1 : ℝ) ↦ x_1 * (pdf X ℙ volume x_1).toReal) volume
have neg : ∀
  (hnt :
    ¬(Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
        Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))),
  @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x_1 : ℝ) ↦ x_1 * (pdf X ℙ volume x_1).toReal) volume
Tactic: by_cases hnt : volume s = 0 ∨ volume s = ∞
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (hypothesis)
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt :
  Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x_1 : ℝ) ↦ x_1 * (pdf X ℙ volume x_1).toReal) volume
have I : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ x * ENNReal.toReal 0) volume
Tactic: have I : Integrable (fun x ↦ x * ENNReal.toReal (0)) := by simp
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt :
  Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
I : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ x * ENNReal.toReal 0) volume
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x_1 : ℝ) ↦ x_1 * (pdf X ℙ volume x_1).toReal) volume
have pos : (ae (F := Measure ℝ) volume).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ x * ENNReal.toReal 0) fun (x_1 : ℝ) ↦
  x_1 * (pdf X ℙ volume x_1).toReal
Tactic: apply I.congr
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt :
  Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
I : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ x * ENNReal.toReal 0) volume
⊢ (ae (F := Measure ℝ) volume).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ x * ENNReal.toReal 0) fun (x_1 : ℝ) ↦
    x_1 * (pdf X ℙ volume x_1).toReal
have h : ∀ (x_1 : ℝ) (hx : pdf X ℙ volume x_1 = 0 x_1), x_1 * ENNReal.toReal 0 = x_1 * (pdf X ℙ volume x_1).toReal
Tactic: filter_upwards [pdf_eq_zero_of_measure_eq_zero_or_top huX hnt] with x hx
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (hypothesis)
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt :
  ¬(Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x_1 : ℝ) ↦ x_1 * (pdf X ℙ volume x_1).toReal) volume
have hnt₁ : ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
  ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: simp only [not_or] at hnt
Cleared hypotheses: hnt
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (hypothesis)
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt :
  ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x_1 : ℝ) ↦ x_1 * (pdf X ℙ volume x_1).toReal) volume
have this : IsProbabilityMeasure ℙ
Tactic: have : IsProbabilityMeasure ℙ := isProbabilityMeasure hnt.1 hnt.2 huX
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt :
  ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : IsProbabilityMeasure ℙ
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x_1 : ℝ) ↦ x_1 * (pdf X ℙ volume x_1).toReal) volume
have neg : AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace) (fun (x_1 : ℝ) ↦ x_1 * (pdf X ℙ volume x_1).toReal)
  volume
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt :
  ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : IsProbabilityMeasure ℙ
neg :
  AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace)
    (fun (x_1 : ℝ) ↦ x_1 * (pdf X ℙ volume x_1).toReal) volume
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x_1 : ℝ) ↦ x_1 * (pdf X ℙ volume x_1).toReal) volume
have neg₁ : @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (x_1 : ℝ) ↦ x_1 * (pdf X ℙ volume x_1).toReal) volume
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt :
  ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : IsProbabilityMeasure ℙ
⊢ @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (x_1 : ℝ) ↦ x_1 * (pdf X ℙ volume x_1).toReal) volume
have neg : ∫⁻ (x : ℝ),
    ‖x‖ₑ * s.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := ℝ → ℝ≥0∞) (((volume : (a : Set ℝ) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1) x ≠
  ∞
Tactic: refine hasFiniteIntegral_mul (pdf_eq hcs.measurableSet huX) ?_
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (hypothesis)
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt :
  ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : IsProbabilityMeasure ℙ
ind : ℝ → ℝ≥0∞ := HSMul.hSMul (α := ℝ≥0∞) (β := ℝ → ℝ≥0∞) (((volume : (a : Set ℝ) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1
⊢ ∫⁻ (x : ℝ), ‖x‖ₑ * s.indicator ind x ≠ ∞
have this₁ : ∀ (x : ℝ), ‖x‖ₑ * s.indicator ind x = s.indicator (fun (x : ℝ) ↦ ‖x‖ₑ * ind x) x
Tactic: have : ∀ x, ‖x‖ₑ * s.indicator ind x = s.indicator (fun x => ‖x‖ₑ * ind x) x := fun x =>
    (s.indicator_mul_right (fun x => ↑‖x‖₊) ind).symm
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt :
  ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this_1 : IsProbabilityMeasure ℙ
ind : ℝ → ℝ≥0∞ := HSMul.hSMul (α := ℝ≥0∞) (β := ℝ → ℝ≥0∞) (((volume : (a : Set ℝ) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1
this : ∀ (x : ℝ), ‖x‖ₑ * s.indicator ind x = s.indicator (fun (x : ℝ) ↦ ‖x‖ₑ * ind x) x
⊢ ∫⁻ (x : ℝ), ‖x‖ₑ * s.indicator ind x ≠ ∞
have neg : ∫⁻ (x : ℝ) in s, HMul.hMul (β := ℝ≥0∞) ‖x‖ₑ (((volume : (a : Set ℝ) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ∂volume ≠ ∞
Tactic: simp only [ind, this, lintegral_indicator hcs.measurableSet, mul_one, smul_eq_mul,
    Pi.one_apply, Pi.smul_apply]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt :
  ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this_1 : IsProbabilityMeasure ℙ
ind : ℝ → ℝ≥0∞ := HSMul.hSMul (α := ℝ≥0∞) (β := ℝ → ℝ≥0∞) (((volume : (a : Set ℝ) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1
this : ∀ (x : ℝ), ‖x‖ₑ * s.indicator ind x = s.indicator (fun (x : ℝ) ↦ ‖x‖ₑ * ind x) x
⊢ ∫⁻ (x : ℝ) in s, HMul.hMul (β := ℝ≥0∞) ‖x‖ₑ (((volume : (a : Set ℝ) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ∂volume ≠ ∞
have neg : HMul.hMul (β := ℝ≥0∞) (∫⁻ (a : ℝ) in s, ‖a‖ₑ ∂volume) (((volume : (a : Set ℝ) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ≠ ∞
Tactic: rw [lintegral_mul_const _ measurable_enorm]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
huX : IsUniform X s ℙ volume
⊢ ∫ (x : Ω), X x ∂ℙ =
    ENNReal.toReal ((volume : (a : Set ℝ) → ℝ≥0∞) s)⁻¹ *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (restrict volume s) fun (x : ℝ) ↦ x
have rw : Eq (α := ℝ) (∫ (x : Ω), X x ∂ℙ)
  (∫ (x : ℝ),
    x ∂HSMul.hSMul (α := ℝ≥0∞) (β := Measure ℝ) (((volume : (a : Set ℝ) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (restrict volume s))
Tactic: rw [← smul_eq_mul, ← integral_smul_measure]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
huX :
  Measure.map X ℙ =
    HSMul.hSMul (α := ℝ≥0∞) (β := Measure ℝ) (((volume : (a : Set ℝ) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (restrict volume s)
⊢ Eq (α := ℝ) (∫ (x : Ω), X x ∂ℙ)
    (∫ (x : ℝ),
      x ∂HSMul.hSMul (α := ℝ≥0∞) (β := Measure ℝ) (((volume : (a : Set ℝ) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (restrict volume s))
have rw : Eq (α := ℝ) (∫ (x : Ω), X x ∂ℙ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.map X ℙ) fun (x : ℝ) ↦ x)
Tactic: rw [← huX]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
huX :
  Measure.map X ℙ =
    HSMul.hSMul (α := ℝ≥0∞) (β := Measure ℝ) (((volume : (a : Set ℝ) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (restrict volume s)
⊢ Eq (α := ℝ) (∫ (x : Ω), X x ∂ℙ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.map X ℙ) fun (x : ℝ) ↦ x)
have pos : ∀ (hX : AEMeasurable X ℙ),
  Eq (α := ℝ) (∫ (x : Ω), X x ∂ℙ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.map X ℙ) fun (x : ℝ) ↦ x)
Tactic: by_cases hX : AEMeasurable X ℙ
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
huX :
  Measure.map X ℙ =
    HSMul.hSMul (α := ℝ≥0∞) (β := Measure ℝ) (((volume : (a : Set ℝ) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (restrict volume s)
pos :
  ∀ (hX : AEMeasurable X ℙ),
    Eq (α := ℝ) (∫ (x : Ω), X x ∂ℙ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.map X ℙ) fun (x : ℝ) ↦ x)
⊢ Eq (α := ℝ) (∫ (x : Ω), X x ∂ℙ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.map X ℙ) fun (x : ℝ) ↦ x)
have neg : ∀ (hX : ¬AEMeasurable X ℙ),
  Eq (α := ℝ) (∫ (x : Ω), X x ∂ℙ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.map X ℙ) fun (x : ℝ) ↦ x)
Tactic: by_cases hX : AEMeasurable X ℙ
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
huX :
  Measure.map X ℙ =
    HSMul.hSMul (α := ℝ≥0∞) (β := Measure ℝ) (((volume : (a : Set ℝ) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (restrict volume s)
hX : ¬AEMeasurable X ℙ
⊢ Eq (α := ℝ) (∫ (x : Ω), X x ∂ℙ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.map X ℙ) fun (x : ℝ) ↦ x)
have neg : ¬AEStronglyMeasurable X ℙ
Tactic: rw [map_of_not_aemeasurable hX, integral_zero_measure, integral_non_aestronglyMeasurable]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
⊢ PMF α
have refine_1 : Eq (α := ℝ≥0∞) (∑ a ∈ s, (fun (a : α) ↦ (if a ∈ s then (↑(#s) : ℝ≥0∞)⁻¹ else 0 : ℝ≥0∞)) a) 1
Tactic: refine ofFinset (fun a => if a ∈ s then s.card⁻¹ else 0) s ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
refine_1 : Eq (α := ℝ≥0∞) (∑ a ∈ s, (fun (a : α) ↦ (if a ∈ s then (↑(#s) : ℝ≥0∞)⁻¹ else 0 : ℝ≥0∞)) a) 1
⊢ PMF α
have refine_2 : ∀ a ∉ s, Eq (α := ℝ≥0∞) ((fun (a : α) ↦ (if a ∈ s then (↑(#s) : ℝ≥0∞)⁻¹ else 0 : ℝ≥0∞)) a) 0
Tactic: refine ofFinset (fun a => if a ∈ s then s.card⁻¹ else 0) s ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
⊢ Eq (α := ℝ≥0∞) (∑ a ∈ s, (fun (a : α) ↦ (if a ∈ s then (↑(#s) : ℝ≥0∞)⁻¹ else 0 : ℝ≥0∞)) a) 1
have refine_1 : HMul.hMul (α := ℝ≥0∞) (↑(#s) : ℝ≥0∞) (↑(#s) : ℝ≥0∞)⁻¹ = 1
Tactic: simp only [Finset.sum_ite_mem, Finset.inter_self, Finset.sum_const, nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (hypothesis)
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
⊢ HMul.hMul (α := ℝ≥0∞) (↑(#s) : ℝ≥0∞) (↑(#s) : ℝ≥0∞)⁻¹ = 1
have this : Ne (α := ℝ≥0∞) (↑(#s) : ℝ≥0∞) 0
Tactic: have : (s.card : ℝ≥0∞) ≠ 0 := by
      simpa only [Ne, Nat.cast_eq_zero, Finset.card_eq_zero] using
        Finset.nonempty_iff_ne_empty.1 hs
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
⊢ PMF α
have refine_1 : Eq (α := ℝ≥0∞) (∑ a ∈ s, (fun (a : α) ↦ (if a ∈ s then (↑(#s) : ℝ≥0∞)⁻¹ else 0 : ℝ≥0∞)) a) 1
Tactic: classical
  refine ofFinset (fun a => if a ∈ s then s.card⁻¹ else 0) s ?_ ?_
  · simp only [Finset.sum_ite_mem, Finset.inter_self, Finset.sum_const, nsmul_eq_mul]
    have : (s.card : ℝ≥0∞) ≠ 0 := by
      simpa only [Ne, Nat.cast_eq_zero, Finset.card_eq_zero] using
        Finset.nonempty_iff_ne_empty.1 hs
    exact ENNReal.mul_inv_cancel this <| ENNReal.natCast_ne_top s.card
  · exact fun x hx => by simp only [hx, if_false]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
refine_1 : Eq (α := ℝ≥0∞) (∑ a ∈ s, (fun (a : α) ↦ (if a ∈ s then (↑(#s) : ℝ≥0∞)⁻¹ else 0 : ℝ≥0∞)) a) 1
⊢ PMF α
have refine_2 : ∀ a ∉ s, Eq (α := ℝ≥0∞) ((fun (a : α) ↦ (if a ∈ s then (↑(#s) : ℝ≥0∞)⁻¹ else 0 : ℝ≥0∞)) a) 0
Tactic: classical
  refine ofFinset (fun a => if a ∈ s then s.card⁻¹ else 0) s ?_ ?_
  · simp only [Finset.sum_ite_mem, Finset.inter_self, Finset.sum_const, nsmul_eq_mul]
    have : (s.card : ℝ≥0∞) ≠ 0 := by
      simpa only [Ne, Nat.cast_eq_zero, Finset.card_eq_zero] using
        Finset.nonempty_iff_ne_empty.1 hs
    exact ENNReal.mul_inv_cancel this <| ENNReal.natCast_ne_top s.card
  · exact fun x hx => by simp only [hx, if_false]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
⊢ ∀ (x : α), x ∈ (uniformOfFinset s hs).support ↔ x ∈ (↑s : Set α)
have let : ∀ (a : α) (ha : a ∈ s) (x : α), x ∈ (uniformOfFinset s sorry).support ↔ x ∈ (↑s : Set α)
Tactic: let ⟨a, ha⟩ := hs
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
t : Set α
x : α
⊢ Eq (α := ℝ≥0∞) (if x ∈ t then (uniformOfFinset s hs : (a : α) → ℝ≥0∞) x else 0 : ℝ≥0∞)
    (if x ∈ s ∧ x ∈ t then (↑(#s) : ℝ≥0∞)⁻¹ else 0 : ℝ≥0∞)
have simp_rw : Eq (α := ℝ≥0∞) (if x ∈ t then if x ∈ s then (↑(#s) : ℝ≥0∞)⁻¹ else 0 else 0)
  (if x ∈ s ∧ x ∈ t then (↑(#s) : ℝ≥0∞)⁻¹ else 0)
Tactic: simp_rw [uniformOfFinset_apply, ← ite_and, and_comm]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
t : Set α
x : α
simp_rw :
  Eq (α := ℝ≥0∞) (if x ∈ t then if x ∈ s then (↑(#s) : ℝ≥0∞)⁻¹ else 0 else 0)
    (if x ∈ s ∧ x ∈ t then (↑(#s) : ℝ≥0∞)⁻¹ else 0)
⊢ Eq (α := ℝ≥0∞) (if x ∈ t then (uniformOfFinset s hs : (a : α) → ℝ≥0∞) x else 0 : ℝ≥0∞)
    (if x ∈ s ∧ x ∈ t then (↑(#s) : ℝ≥0∞)⁻¹ else 0 : ℝ≥0∞)
have simp_rw₁ : Eq (α := ℝ≥0∞) (if x ∈ t ∧ x ∈ s then (↑(#s) : ℝ≥0∞)⁻¹ else 0) (if x ∈ s ∧ x ∈ t then (↑(#s) : ℝ≥0∞)⁻¹ else 0)
Tactic: simp_rw [uniformOfFinset_apply, ← ite_and, and_comm]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (hypothesis)
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
t : Set α
x : α
hx : x ∈ {x ∈ s | x ∈ t}
⊢ Eq (α := ℝ≥0∞) (if x ∈ s ∧ x ∈ t then (↑(#s) : ℝ≥0∞)⁻¹ else 0) (↑(#s) : ℝ≥0∞)⁻¹
have this : x ∈ s ∧ x ∈ t
Tactic: have this : x ∈ s ∧ x ∈ t := by simpa using hx
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Nonempty α
s : Set α
inst_2 : Fintype (↑s : Type u_1)
⊢ ((uniformOfFintype α).toOuterMeasure : (a : Set α) → ℝ≥0∞) s =
    HDiv.hDiv (α := ℝ≥0∞) (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞)
have rw : ((toOuterMeasure (uniformOfFinset Finset.univ sorry) : MeasureTheory.OuterMeasure α) : (a : Set α) → ℝ≥0∞) s =
  HDiv.hDiv (α := ℝ≥0∞) (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞)
Tactic: rw [uniformOfFintype, toOuterMeasure_uniformOfFinset_apply, Fintype.card_subtype,
    Finset.card_univ]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Nonempty α
s : Set α
inst_2 : Fintype (↑s : Type u_1)
rw :
  ((toOuterMeasure (uniformOfFinset Finset.univ ⋯) : MeasureTheory.OuterMeasure α) : (a : Set α) → ℝ≥0∞) s =
    HDiv.hDiv (α := ℝ≥0∞) (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞)
⊢ ((uniformOfFintype α).toOuterMeasure : (a : Set α) → ℝ≥0∞) s =
    HDiv.hDiv (α := ℝ≥0∞) (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞)
have rw₁ : HDiv.hDiv (α := ℝ≥0∞) (↑(Finset.card.{u_1} (α := α) {x : α | x ∈ s}) : ℝ≥0∞)
    (↑(Finset.card.{u_1} (α := α) Finset.univ) : ℝ≥0∞) =
  HDiv.hDiv (α := ℝ≥0∞) (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞)
Tactic: rw [uniformOfFintype, toOuterMeasure_uniformOfFinset_apply, Fintype.card_subtype,
    Finset.card_univ]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Nonempty α
s : Set α
inst_2 : Fintype (↑s : Type u_1)
rw :
  ((toOuterMeasure (uniformOfFinset Finset.univ ⋯) : MeasureTheory.OuterMeasure α) : (a : Set α) → ℝ≥0∞) s =
    HDiv.hDiv (α := ℝ≥0∞) (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞)
rw₁ :
  HDiv.hDiv (α := ℝ≥0∞) (↑(Finset.card.{u_1} (α := α) {x : α | x ∈ s}) : ℝ≥0∞)
      (↑(Finset.card.{u_1} (α := α) Finset.univ) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞)
⊢ ((uniformOfFintype α).toOuterMeasure : (a : Set α) → ℝ≥0∞) s =
    HDiv.hDiv (α := ℝ≥0∞) (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞)
have rw₂ : HDiv.hDiv (α := ℝ≥0∞) (↑(Finset.card.{u_1} (α := α) {x : α | x ∈ s}) : ℝ≥0∞)
    (↑(Finset.card.{u_1} (α := α) Finset.univ) : ℝ≥0∞) =
  HDiv.hDiv (α := ℝ≥0∞) (↑(Finset.card.{u_1} (α := α) {x : α | x ∈ s}) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞)
Tactic: rw [uniformOfFintype, toOuterMeasure_uniformOfFinset_apply, Fintype.card_subtype,
    Finset.card_univ]