awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.TwoValued
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
hXmeas : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
inl :
  ∀ [IsZeroOrProbabilityMeasure.{u_1} (α := Ω) (m0 := m) 0] (hXmeas : AEMeasurable (_m := m) X 0)
    (hX : ∀ᵐ (ω : Ω) ∂0, X ω = 0 ∨ X ω = 1),
    variance (mΩ := m) X 0 =
      Measure.real.{u_1} (α := Ω) (m := m) 0 {ω : Ω | X ω = 0} *
        Measure.real.{u_1} (α := Ω) (m := m) 0 {ω : Ω | X ω = 1}
inr : ∀ (hμ : IsProbabilityMeasure μ), Var[X; μ] = μ.real {ω : Ω | X ω = 0} * μ.real {ω : Ω | X ω = 1}
⊢ Var[X; μ] = μ.real {ω : Ω | X ω = 0} * μ.real {ω : Ω | X ω = 1}

Tactic:
obtain rfl | hμ := eq_zero_or_isProbabilityMeasure μ

Premises used: MeasureTheory.eq_zero_or_isProbabilityMeasure, rfl
-- Module: Mathlib.Probability.Distributions.TwoValued
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
inst : IsZeroOrProbabilityMeasure.{u_1} (α := Ω) (m0 := m) 0
hXmeas : AEMeasurable (_m := m) X 0
hX : ∀ᵐ (ω : Ω) ∂0, X ω = 0 ∨ X ω = 1
⊢ variance (mΩ := m) X 0 =
    Measure.real.{u_1} (α := Ω) (m := m) 0 {ω : Ω | X ω = 0} * Measure.real.{u_1} (α := Ω) (m := m) 0 {ω : Ω | X ω = 1}

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.TwoValued
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
hXmeas : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
hμ : IsProbabilityMeasure μ
⊢ Var[X; μ] = μ.real {ω : Ω | X ω = 0} * μ.real {ω : Ω | X ω = 1}

Tactic:
simpa [Pi.mul_def, integral_of_ae_eq_zero_or_one, integral_one_sub_of_ae_eq_zero_or_one, mul_comm,
    *] using condVar_of_ae_eq_zero_or_one bot_le hXmeas hX

Premises used: MeasureTheory.integral_of_ae_eq_zero_or_one, ProbabilityTheory.condVar_of_ae_eq_zero_or_one, mul_comm, Pi.mul_def, MeasureTheory.integral_one_sub_of_ae_eq_zero_or_one, bot_le
-- Module: Mathlib.Probability.Distributions.Uniform
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 : Measure.map X ℙ = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s)
by_contra : ∀ (h : ¬AEMeasurable X ℙ), False
⊢ AEMeasurable X ℙ

Tactic:
by_contra h
-- Module: Mathlib.Probability.Distributions.Uniform
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 : Measure.map X ℙ = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s)
h : ¬AEMeasurable X ℙ
⊢ 0 = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s)

Tactic:
rw [map_of_not_aemeasurable h] at hu

Premises used: MeasureTheory.Measure.map_of_not_aemeasurable
-- Module: Mathlib.Probability.Distributions.Uniform
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 : Measure.map X ℙ = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s)
h : ¬AEMeasurable X ℙ
hu₁ : 0 = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s)
⊢ ¬AEMeasurable X ℙ

Tactic:
rw [map_of_not_aemeasurable h] at hu

Premises used: MeasureTheory.Measure.map_of_not_aemeasurable
-- Module: Mathlib.Probability.Distributions.Uniform
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 : 0 = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s)
h : ¬AEMeasurable X ℙ
apply : Eq (α := ℝ≥0∞) 0 1
⊢ False

Tactic:
apply zero_ne_one' ℝ≥0∞

Premises used: ENNReal, zero_ne_one'
-- Module: Mathlib.Probability.Distributions.Uniform
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 : 0 = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s)
h : ¬AEMeasurable X ℙ
⊢ Eq (α := ℝ≥0∞) (0 : ℝ≥0∞) (((0 : Measure E) : (a : Set E) → ℝ≥0∞) Set.univ : ℝ≥0∞)

Tactic:
rfl

Premises used: ENNReal.ofNNReal, WithTop.some, rfl
-- Module: Mathlib.Probability.Distributions.Uniform
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 : 0 = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s)
h : ¬AEMeasurable X ℙ
rw :
  Eq (α := ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s) : (a : Set E) → ℝ≥0∞) Set.univ :
      ℝ≥0∞)
    (1 : ℝ≥0∞)
