awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.TwoValued
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hXmeas : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
h : ¬Eq (α := ENNReal) ((μ : (a : Set Ω) → ENNReal) {ω : Ω | X ω = 1} : ENNReal) (⊤ : ENNReal)
⊢ HAdd.hAdd (α := ℝ)
      (∫ (x : ℝ),
        id
          x ∂HSMul.hSMul (α := ENNReal) (β := Measure ℝ) ((μ : (a : Set Ω) → ENNReal) (X ⁻¹' {0}) : ENNReal)
          (Measure.dirac 0))
      (∫ (x : ℝ),
        id
          x ∂HSMul.hSMul (α := ENNReal) (β := Measure ℝ) ((μ : (a : Set Ω) → ENNReal) (X ⁻¹' {1}) : ENNReal)
          (Measure.dirac 1)) =
    μ.real {ω : Ω | X ω = 1}

Tactic:
simp [Measure.real, Set.preimage]

Premises used: MeasureTheory.Measure.real, Set.preimage
-- Module: Mathlib.Probability.Distributions.TwoValued
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hXmeas : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
⊢ ∀ᵐ (ω : Ω) ∂μ, 1 - X ω = 0 ∨ 1 - X ω = 1

Tactic:
simpa [sub_eq_zero, or_comm, eq_comm (a := (1 : ℝ))] using hX

Premises used: sub_eq_zero, eq_comm, or_comm
-- Module: Mathlib.Probability.Distributions.TwoValued
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hXmeas : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
⊢ μ.real {ω : Ω | 1 - X ω = 1} = μ.real {ω : Ω | X ω = 0}

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.TwoValued
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hXmeas : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
_ : μ.real {ω : Ω | 1 - X ω = 1} = μ.real {ω : Ω | X ω = 0}
⊢ ∫ (ω : Ω), 1 - X ω ∂μ = μ.real {ω : Ω | X ω = 0}

Tactic:
calc
    _ = μ.real {ω | 1 - X ω = 1} :=
      integral_of_ae_eq_zero_or_one (aemeasurable_const (b := 1).sub hXmeas)
        (by simpa [sub_eq_zero, or_comm, eq_comm (a := (1 : ℝ))] using hX)
    _ = μ.real {ω | X ω = 0} := by simp

Premises used: setOf, MeasureTheory.Measure.real, HSub.hSub, MeasureTheory.integral_of_ae_eq_zero_or_one, OfNat.ofNat, Eq, AEMeasurable.sub, aemeasurable_const
-- Module: Mathlib.Probability.Distributions.TwoValued
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst : IsFiniteMeasure μ
hXmeas : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
inr :
  ∀
    (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), Var[X; μ | m] =ᶠ[ae μ] μ[X | m] * μ[1 - X | m]
wlog :
  ∀ {Ω : 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]
⊢ Var[X; μ | m] =ᶠ[ae μ] μ[X | m] * μ[1 - X | m]

Tactic:
wlog hXmeas : Measurable[m₀] X

Premises used: Measurable
-- Module: Mathlib.Probability.Distributions.TwoValued
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
inr : ∀ (Y : Ω → ℝ) (hYmeas : Measurable Y) (hXY : X =ᶠ[ae μ] Y), Var[X; μ | m] =ᶠ[ae μ] μ[X | m] * μ[1 - X | m]
⊢ Var[X; μ | m] =ᶠ[ae μ] μ[X | m] * μ[1 - X | m]

Tactic:
obtain ⟨Y, hYmeas, hXY⟩ := ‹AEMeasurable[m₀] X μ›

Premises used: AEMeasurable
-- Module: Mathlib.Probability.Distributions.TwoValued
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[X; μ | m] =ᶠ[ae μ] Var[Y; μ | m]

Tactic:
condVar_congr_ae hXY

Premises used: ProbabilityTheory.condVar_congr_ae
-- Module: Mathlib.Probability.Distributions.TwoValued
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]

Tactic:
this hm hYmeas.aemeasurable ?_ hYmeas

Premises used: Measurable.aemeasurable
-- Module: Mathlib.Probability.Distributions.TwoValued
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
refine : ∀ᵐ (ω : Ω) ∂μ, Y ω = 0 ∨ Y ω = 1
⊢ Var[Y; μ | m] =ᶠ[ae μ] μ[Y | m] * μ[1 - Y | m]

Tactic:
refine this hm hYmeas.aemeasurable ?_ hYmeas

Premises used: Measurable.aemeasurable
-- Module: Mathlib.Probability.Distributions.TwoValued
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
h : ∀ (ω : Ω) (hXω : X ω = 0 ∨ X ω = 1) (hXYω : X ω = Y ω), Y ω = 0 ∨ Y ω = 1
⊢ ∀ᵐ (ω : Ω) ∂μ, Y ω = 0 ∨ Y ω = 1

Tactic:
filter_upwards [hX, hXY] with ω hXω hXYω
-- Module: Mathlib.Probability.Distributions.TwoValued
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
ω : Ω
hXω : X ω = 0 ∨ X ω = 1
hXYω : X ω = Y ω
⊢ Y ω = 0 ∨ Y ω = 1

Tactic:
simp [hXω, ← hXYω]
-- Module: Mathlib.Probability.Distributions.TwoValued
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
⊢ μ[Y | m] * μ[1 - Y | m] =ᶠ[ae μ] μ[X | m] * μ[1 - X | m]

Tactic:
.mul ?_ ?_

Premises used: Filter.EventuallyEq.mul
-- Module: Mathlib.Probability.Distributions.TwoValued
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
refine_1 : μ[Y | m] =ᶠ[ae μ] μ[X | m]
refine_2 : μ[1 - Y | m] =ᶠ[ae μ] μ[1 - X | m]
⊢ μ[Y | m] * μ[1 - Y | m] =ᶠ[ae μ] μ[X | m] * μ[1 - X | m]

Tactic:
refine .mul ?_ ?_
-- Module: Mathlib.Probability.Distributions.TwoValued
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
h : ∀ (ω : Ω) (hω : X ω = Y ω), Y ω = X ω
⊢ Y =ᶠ[ae μ] X

Tactic:
filter_upwards [hXY] with ω hω
-- Module: Mathlib.Probability.Distributions.TwoValued
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
ω : Ω
hω : X ω = Y ω
⊢ Y ω = X ω

Tactic:
simp [hω]
-- Module: Mathlib.Probability.Distributions.TwoValued
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
⊢ μ[Y | m] =ᶠ[ae μ] μ[X | m]

Tactic:
exact condExp_congr_ae <| by filter_upwards [hXY] with ω hω; simp [hω]

Premises used: MeasureTheory.condExp_congr_ae
-- Module: Mathlib.Probability.Distributions.TwoValued
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
h : ∀ (ω : Ω) (hω : X ω = Y ω), HSub.hSub (α := Ω → ℝ) 1 Y ω = HSub.hSub (α := Ω → ℝ) 1 X ω
⊢ 1 - Y =ᶠ[ae μ] 1 - X

Tactic:
filter_upwards [hXY] with ω hω
-- Module: Mathlib.Probability.Distributions.TwoValued
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
ω : Ω
hω : X ω = Y ω
⊢ HSub.hSub (α := Ω → ℝ) 1 Y ω = HSub.hSub (α := Ω → ℝ) 1 X ω

Tactic:
simp [hω]
-- Module: Mathlib.Probability.Distributions.TwoValued
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
⊢ μ[1 - Y | m] =ᶠ[ae μ] μ[1 - X | m]

Tactic:
exact condExp_congr_ae <| by filter_upwards [hXY] with ω hω; simp [hω]

Premises used: MeasureTheory.condExp_congr_ae
-- Module: Mathlib.Probability.Distributions.TwoValued
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]
μ₂ : μ[Y | m] * μ[1 - Y | m] =ᶠ[ae μ] μ[X | m] * μ[1 - X | m]
⊢ Var[X; μ | 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ω]

Premises used: ProbabilityTheory.condVar_congr_ae
-- Module: Mathlib.Probability.Distributions.TwoValued
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
h : ∀ (a : Ω), X a = 0 ∨ X a = 1 → ‖X a‖ ≤ 1
⊢ ∀ᵐ (x : Ω) ∂μ, ‖X x‖ ≤ 1

Tactic:
filter_upwards [hX]
-- Module: Mathlib.Probability.Distributions.TwoValued
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
ω : Ω
hω : X ω = 0
⊢ ‖X ω‖ ≤ 1

Tactic:
simp [hω]
-- Module: Mathlib.Probability.Distributions.TwoValued
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
ω : Ω
hω : X ω = 1
⊢ ‖X ω‖ ≤ 1

Tactic:
simp [hω]
-- Module: Mathlib.Probability.Distributions.TwoValued
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

Tactic:
.sub ?_ ae_eq_rfl

Premises used: MeasureTheory.ae_eq_rfl, Filter.EventuallyEq.sub
-- Module: Mathlib.Probability.Distributions.TwoValued
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
refine : μ[HPow.hPow (β := ℕ) X 2 | m] =ᶠ[ae μ] μ[X | m]
⊢ μ[HPow.hPow (β := ℕ) X 2 | m] - HPow.hPow (β := ℕ) μ[X | m] 2 =ᶠ[ae μ] μ[X | m] - HPow.hPow (β := ℕ) μ[X | m] 2

Tactic:
refine .sub ?_ ae_eq_rfl
-- Module: Mathlib.Probability.Distributions.TwoValued
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
h : ∀ (a : Ω), X a = 0 ∨ X a = 1 → HPow.hPow (β := ℕ) X 2 a = X a
⊢ HPow.hPow (β := ℕ) X 2 =ᶠ[ae μ] X

Tactic:
filter_upwards [hX]
-- Module: Mathlib.Probability.Distributions.TwoValued
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
ω : Ω
hω : X ω = 0
⊢ HPow.hPow (β := ℕ) X 2 ω = X ω

Tactic:
simp [hω]
-- Module: Mathlib.Probability.Distributions.TwoValued
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
ω : Ω
hω : X ω = 1
⊢ HPow.hPow (β := ℕ) X 2 ω = X ω

Tactic:
simp [hω]
-- Module: Mathlib.Probability.Distributions.TwoValued
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] =ᶠ[ae μ] μ[X | m]

Tactic:
exact condExp_congr_ae <| by filter_upwards [hX]; rintro ω (hω | hω) <;> simp [hω]

Premises used: MeasureTheory.condExp_congr_ae
-- Module: Mathlib.Probability.Distributions.TwoValued
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
rw : μ[X | m] * (1 - μ[X | m]) =ᶠ[ae μ] μ[X | m] * μ[1 - X | m]
⊢ μ[X | m] - HPow.hPow (β := ℕ) μ[X | m] 2 =ᶠ[ae μ] μ[X | m] * μ[1 - X | m]

Tactic:
rw [sq, ← one_sub_mul, mul_comm]

Premises used: one_sub_mul, sq, mul_comm
-- Module: Mathlib.Probability.Distributions.TwoValued
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]

