awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Distributions.TwoValued (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst : IsFiniteMeasure μ
hXmeas_1 : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
this :
  ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {m₀ : MeasurableSpace Ω} (hm : m ≤ m₀) {μ : Measure Ω}
    [IsFiniteMeasure μ] (hXmeas : AEMeasurable X μ) (hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1) (hXmeas : Measurable X),
    Var[X; μ | m] =ᶠ[ae μ] μ[X | m] * μ[1 - X | m]
hXmeas : ¬Measurable X
Y : Ω → ℝ
hYmeas : Measurable Y
hXY : X =ᶠ[ae μ] Y
μ₁ : Var[Y; μ | m] =ᶠ[ae μ] μ[Y | m] * μ[1 - Y | m]
⊢ Var[X; μ | m] =ᶠ[ae μ] μ[X | m] * μ[1 - X | m]
have μ₂ : μ[Y | m] * μ[1 - Y | m] =ᶠ[ae μ] μ[X | m] * μ[1 - X | m]
Tactic: calc
      Var[X; μ | m]
      _ =ᵐ[μ] Var[Y; μ | m] := condVar_congr_ae hXY
      _ =ᵐ[μ] μ[Y | m] * μ[1 - Y | m] := by
        refine this hm hYmeas.aemeasurable ?_ hYmeas
        filter_upwards [hX, hXY] with ω hXω hXYω
        simp [hXω, ← hXYω]
      _ =ᵐ[μ] μ[X | m] * μ[1 - X | m] := by
        refine .mul ?_ ?_ <;>
          exact condExp_congr_ae <| by filter_upwards [hXY] with ω hω; simp [hω]
-- Lean 4 proof step from Mathlib.Probability.Distributions.TwoValued (goal)
Goal:
Ω_1 : Type u_1
m_1 : MeasurableSpace Ω_1
X_1 : Ω_1 → ℝ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst : IsFiniteMeasure μ
hXmeas_1 : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
hXmeas : Measurable X
⊢ ∀ᵐ (x : Ω) ∂μ, ‖X x‖ ≤ 1
have h : ∀ (a : Ω), X a = 0 ∨ X a = 1 → ‖X a‖ ≤ 1
Tactic: filter_upwards [hX]
-- Lean 4 proof step from Mathlib.Probability.Distributions.TwoValued (goal)
Goal:
Ω_1 : Type u_1
m_1 : MeasurableSpace Ω_1
X_1 : Ω_1 → ℝ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst : IsFiniteMeasure μ
hXmeas_1 : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
hXmeas : Measurable X
⊢ μ[HPow.hPow (β := ℕ) X 2 | m] - HPow.hPow (β := ℕ) μ[X | m] 2 =ᶠ[ae μ] μ[X | m] - HPow.hPow (β := ℕ) μ[X | m] 2
have refine : μ[HPow.hPow (β := ℕ) X 2 | m] =ᶠ[ae μ] μ[X | m]
Tactic: refine .sub ?_ ae_eq_rfl
-- Lean 4 proof step from Mathlib.Probability.Distributions.TwoValued (goal)
Goal:
Ω_1 : Type u_1
m_1 : MeasurableSpace Ω_1
X_1 : Ω_1 → ℝ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst : IsFiniteMeasure μ
hXmeas_1 : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
hXmeas : Measurable X
⊢ HPow.hPow (β := ℕ) X 2 =ᶠ[ae μ] X
have h : ∀ (a : Ω), X a = 0 ∨ X a = 1 → HPow.hPow (β := ℕ) X 2 a = X a
Tactic: filter_upwards [hX]
-- Lean 4 proof step from Mathlib.Probability.Distributions.TwoValued (goal)
Goal:
Ω_1 : Type u_1
m_1 : MeasurableSpace Ω_1
X_1 : Ω_1 → ℝ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst : IsFiniteMeasure μ
hXmeas_1 : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
hXmeas : Measurable X
⊢ μ[X | m] - HPow.hPow (β := ℕ) μ[X | m] 2 =ᶠ[ae μ] μ[X | m] * μ[1 - X | m]
have rw : μ[X | m] * (1 - μ[X | m]) =ᶠ[ae μ] μ[X | m] * μ[1 - X | m]
Tactic: rw [sq, ← one_sub_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Probability.Distributions.TwoValued (goal)
Goal:
Ω_1 : Type u_1
m_1 : MeasurableSpace Ω_1
X_1 : Ω_1 → ℝ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst : IsFiniteMeasure μ
hXmeas_1 : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
hXmeas : Measurable X
⊢ μ[X | m] * (1 - μ[X | m]) =ᶠ[ae μ] μ[X | m] * μ[1 - X | m]
have refine : 1 - μ[X | m] =ᶠ[ae μ] μ[1 - X | m]
Tactic: refine .mul ae_eq_rfl ?_
-- Lean 4 proof step from Mathlib.Probability.Distributions.TwoValued (goal)
Goal:
Ω_1 : Type u_1
m_1 : MeasurableSpace Ω_1
X_1 : Ω_1 → ℝ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst : IsFiniteMeasure μ
hXmeas_1 : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
hXmeas : Measurable X
⊢ μ[1 | m] - μ[X | m] =ᶠ[ae μ] μ[1 - X | m]
have refine : ∀ᵐ (x : Ω) ∂μ, ‖X x‖ ≤ 1
Tactic: refine (condExp_sub (integrable_const _)
            (.of_bound (C := 1) hXmeas.aestronglyMeasurable ?_) _).symm
-- Lean 4 proof step from Mathlib.Probability.Distributions.TwoValued (goal)
Goal:
Ω_1 : Type u_1
m_1 : MeasurableSpace Ω_1
X_1 : Ω_1 → ℝ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst : IsFiniteMeasure μ
hXmeas_1 : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
hXmeas : Measurable X
⊢ 1 - μ[X | m] =ᶠ[ae μ] μ[1 - X | m]
have _ : 1 - μ[X | m] = μ[1 | m] - μ[X | m]
Tactic: calc
        1 - μ[X | m]
        _ = μ[1 | m] - μ[X | m] := by simp [Pi.one_def, hm]
        _ =ᵐ[μ] μ[1 - X | m] := by
          refine (condExp_sub (integrable_const _)
            (.of_bound (C := 1) hXmeas.aestronglyMeasurable ?_) _).symm
          filter_upwards [hX]
          rintro ω (hω | hω) <;> simp [hω]
-- Lean 4 proof step from Mathlib.Probability.Distributions.TwoValued (goal)
Goal:
Ω_1 : Type u_1
m_1 : MeasurableSpace Ω_1
X_1 : Ω_1 → ℝ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst : IsFiniteMeasure μ
hXmeas_1 : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
hXmeas : Measurable X
_ : 1 - μ[X | m] = μ[1 | m] - μ[X | m]
⊢ 1 - μ[X | m] =ᶠ[ae μ] μ[1 - X | m]
have _₁ : μ[1 | m] - μ[X | m] =ᶠ[ae μ] μ[1 - X | m]
Tactic: calc
        1 - μ[X | m]
        _ = μ[1 | m] - μ[X | m] := by simp [Pi.one_def, hm]
        _ =ᵐ[μ] μ[1 - X | m] := by
          refine (condExp_sub (integrable_const _)
            (.of_bound (C := 1) hXmeas.aestronglyMeasurable ?_) _).symm
          filter_upwards [hX]
          rintro ω (hω | hω) <;> simp [hω]
-- Lean 4 proof step from Mathlib.Probability.Distributions.TwoValued (goal)
Goal:
Ω_1 : Type u_1
m_1 : MeasurableSpace Ω_1
X_1 : Ω_1 → ℝ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst : IsFiniteMeasure μ
hXmeas_1 : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
hXmeas : Measurable X
⊢ Var[X; μ | m] =ᶠ[ae μ] μ[X | m] * μ[1 - X | m]
have _ : μ[HPow.hPow (β := ℕ) X 2 | m] - HPow.hPow (β := ℕ) μ[X | m] 2 =ᶠ[ae μ] μ[X | m] - HPow.hPow (β := ℕ) μ[X | m] 2
Tactic: calc
    _ =ᵐ[μ] μ[X ^ 2 | m] - μ[X | m] ^ 2 :=
      condVar_ae_eq_condExp_sq_sub_sq_condExp hm <| .of_bound hXmeas.aestronglyMeasurable 1 <| by
        filter_upwards [hX]; rintro ω (hω | hω) <;> simp [hω]
    _ =ᵐ[μ] μ[X | m] - μ[X | m] ^ 2 := by
      refine .sub ?_ ae_eq_rfl
      exact condExp_congr_ae <| by filter_upwards [hX]; rintro ω (hω | hω) <;> simp [hω]
    _ =ᵐ[μ] μ[X | m] * μ[1 - X | m] := by
      rw [sq, ← one_sub_mul, mul_comm]
      refine .mul ae_eq_rfl ?_
      calc
        1 - μ[X | m]
        _ = μ[1 | m] - μ[X | m] := by simp [Pi.one_def, hm]
        _ =ᵐ[μ] μ[1 - X | m] := by
          refine (condExp_sub (integrable_const _)
            (.of_bound (C := 1) hXmeas.aestronglyMeasurable ?_) _).symm
          filter_upwards [hX]
          rintro ω (hω | hω) <;> simp [hω]
-- Lean 4 proof step from Mathlib.Probability.Distributions.TwoValued (goal)
Goal:
Ω_1 : Type u_1
m_1 : MeasurableSpace Ω_1
X_1 : Ω_1 → ℝ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst : IsFiniteMeasure μ
hXmeas_1 : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
hXmeas : Measurable X
_ : μ[HPow.hPow (β := ℕ) X 2 | m] - HPow.hPow (β := ℕ) μ[X | m] 2 =ᶠ[ae μ] μ[X | m] - HPow.hPow (β := ℕ) μ[X | m] 2
⊢ Var[X; μ | m] =ᶠ[ae μ] μ[X | m] * μ[1 - X | m]
have _₁ : μ[X | m] - HPow.hPow (β := ℕ) μ[X | m] 2 =ᶠ[ae μ] μ[X | m] * μ[1 - X | m]
Tactic: calc
    _ =ᵐ[μ] μ[X ^ 2 | m] - μ[X | m] ^ 2 :=
      condVar_ae_eq_condExp_sq_sub_sq_condExp hm <| .of_bound hXmeas.aestronglyMeasurable 1 <| by
        filter_upwards [hX]; rintro ω (hω | hω) <;> simp [hω]
    _ =ᵐ[μ] μ[X | m] - μ[X | m] ^ 2 := by
      refine .sub ?_ ae_eq_rfl
      exact condExp_congr_ae <| by filter_upwards [hX]; rintro ω (hω | hω) <;> simp [hω]
    _ =ᵐ[μ] μ[X | m] * μ[1 - X | m] := by
      rw [sq, ← one_sub_mul, mul_comm]
      refine .mul ae_eq_rfl ?_
      calc
        1 - μ[X | m]
        _ = μ[1 | m] - μ[X | m] := by simp [Pi.one_def, hm]
        _ =ᵐ[μ] μ[1 - X | m] := by
          refine (condExp_sub (integrable_const _)
            (.of_bound (C := 1) hXmeas.aestronglyMeasurable ?_) _).symm
          filter_upwards [hX]
          rintro ω (hω | hω) <;> simp [hω]
-- Lean 4 proof step from Mathlib.Probability.Distributions.TwoValued (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
hXmeas : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
⊢ Var[X; μ] = μ.real {ω : Ω | X ω = 0} * μ.real {ω : Ω | X ω = 1}
have 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}
Tactic: obtain rfl | hμ := eq_zero_or_isProbabilityMeasure μ
Cleared hypotheses: μ, inst, hXmeas, hX
-- Lean 4 proof step from Mathlib.Probability.Distributions.TwoValued (goal)
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}
⊢ Var[X; μ] = μ.real {ω : Ω | X ω = 0} * μ.real {ω : Ω | X ω = 1}
have inr : ∀ (hμ : IsProbabilityMeasure μ), Var[X; μ] = μ.real {ω : Ω | X ω = 0} * μ.real {ω : Ω | X ω = 1}
Tactic: obtain rfl | hμ := eq_zero_or_isProbabilityMeasure μ
-- 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 : Measure.map X ℙ = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s)
⊢ AEMeasurable X ℙ
have by_contra : ∀ (h : ¬AEMeasurable X ℙ), False
Tactic: by_contra h
-- 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
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 ℙ
⊢ False
have hu₁ : 0 = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s)
Tactic: rw [map_of_not_aemeasurable h] at hu
Cleared hypotheses: hu, h
-- 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 : 0 = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s)
h : ¬AEMeasurable X ℙ
⊢ False
have apply : Eq (α := ℝ≥0∞) 0 1
Tactic: apply zero_ne_one' ℝ≥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
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 : Measure E) : (a : Set E) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞)
  ((HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s) : (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]
-- 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 : 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∞)
⊢ Eq (α := ℝ≥0∞) (((0 : Measure E) : (a : Set E) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
have rw₁ : HSMul.hSMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞)
    ((μ.restrict s : (a : Set E) → ℝ≥0∞) Set.univ : ℝ≥0∞) =
  1
Tactic: rw [hu, smul_apply, restrict_apply MeasurableSet.univ,
      Set.univ_inter, smul_eq_mul, ENNReal.inv_mul_cancel 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 : 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
⊢ Eq (α := ℝ≥0∞) (((0 : Measure E) : (a : Set E) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
have rw₂ : HSMul.hSMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (Set.univ ∩ s) : ℝ≥0∞) =
  1
Tactic: rw [hu, smul_apply, restrict_apply MeasurableSet.univ,
      Set.univ_inter, smul_eq_mul, ENNReal.inv_mul_cancel 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 : 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
⊢ Eq (α := ℝ≥0∞) (((0 : Measure E) : (a : Set E) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
have rw₃ : HSMul.hSMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) = 1
Tactic: rw [hu, smul_apply, restrict_apply MeasurableSet.univ,
      Set.univ_inter, smul_eq_mul, ENNReal.inv_mul_cancel 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 : 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
⊢ Eq (α := ℝ≥0∞) (((0 : Measure E) : (a : Set E) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
have rw₄ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) = 1
Tactic: rw [hu, smul_apply, restrict_apply MeasurableSet.univ,
      Set.univ_inter, smul_eq_mul, ENNReal.inv_mul_cancel 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 : 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
⊢ Eq (α := ℝ≥0∞) (((0 : Measure E) : (a : Set E) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
have rw₅ : Eq (α := ℝ≥0∞) 1 1
Tactic: rw [hu, smul_apply, restrict_apply MeasurableSet.univ,
      Set.univ_inter, smul_eq_mul, ENNReal.inv_mul_cancel 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
hu : IsUniform X s ℙ μ
⊢ Measure.map X ℙ ≪ μ
have rw : μ[|s] ≪ μ
Tactic: rw [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
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
⊢ (ℙ : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' A) =
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
have 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∞)
Tactic: rwa [← map_apply_of_aemeasurable (hu.aemeasurable hns hnt) hA, hu, ProbabilityTheory.cond_apply',
    ENNReal.div_eq_inv_mul]
-- 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 ℙ μ
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∞)
⊢ (ℙ : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' A) =
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
have rwa₁ : μ[A | s] =
  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]
-- 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 ℙ μ
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∞)
⊢ (ℙ : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' A) =
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
have 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∞)
Tactic: rwa [← map_apply_of_aemeasurable (hu.aemeasurable hns hnt) hA, hu, ProbabilityTheory.cond_apply',
    ENNReal.div_eq_inv_mul]
-- 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 ℙ μ
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
⊢ (ℙ : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' A) =
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
have 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∞)
Tactic: rwa [← map_apply_of_aemeasurable (hu.aemeasurable hns hnt) hA, hu, ProbabilityTheory.cond_apply',
    ENNReal.div_eq_inv_mul]
-- 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
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 ℙ μ
⊢ Eq (α := ℝ≥0∞) ((ℙ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
have this : X ⁻¹' Set.univ = Set.univ
Tactic: have : X ⁻¹' Set.univ = Set.univ := Set.preimage_univ