rw₁ :
  HSMul.hSMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞)
      ((μ.restrict s : (a : Set E) → ℝ≥0∞) Set.univ : ℝ≥0∞) =
    1
rw₂ :
  HSMul.hSMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (Set.univ ∩ s) : ℝ≥0∞) =
    1
rw₃ :
  HSMul.hSMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) = 1
rw₄ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) = 1
rw₅ rw₆ : Eq (α := ℝ≥0∞) 1 1
⊢ Eq (α := ℝ≥0∞) (((0 : Measure E) : (a : Set E) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
rw [hu, smul_apply, restrict_apply MeasurableSet.univ,
      Set.univ_inter, smul_eq_mul, ENNReal.inv_mul_cancel hns hnt]

Premises used: MeasureTheory.Measure.restrict_apply, Set.univ_inter, MeasureTheory.Measure.smul_apply, ENNReal.inv_mul_cancel, smul_eq_mul, MeasurableSet.univ
-- Module: Mathlib.Probability.Distributions.Uniform
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 ℙ μ
rw : μ[|s] ≪ μ
⊢ Measure.map X ℙ ≪ μ

Tactic:
rw [hu]
-- Module: Mathlib.Probability.Distributions.Uniform
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 ℙ μ
⊢ μ[|s] ≪ μ

Tactic:
ProbabilityTheory.cond_absolutelyContinuous

Premises used: ProbabilityTheory.cond_absolutelyContinuous
-- Module: Mathlib.Probability.Distributions.Uniform
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 ℙ μ
⊢ μ[|s] ≪ μ

Tactic:
exact ProbabilityTheory.cond_absolutelyContinuous

Premises used: ProbabilityTheory.cond_absolutelyContinuous
-- Module: Mathlib.Probability.Distributions.Uniform
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 ℙ μ
A : Set E
hA : MeasurableSet A
rwa :
  ((Measure.map X ℙ : Measure E) : (a : Set E) → ℝ≥0∞) A =
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
rwa₁ :
  μ[A | s] =
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
rwa₂ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
ht : MeasurableSet A
rwa₃ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞)
ht₁ : MeasurableSet A
rwa₄ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞)
ht₂ ht₃ ht₄ : MeasurableSet A
⊢ (ℙ : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' A) =
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rwa [← map_apply_of_aemeasurable (hu.aemeasurable hns hnt) hA, hu, ProbabilityTheory.cond_apply',
    ENNReal.div_eq_inv_mul]

Premises used: MeasureTheory.Measure.map_apply_of_aemeasurable, ProbabilityTheory.cond_apply', MeasureTheory.pdf.IsUniform.aemeasurable, ENNReal.div_eq_inv_mul
-- Module: Mathlib.Probability.Distributions.Uniform
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 ℙ μ
⊢ X ⁻¹' Set.univ = Set.univ

Tactic:
have : X ⁻¹' Set.univ = Set.univ := Set.preimage_univ
-- Module: Mathlib.Probability.Distributions.Uniform
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
rw₃ rw₄ : Eq (α := ℝ≥0∞) 1 1
⊢ Eq (α := ℝ≥0∞) ((ℙ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
rw [← this, hu.measure_preimage hns hnt MeasurableSet.univ, Set.inter_univ,
      ENNReal.div_self hns hnt]

Premises used: Set.inter_univ, MeasureTheory.pdf.IsUniform.measure_preimage, ENNReal.div_self, MeasurableSet.univ
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
rw rw₁ : Measure.map X ℙ = μ[|s] ↔ Measure.map X ℙ = μ[|s]
⊢ Measure.map X ℙ = μ[|toMeasurable μ s] ↔ Measure.map X ℙ = μ[|s]

Tactic:
rw [ProbabilityTheory.cond_toMeasurable_eq]

Premises used: ProbabilityTheory.cond_toMeasurable_eq
-- Module: Mathlib.Probability.Distributions.Uniform
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 ℙ μ
⊢ IsUniform X (toMeasurable μ s) ℙ μ

Tactic:
toMeasurable_iff.mpr hu

Premises used: Iff.mpr, MeasureTheory.pdf.IsUniform.toMeasurable_iff
-- Module: Mathlib.Probability.Distributions.Uniform
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
apply :
  Measure.map X ℙ =
    μ.withDensity (t.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞) 1))
⊢ HasPDF X ℙ μ

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)

Premises used: AEMeasurable.const_smul, Measurable.aemeasurable, Set.indicator, AEMeasurable.indicator, measurable_one, MeasureTheory.measurableSet_toMeasurable, Inv.inv, MeasureTheory.hasPDF_of_map_eq_withDensity, HSMul.hSMul, MeasureTheory.pdf.IsUniform.aemeasurable, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Probability.Distributions.Uniform
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)
rw₆ rw₇ :
  HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict 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))