Tactic:
.mul ae_eq_rfl ?_

Premises used: MeasureTheory.ae_eq_rfl, Filter.EventuallyEq.mul
-- Module: Mathlib.Probability.Distributions.TwoValued
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
refine : 1 - μ[X | m] =ᶠ[ae μ] μ[1 - X | m]
⊢ μ[X | m] * (1 - μ[X | m]) =ᶠ[ae μ] μ[X | m] * μ[1 - X | m]

Tactic:
refine .mul ae_eq_rfl ?_
-- Module: Mathlib.Probability.Distributions.TwoValued
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]

Tactic:
simp [Pi.one_def, hm]

Premises used: Pi.one_def
-- Module: Mathlib.Probability.Distributions.TwoValued
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]

Tactic:
(condExp_sub (integrable_const _)
            (.of_bound (C := 1) hXmeas.aestronglyMeasurable ?_) _).symm

Premises used: Measurable.aestronglyMeasurable, MeasureTheory.Integrable.of_bound, OfNat.ofNat, MeasureTheory.condExp_sub, MeasureTheory.integrable_const, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Distributions.TwoValued
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
refine : ∀ᵐ (x : Ω) ∂μ, ‖X x‖ ≤ 1
⊢ μ[1 | m] - μ[X | m] =ᶠ[ae μ] μ[1 - X | m]

Tactic:
refine (condExp_sub (integrable_const _)
            (.of_bound (C := 1) hXmeas.aestronglyMeasurable ?_) _).symm

Premises used: Measurable.aestronglyMeasurable, MeasureTheory.Integrable.of_bound, OfNat.ofNat, MeasureTheory.condExp_sub, MeasureTheory.integrable_const, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Distributions.TwoValued
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 | m] - μ[X | m] =ᶠ[ae μ] μ[1 - X | m]
⊢ 1 - μ[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ω]
-- Module: Mathlib.Probability.Distributions.TwoValued
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
_₁ : μ[X | m] - HPow.hPow (β := ℕ) μ[X | m] 2 =ᶠ[ae μ] μ[X | m] * μ[1 - X | m]
⊢ Var[X; μ | m] =ᶠ[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ω]

Premises used: ProbabilityTheory.condVar_ae_eq_condExp_sq_sub_sq_condExp