-- Mathlib/Probability/Distributions/Uniform.lean
theorem pdf_eq {X : Ω → E} {s : Set E} (hms : MeasurableSet s)
    (hu : IsUniform X s ℙ μ) : pdf X ℙ μ =ᵐ[μ] s.indicator ((μ s)⁻¹ • (1 : E → ℝ≥0∞))

Proof state:
case neg
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 : ¬μ s = ⊤
hns : ¬μ s = 0
this✝ : HasPDF X ℙ μ
this : IsProbabilityMeasure ℙ
⊢ Measure.map X ℙ = μ.withDensity (s.indicator ((μ s)⁻¹ • 1))

Tactic:
rw [hu, withDensity_indicator hms, withDensity_smul _ measurable_one, withDensity_one,
  ProbabilityTheory.cond]

Result:
no goals

Proof state:
case h
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 : ¬μ s = ⊤
hns : μ s = 0
x : E
hx : x ∉ s
h'x : pdf X ℙ μ x = 0 x
⊢ pdf X ℙ μ x = s.indicator ((μ s)⁻¹ • 1) x

Tactic:
simp [hx, h'x, hns]

Result:
no goals

Proof state:
case neg
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 : ¬μ s = ⊤
hns : ¬μ s = 0
this : HasPDF X ℙ μ
⊢ pdf X ℙ μ =ᶠ[ae μ] s.indicator ((μ s)⁻¹ • 1)

Tactic:
have : IsProbabilityMeasure ℙ := isProbabilityMeasure hns hnt hu

Result:
case neg
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 : ¬μ s = ⊤
hns : ¬μ s = 0
this✝ : HasPDF X ℙ μ
this : IsProbabilityMeasure ℙ
⊢ pdf X ℙ μ =ᶠ[ae μ] s.indicator ((μ s)⁻¹ • 1)

Proof state:
case neg
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 : ¬μ s = ⊤
⊢ pdf X ℙ μ =ᶠ[ae μ] s.indicator ((μ s)⁻¹ • 1)

Tactic:
by_cases hns : μ s = 0

Result:
case pos
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 : ¬μ s = ⊤
hns : μ s = 0
⊢ pdf X ℙ μ =ᶠ[ae μ] s.indicator ((μ s)⁻¹ • 1)

case neg
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 : ¬μ s = ⊤
hns : ¬μ s = 0
⊢ pdf X ℙ μ =ᶠ[ae μ] s.indicator ((μ s)⁻¹ • 1)

Proof state:
case pos
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 : ¬μ s = ⊤
hns : μ s = 0
⊢ pdf X ℙ μ =ᶠ[ae μ] s.indicator ((μ s)⁻¹ • 1)

Tactic:
filter_upwards [measure_zero_iff_ae_nmem.mp hns,
  pdf_eq_zero_of_measure_eq_zero_or_top hu (Or.inl hns)] with x hx h'x

Result:
case h
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 : ¬μ s = ⊤
hns : μ s = 0
x : E
hx : x ∉ s
h'x : pdf X ℙ μ x = 0 x
⊢ pdf X ℙ μ x = s.indicator ((μ s)⁻¹ • 1) x

Proof state:
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 : ¬μ s = ⊤
hns : ¬μ s = 0
this✝ : HasPDF X ℙ μ
this : IsProbabilityMeasure ℙ
⊢ AEMeasurable (s.indicator ((μ s)⁻¹ • 1)) μ

Tactic:
exact (measurable_one.aemeasurable.const_smul (μ s)⁻¹).indicator hms

Result:
no goals

Proof state:
case neg
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 : ¬μ s = ⊤
hns : ¬μ s = 0
⊢ pdf X ℙ μ =ᶠ[ae μ] s.indicator ((μ s)⁻¹ • 1)

Tactic:
have : HasPDF X ℙ μ := hasPDF hns hnt hu

Result:
case neg
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 : ¬μ s = ⊤
hns : ¬μ s = 0
this : HasPDF X ℙ μ
⊢ pdf X ℙ μ =ᶠ[ae μ] s.indicator ((μ s)⁻¹ • 1)

Proof state:
case pos
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 : μ s = ⊤
⊢ pdf X ℙ μ =ᶠ[ae μ] s.indicator ((μ s)⁻¹ • 1)

Tactic:
simp [pdf_eq_zero_of_measure_eq_zero_or_top hu (Or.inr hnt), hnt]

Result:
no goals

Proof state:
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 ((μ s)⁻¹ • 1)

Tactic:
by_cases hnt : μ s = ∞

Result:
case pos
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 : μ s = ⊤
⊢ pdf X ℙ μ =ᶠ[ae μ] s.indicator ((μ s)⁻¹ • 1)

case neg
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 : ¬μ s = ⊤
⊢ pdf X ℙ μ =ᶠ[ae μ] s.indicator ((μ s)⁻¹ • 1)

Proof state:
case neg
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 : ¬μ s = ⊤
hns : ¬μ s = 0
this✝ : HasPDF X ℙ μ
this : IsProbabilityMeasure ℙ
⊢ pdf X ℙ μ =ᶠ[ae μ] s.indicator ((μ s)⁻¹ • 1)

Tactic:
apply (eq_of_map_eq_withDensity _ _).mp

Result:
case neg
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 : ¬μ s = ⊤
hns : ¬μ s = 0
this✝ : HasPDF X ℙ μ
this : IsProbabilityMeasure ℙ
⊢ Measure.map X ℙ = μ.withDensity (s.indicator ((μ s)⁻¹ • 1))

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 : ¬μ s = ⊤
hns : ¬μ s = 0
this✝ : HasPDF X ℙ μ
this : IsProbabilityMeasure ℙ
⊢ AEMeasurable (s.indicator ((μ s)⁻¹ • 1)) μ