Tactic:
rw [hu, withDensity_indicator (measurableSet_toMeasurable μ s), withDensity_smul _ measurable_one,
    withDensity_one, restrict_toMeasurable hnt, measure_toMeasurable, ProbabilityTheory.cond]

Premises used: MeasureTheory.Measure.restrict_toMeasurable, MeasureTheory.withDensity_one, MeasureTheory.withDensity_indicator, MeasureTheory.measure_toMeasurable, measurable_one, MeasureTheory.measurableSet_toMeasurable, MeasureTheory.withDensity_smul, ProbabilityTheory.cond
-- Module: Mathlib.Probability.Distributions.Uniform
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
inr : ∀ (H : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)), pdf X ℙ μ =ᶠ[ae μ] 0
⊢ pdf X ℙ μ =ᶠ[ae μ] 0

Tactic:
rcases hμs with H | H
-- Module: Mathlib.Probability.Distributions.Uniform
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∞)
⊢ 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

Premises used: Iff.mpr, MeasureTheory.Measure.restrict_eq_zero, smul_zero, ENNReal.inv_zero, ProbabilityTheory.cond, MeasureTheory.pdf.IsUniform
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
H : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hu : Eq (α := Measure E) (Measure.map X ℙ) 0
⊢ pdf X ℙ μ =ᶠ[ae μ] 0

Tactic:
simp [pdf, hu]

Premises used: MeasureTheory.pdf
-- Module: Mathlib.Probability.Distributions.Uniform
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∞)
⊢ Eq (α := Measure E) (Measure.map X ℙ) 0

Tactic:
simp only [IsUniform, ProbabilityTheory.cond, H, ENNReal.inv_top, zero_smul] at hu

Premises used: zero_smul, ENNReal.inv_top, ProbabilityTheory.cond, MeasureTheory.pdf.IsUniform
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
H : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hu : Eq (α := Measure E) (Measure.map X ℙ) 0
⊢ pdf X ℙ μ =ᶠ[ae μ] 0

Tactic:
simp [pdf, hu]

Premises used: MeasureTheory.pdf
-- Module: Mathlib.Probability.Distributions.Uniform
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)
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)
⊢ pdf X ℙ μ =ᶠ[ae μ] s.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1)

Tactic:
by_cases hnt : μ s = ∞

Premises used: DFunLike.coe
-- Module: Mathlib.Probability.Distributions.Uniform
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)

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

Premises used: MeasureTheory.pdf.IsUniform.pdf_eq_zero_of_measure_eq_zero_or_top, Or.inr
-- Module: Mathlib.Probability.Distributions.Uniform
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)
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)
⊢ pdf X ℙ μ =ᶠ[ae μ] s.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1)

Tactic:
by_cases hns : μ s = 0

Premises used: DFunLike.coe
-- Module: Mathlib.Probability.Distributions.Uniform
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∞)
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
⊢ pdf X ℙ μ =ᶠ[ae μ] s.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 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

Premises used: MeasureTheory.pdf.IsUniform.pdf_eq_zero_of_measure_eq_zero_or_top, Iff.mp, Or.inl, MeasureTheory.measure_eq_zero_iff_ae_notMem
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x_1 : 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∞)
x : E
hx : x ∉ s
h'x : pdf X ℙ μ x = 0 x
⊢ pdf X ℙ μ x = s.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1) x

Tactic:
simp [hx, h'x, hns]
-- Module: Mathlib.Probability.Distributions.Uniform
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∞)
⊢ HasPDF X ℙ μ

Tactic:
have : HasPDF X ℙ μ := hasPDF hns hnt hu
-- Module: Mathlib.Probability.Distributions.Uniform
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 ℙ μ
⊢ IsProbabilityMeasure ℙ

Tactic:
have : IsProbabilityMeasure ℙ := isProbabilityMeasure hns hnt hu
-- Module: Mathlib.Probability.Distributions.Uniform
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))
apply : AEMeasurable (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)

Tactic:
apply (eq_of_map_eq_withDensity _ _).mp

Premises used: MeasureTheory.pdf.eq_of_map_eq_withDensity, Iff.mp
-- Module: Mathlib.Probability.Distributions.Uniform
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)
neg₄ neg₅ :
  HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict 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))

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

Premises used: MeasureTheory.withDensity_one, MeasureTheory.withDensity_indicator, measurable_one, MeasureTheory.withDensity_smul, ProbabilityTheory.cond