awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Distributions.SetBernoulli (goal)
Goal:
ι : Type u_1
s : Set ι
p : (↑I : Type)
inst : Countable ι
u : Finset ι
hsu : s ⊆ (↑u : Set ι)
_ :
  Eq (α := ℝ≥0∞) ((setBer((↑u : Set ι), p) : (a : Set (Set ι)) → ℝ≥0∞) {s} : ℝ≥0∞)
    (∏' (i : ι),
        ((if i ∈ u ↔ i ∈ s then (↑(toNNReal p) : ℝ≥0∞) else 0) + if i ∈ s then 0 else (↑(toNNReal (σ p)) : ℝ≥0∞)) :
      ℝ≥0∞)
⊢ (setBer((↑u : Set ι), p) : (a : Set (Set ι)) → ℝ≥0∞) {s} =
    (↑(toNNReal p) : ℝ≥0∞) ^ s.ncard * (↑(toNNReal (σ p)) : ℝ≥0∞) ^ ((↑u : Set ι) \ s).ncard
have _₁ : Eq (α := ℝ≥0∞)
  (∏' (i : ι),
    ((if i ∈ u ↔ i ∈ s then (↑(toNNReal p) : ℝ≥0∞) else 0) + if i ∈ s then 0 else (↑(toNNReal (σ p)) : ℝ≥0∞)))
  (∏ i ∈ u, if i ∈ s then (↑(toNNReal p) : ℝ≥0∞) else (↑(toNNReal (σ p)) : ℝ≥0∞))
Tactic: calc
    setBer(u, p) {s}
    _ = ∏' i, ((if i ∈ u ↔ i ∈ s then (toNNReal p : ℝ≥0∞) else 0) +
          if i ∈ s then 0 else (toNNReal (σ p) : ℝ≥0∞)) := by
      simp [setBernoulli_apply, Set.image_singleton, Set.indicator]
    _ = ∏ i ∈ u, (if i ∈ s then (toNNReal p : ℝ≥0∞) else (toNNReal (σ p) : ℝ≥0∞)) := by
      rw [tprod_eq_prod, Finset.prod_congr rfl] <;>
        simp +contextual [ite_add_ite, mt (@hsu _), ← ENNReal.coe_add]
    _ = toNNReal p ^ s.ncard * toNNReal (σ p) ^ (↑u \ s).ncard := by
      simp [Finset.prod_ite, ← Set.ncard_coe_finset, Set.setOf_and,
        Set.inter_eq_right.2 hsu, ← Set.compl_setOf, Set.diff_eq_compl_inter, Set.inter_comm]
-- Lean 4 proof step from Mathlib.Probability.Distributions.SetBernoulli (goal)
Goal:
ι : Type u_1
s : Set ι
p : (↑I : Type)
inst : Countable ι
u : Finset ι
hsu : s ⊆ (↑u : Set ι)
_ :
  Eq (α := ℝ≥0∞) ((setBer((↑u : Set ι), p) : (a : Set (Set ι)) → ℝ≥0∞) {s} : ℝ≥0∞)
    (∏' (i : ι),
        ((if i ∈ u ↔ i ∈ s then (↑(toNNReal p) : ℝ≥0∞) else 0) + if i ∈ s then 0 else (↑(toNNReal (σ p)) : ℝ≥0∞)) :
      ℝ≥0∞)
_₁ :
  Eq (α := ℝ≥0∞)
    (∏' (i : ι),
      ((if i ∈ u ↔ i ∈ s then (↑(toNNReal p) : ℝ≥0∞) else 0) + if i ∈ s then 0 else (↑(toNNReal (σ p)) : ℝ≥0∞)))
    (∏ i ∈ u, if i ∈ s then (↑(toNNReal p) : ℝ≥0∞) else (↑(toNNReal (σ p)) : ℝ≥0∞))
⊢ (setBer((↑u : Set ι), p) : (a : Set (Set ι)) → ℝ≥0∞) {s} =
    (↑(toNNReal p) : ℝ≥0∞) ^ s.ncard * (↑(toNNReal (σ p)) : ℝ≥0∞) ^ ((↑u : Set ι) \ s).ncard
have _₂ : (∏ i ∈ u, if i ∈ s then (↑(toNNReal p) : ℝ≥0∞) else (↑(toNNReal (σ p)) : ℝ≥0∞)) =
  (↑(toNNReal p) : ℝ≥0∞) ^ s.ncard * (↑(toNNReal (σ p)) : ℝ≥0∞) ^ ((↑u : Set ι) \ s).ncard
Tactic: calc
    setBer(u, p) {s}
    _ = ∏' i, ((if i ∈ u ↔ i ∈ s then (toNNReal p : ℝ≥0∞) else 0) +
          if i ∈ s then 0 else (toNNReal (σ p) : ℝ≥0∞)) := by
      simp [setBernoulli_apply, Set.image_singleton, Set.indicator]
    _ = ∏ i ∈ u, (if i ∈ s then (toNNReal p : ℝ≥0∞) else (toNNReal (σ p) : ℝ≥0∞)) := by
      rw [tprod_eq_prod, Finset.prod_congr rfl] <;>
        simp +contextual [ite_add_ite, mt (@hsu _), ← ENNReal.coe_add]
    _ = toNNReal p ^ s.ncard * toNNReal (σ p) ^ (↑u \ s).ncard := by
      simp [Finset.prod_ite, ← Set.ncard_coe_finset, Set.setOf_and,
        Set.inter_eq_right.2 hsu, ← Set.compl_setOf, Set.diff_eq_compl_inter, Set.inter_comm]
-- Lean 4 proof step from Mathlib.Probability.Distributions.SetBernoulli (goal)
Goal:
ι : Type u_1
s u : Set ι
p : (↑I : Type)
inst : Countable ι
hsu : s ⊆ u
hu : u.Finite
⊢ (setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) {s} =
    (↑(toNNReal p) : ℝ≥0∞) ^ s.ncard * (↑(toNNReal (σ p)) : ℝ≥0∞) ^ (u \ s).ncard
have lift : ∀ (u : Finset ι) (hsu : s ⊆ (↑u : Set ι)) (hu : (↑u : Set ι).Finite),
  (setBer((↑u : Set ι), p) : (a : Set (Set ι)) → ℝ≥0∞) {s} =
    (↑(toNNReal p) : ℝ≥0∞) ^ s.ncard * (↑(toNNReal (σ p)) : ℝ≥0∞) ^ ((↑u : Set ι) \ s).ncard
Tactic: classical
  lift u to Finset ι using hu
  calc
    setBer(u, p) {s}
    _ = ∏' i, ((if i ∈ u ↔ i ∈ s then (toNNReal p : ℝ≥0∞) else 0) +
          if i ∈ s then 0 else (toNNReal (σ p) : ℝ≥0∞)) := by
      simp [setBernoulli_apply, Set.image_singleton, Set.indicator]
    _ = ∏ i ∈ u, (if i ∈ s then (toNNReal p : ℝ≥0∞) else (toNNReal (σ p) : ℝ≥0∞)) := by
      rw [tprod_eq_prod, Finset.prod_congr rfl] <;>
        simp +contextual [ite_add_ite, mt (@hsu _), ← ENNReal.coe_add]
    _ = toNNReal p ^ s.ncard * toNNReal (σ p) ^ (↑u \ s).ncard := by
      simp [Finset.prod_ite, ← Set.ncard_coe_finset, Set.setOf_and,
        Set.inter_eq_right.2 hsu, ← Set.compl_setOf, Set.diff_eq_compl_inter, Set.inter_comm]
Cleared hypotheses: u, hsu, hu
-- Lean 4 proof step from Mathlib.Probability.Distributions.SetBernoulli (goal)
Goal:
ι : Type u_1
s u : Set ι
p : (↑I : Type)
inst : Countable ι
hsu : s ⊆ u
hu : u.Finite
lift :
  ∀ (u : Finset ι) (hsu : s ⊆ (↑u : Set ι)) (hu : (↑u : Set ι).Finite),
    (setBer((↑u : Set ι), p) : (a : Set (Set ι)) → ℝ≥0∞) {s} =
      (↑(toNNReal p) : ℝ≥0∞) ^ s.ncard * (↑(toNNReal (σ p)) : ℝ≥0∞) ^ ((↑u : Set ι) \ s).ncard
⊢ (setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) {s} =
    (↑(toNNReal p) : ℝ≥0∞) ^ s.ncard * (↑(toNNReal (σ p)) : ℝ≥0∞) ^ (u \ s).ncard
have lift₁ : ∀ (u : Finset ι) (hsu : s ⊆ (↑u : Set ι)),
  (setBer((↑u : Set ι), p) : (a : Set (Set ι)) → ℝ≥0∞) {s} =
    (↑(toNNReal p) : ℝ≥0∞) ^ s.ncard * (↑(toNNReal (σ p)) : ℝ≥0∞) ^ ((↑u : Set ι) \ s).ncard
Tactic: classical
  lift u to Finset ι using hu
  calc
    setBer(u, p) {s}
    _ = ∏' i, ((if i ∈ u ↔ i ∈ s then (toNNReal p : ℝ≥0∞) else 0) +
          if i ∈ s then 0 else (toNNReal (σ p) : ℝ≥0∞)) := by
      simp [setBernoulli_apply, Set.image_singleton, Set.indicator]
    _ = ∏ i ∈ u, (if i ∈ s then (toNNReal p : ℝ≥0∞) else (toNNReal (σ p) : ℝ≥0∞)) := by
      rw [tprod_eq_prod, Finset.prod_congr rfl] <;>
        simp +contextual [ite_add_ite, mt (@hsu _), ← ENNReal.coe_add]
    _ = toNNReal p ^ s.ncard * toNNReal (σ p) ^ (↑u \ s).ncard := by
      simp [Finset.prod_ite, ← Set.ncard_coe_finset, Set.setOf_and,
        Set.inter_eq_right.2 hsu, ← Set.compl_setOf, Set.diff_eq_compl_inter, Set.inter_comm]
Cleared hypotheses: u, hsu, hu
-- Lean 4 proof step from Mathlib.Probability.Distributions.SetBernoulli (goal)
Goal:
ι : Type u_1
p : (↑I : Type)
inst : Countable ι
⊢ Eq.{u_1 + 1} (α := Measure (Set ι)) setBer(∅, p) (dirac ∅)
have h : ∀ (s : Set (Set ι)) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((setBer(∅, p) : Measure (Set ι)) : (a : Set (Set ι)) → ℝ≥0∞) s : ℝ≥0∞)
    (((dirac ∅ : Measure (Set ι)) : (a : Set (Set ι)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.Probability.Distributions.SetBernoulli (goal)
Goal:
ι : Type u_1
p : (↑I : Type)
inst : Countable ι
s : Set (Set ι)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((setBer(∅, p) : Measure (Set ι)) : (a : Set (Set ι)) → ℝ≥0∞) s : ℝ≥0∞)
    (((dirac ∅ : Measure (Set ι)) : (a : Set (Set ι)) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) (((setBer(∅, p) : Measure (Set ι)) : (a : Set (Set ι)) → ℝ≥0∞) {s_1 : Set ι | s_1 ∈ s ∧ s_1 ⊆ ∅} : ℝ≥0∞)
  (((dirac ∅ : Measure (Set ι)) : (a : Set (Set ι)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [setBernoulli_apply_eq_apply_subsets]
-- Lean 4 proof step from Mathlib.Probability.Distributions.SetBernoulli (goal)
Goal:
ι : Type u_1
p : (↑I : Type)
inst : Countable ι
s : Set (Set ι)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    (((setBer(∅, p) : Measure (Set ι)) : (a : Set (Set ι)) → ℝ≥0∞) {s_1 : Set ι | s_1 ∈ s ∧ s_1 ⊆ ∅} : ℝ≥0∞)
    (((dirac ∅ : Measure (Set ι)) : (a : Set (Set ι)) → ℝ≥0∞) s : ℝ≥0∞)
have pos : ∀ (h : ∅ ∈ s),
  Eq (α := ℝ≥0∞)
    (((setBer(∅, p) : Measure (Set ι)) : (a : Set (Set ι)) → ℝ≥0∞) {s_1 : Set ι | s_1 ∈ s ∧ s_1 ⊆ ∅} : ℝ≥0∞)
    (((dirac ∅ : Measure (Set ι)) : (a : Set (Set ι)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: by_cases h : ∅ ∈ s
-- Lean 4 proof step from Mathlib.Probability.Distributions.SetBernoulli (goal)
Goal:
ι : Type u_1
p : (↑I : Type)
inst : Countable ι
s : Set (Set ι)
hs : MeasurableSet s
pos :
  ∀ (h : ∅ ∈ s),
    Eq (α := ℝ≥0∞)
      (((setBer(∅, p) : Measure (Set ι)) : (a : Set (Set ι)) → ℝ≥0∞) {s_1 : Set ι | s_1 ∈ s ∧ s_1 ⊆ ∅} : ℝ≥0∞)
      (((dirac ∅ : Measure (Set ι)) : (a : Set (Set ι)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((setBer(∅, p) : Measure (Set ι)) : (a : Set (Set ι)) → ℝ≥0∞) {s_1 : Set ι | s_1 ∈ s ∧ s_1 ⊆ ∅} : ℝ≥0∞)
    (((dirac ∅ : Measure (Set ι)) : (a : Set (Set ι)) → ℝ≥0∞) s : ℝ≥0∞)
have neg : ∀ (h : ∅ ∉ s),
  Eq (α := ℝ≥0∞)
    (((setBer(∅, p) : Measure (Set ι)) : (a : Set (Set ι)) → ℝ≥0∞) {s_1 : Set ι | s_1 ∈ s ∧ s_1 ⊆ ∅} : ℝ≥0∞)
    (((dirac ∅ : Measure (Set ι)) : (a : Set (Set ι)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: by_cases h : ∅ ∈ s
-- Lean 4 proof step from Mathlib.Probability.Distributions.SetBernoulli (hypothesis)
Goal:
ι : Type u_1
p : (↑I : Type)
inst : Countable ι
s : Set (Set ι)
hs : MeasurableSet s
h : ∅ ∈ s
⊢ Eq (α := ℝ≥0∞)
    (((setBer(∅, p) : Measure (Set ι)) : (a : Set (Set ι)) → ℝ≥0∞) {s_1 : Set ι | s_1 ∈ s ∧ s_1 ⊆ ∅} : ℝ≥0∞)
    (((dirac ∅ : Measure (Set ι)) : (a : Set (Set ι)) → ℝ≥0∞) s : ℝ≥0∞)
have this : Eq (α := Set (Set ι)) {t : Set ι | t ∈ s ∧ t ⊆ ∅} {∅}
Tactic: have : {t | t ∈ s ∧ t ⊆ ∅} = {∅} := by grind
-- Lean 4 proof step from Mathlib.Probability.Distributions.SetBernoulli (hypothesis)
Goal:
ι : Type u_1
p : (↑I : Type)
inst : Countable ι
s : Set (Set ι)
hs : MeasurableSet s
h : ∅ ∉ s
⊢ Eq (α := ℝ≥0∞)
    (((setBer(∅, p) : Measure (Set ι)) : (a : Set (Set ι)) → ℝ≥0∞) {s_1 : Set ι | s_1 ∈ s ∧ s_1 ⊆ ∅} : ℝ≥0∞)
    (((dirac ∅ : Measure (Set ι)) : (a : Set (Set ι)) → ℝ≥0∞) s : ℝ≥0∞)
have this : Eq.{u_1 + 1} (α := Set (Set ι)) {t : Set ι | t ∈ s ∧ t ⊆ ∅} ∅
Tactic: have : {t | t ∈ s ∧ t ⊆ ∅} = ∅ := by grind
-- Lean 4 proof step from Mathlib.Probability.Distributions.SetBernoulli (goal)
Goal:
ι : Type u_1
p : (↑I : Type)
inst : Countable ι
s : Set (Set ι)
hs : MeasurableSet s
h : ∅ ∉ s
this : Eq.{u_1 + 1} (α := Set (Set ι)) {t : Set ι | t ∈ s ∧ t ⊆ ∅} ∅
⊢ Eq (α := ℝ≥0∞)
    (((setBer(∅, p) : Measure (Set ι)) : (a : Set (Set ι)) → ℝ≥0∞) {s_1 : Set ι | s_1 ∈ s ∧ s_1 ⊆ ∅} : ℝ≥0∞)
    (((dirac ∅ : Measure (Set ι)) : (a : Set (Set ι)) → ℝ≥0∞) s : ℝ≥0∞)
have neg : Eq (α := ℝ≥0∞) (((setBer(∅, p) : Measure (Set ι)) : (a : Set (Set ι)) → ℝ≥0∞) ∅ : ℝ≥0∞)
  (((dirac ∅ : Measure (Set ι)) : (a : Set (Set ι)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Probability.Distributions.TwoValued (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hXmeas : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
⊢ ∫ (x : Ω), X x ∂μ = μ.real {ω : Ω | X ω = 1}
have refine : (@integral _ _ _ _ Real.measurableSpace (Measure.map X μ) fun (y : ℝ) ↦ id y) = μ.real {ω : Ω | X ω = 1}
Tactic: refine (integral_map (f := id) hXmeas <| by fun_prop).symm.trans ?_
-- Lean 4 proof step from Mathlib.Probability.Distributions.TwoValued (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hXmeas : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
⊢ (@integral _ _ _ _ Real.measurableSpace (Measure.map X μ) fun (y : ℝ) ↦ id y) = μ.real {ω : Ω | X ω = 1}
have rw : ∫ (y : ℝ),
    id
      y ∂(HSMul.hSMul (α := ENNReal) (β := Measure ℝ) ((μ : (a : Set Ω) → ENNReal) (X ⁻¹' {0}) : ENNReal)
        (Measure.dirac 0) +
      HSMul.hSMul (α := ENNReal) (β := Measure ℝ) ((μ : (a : Set Ω) → ENNReal) (X ⁻¹' {1}) : ENNReal)
        (Measure.dirac 1)) =
  μ.real {ω : Ω | X ω = 1}
Tactic: rw [(Measure.ae_eq_or_eq_iff_map_eq_dirac_add_dirac hXmeas zero_ne_one).1 hX]
-- Lean 4 proof step from Mathlib.Probability.Distributions.TwoValued (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hXmeas : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
⊢ ∫ (y : ℝ),
      id
        y ∂(HSMul.hSMul (α := ENNReal) (β := Measure ℝ) ((μ : (a : Set Ω) → ENNReal) (X ⁻¹' {0}) : ENNReal)
          (Measure.dirac 0) +
        HSMul.hSMul (α := ENNReal) (β := Measure ℝ) ((μ : (a : Set Ω) → ENNReal) (X ⁻¹' {1}) : ENNReal)
          (Measure.dirac 1)) =
    μ.real {ω : Ω | X ω = 1}
have pos : ∀ (h : Eq (α := ENNReal) ((μ : (a : Set Ω) → ENNReal) {ω : Ω | X ω = 1} : ENNReal) (⊤ : ENNReal)),
  ∫ (y : ℝ),
      id
        y ∂(HSMul.hSMul (α := ENNReal) (β := Measure ℝ) ((μ : (a : Set Ω) → ENNReal) (X ⁻¹' {0}) : ENNReal)
          (Measure.dirac 0) +
        HSMul.hSMul (α := ENNReal) (β := Measure ℝ) ((μ : (a : Set Ω) → ENNReal) (X ⁻¹' {1}) : ENNReal)
          (Measure.dirac 1)) =
    μ.real {ω : Ω | X ω = 1}
Tactic: by_cases h : μ {ω | X ω = 1} = ⊤
-- Lean 4 proof step from Mathlib.Probability.Distributions.TwoValued (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hXmeas : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
pos :
  ∀ (h : Eq (α := ENNReal) ((μ : (a : Set Ω) → ENNReal) {ω : Ω | X ω = 1} : ENNReal) (⊤ : ENNReal)),
    ∫ (y : ℝ),
        id
          y ∂(HSMul.hSMul (α := ENNReal) (β := Measure ℝ) ((μ : (a : Set Ω) → ENNReal) (X ⁻¹' {0}) : ENNReal)
            (Measure.dirac 0) +
          HSMul.hSMul (α := ENNReal) (β := Measure ℝ) ((μ : (a : Set Ω) → ENNReal) (X ⁻¹' {1}) : ENNReal)
            (Measure.dirac 1)) =
      μ.real {ω : Ω | X ω = 1}
⊢ ∫ (y : ℝ),
      id
        y ∂(HSMul.hSMul (α := ENNReal) (β := Measure ℝ) ((μ : (a : Set Ω) → ENNReal) (X ⁻¹' {0}) : ENNReal)
          (Measure.dirac 0) +
        HSMul.hSMul (α := ENNReal) (β := Measure ℝ) ((μ : (a : Set Ω) → ENNReal) (X ⁻¹' {1}) : ENNReal)
          (Measure.dirac 1)) =
    μ.real {ω : Ω | X ω = 1}
have neg : ∀ (h : ¬Eq (α := ENNReal) ((μ : (a : Set Ω) → ENNReal) {ω : Ω | X ω = 1} : ENNReal) (⊤ : ENNReal)),
  ∫ (y : ℝ),
      id
        y ∂(HSMul.hSMul (α := ENNReal) (β := Measure ℝ) ((μ : (a : Set Ω) → ENNReal) (X ⁻¹' {0}) : ENNReal)
          (Measure.dirac 0) +
        HSMul.hSMul (α := ENNReal) (β := Measure ℝ) ((μ : (a : Set Ω) → ENNReal) (X ⁻¹' {1}) : ENNReal)
          (Measure.dirac 1)) =
    μ.real {ω : Ω | X ω = 1}
Tactic: by_cases h : μ {ω | X ω = 1} = ⊤
-- Lean 4 proof step from Mathlib.Probability.Distributions.TwoValued (goal)
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)
⊢ ∫ (y : ℝ),
      id
        y ∂(HSMul.hSMul (α := ENNReal) (β := Measure ℝ) ((μ : (a : Set Ω) → ENNReal) (X ⁻¹' {0}) : ENNReal)
          (Measure.dirac 0) +
        HSMul.hSMul (α := ENNReal) (β := Measure ℝ) ((μ : (a : Set Ω) → ENNReal) (X ⁻¹' {1}) : ENNReal)
          (Measure.dirac 1)) =
    μ.real {ω : Ω | X ω = 1}
have neg : 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: rw [integral_add_measure ⟨by fun_prop, by simp [HasFiniteIntegral]⟩ <|
    .smul_measure (by simp [integrable_dirac]) h]
-- Lean 4 proof step from Mathlib.Probability.Distributions.TwoValued (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hXmeas : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
⊢ ∫ (ω : Ω), 1 - X ω ∂μ = μ.real {ω : Ω | X ω = 0}
have _ : μ.real {ω : Ω | 1 - X ω = 1} = μ.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
-- 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 : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
⊢ Var[X; μ | m] =ᶠ[ae μ] μ[X | m] * μ[1 - X | m]
have 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]
Tactic: wlog hXmeas : Measurable[m₀] X
-- 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 : 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]
⊢ Var[X; μ | m] =ᶠ[ae μ] μ[X | m] * μ[1 - X | m]
have 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]
Tactic: wlog hXmeas : Measurable[m₀] X
Cleared hypotheses: m₀, hm, μ, inst, hXmeas, hX
-- 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
⊢ Var[X; μ | m] =ᶠ[ae μ] μ[X | m] * μ[1 - X | m]
have inr : ∀ (Y : Ω → ℝ) (hYmeas : Measurable Y) (hXY : X =ᶠ[ae μ] Y), Var[X; μ | m] =ᶠ[ae μ] μ[X | m] * μ[1 - X | m]
Tactic: obtain ⟨Y, hYmeas, hXY⟩ := ‹AEMeasurable[m₀] X μ›
-- 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]
have refine : ∀ᵐ (ω : Ω) ∂μ, Y ω = 0 ∨ Y ω = 1
Tactic: refine this hm hYmeas.aemeasurable ?_ hYmeas
-- 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
⊢ ∀ᵐ (ω : Ω) ∂μ, Y ω = 0 ∨ Y ω = 1
have h : ∀ (ω : Ω) (hXω : X ω = 0 ∨ X ω = 1) (hXYω : X ω = Y ω), Y ω = 0 ∨ Y ω = 1
Tactic: filter_upwards [hX, hXY] with ω hXω hXYω
-- 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
⊢ μ[Y | m] * μ[1 - Y | m] =ᶠ[ae μ] μ[X | m] * μ[1 - X | m]
have refine_1 : μ[Y | m] =ᶠ[ae μ] μ[X | m]
Tactic: refine .mul ?_ ?_
-- 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
refine_1 : μ[Y | m] =ᶠ[ae μ] μ[X | m]
⊢ μ[Y | m] * μ[1 - Y | m] =ᶠ[ae μ] μ[X | m] * μ[1 - X | m]
have refine_2 : μ[1 - Y | m] =ᶠ[ae μ] μ[1 - X | m]
Tactic: refine .mul ?_ ?_
-- 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
⊢ Y =ᶠ[ae μ] X
have h : ∀ (ω : Ω) (hω : X ω = Y ω), Y ω = X ω
Tactic: filter_upwards [hXY] with ω hω
-- 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
⊢ 1 - Y =ᶠ[ae μ] 1 - X
have h : ∀ (ω : Ω) (hω : X ω = Y ω), HSub.hSub (α := Ω → ℝ) 1 Y ω = HSub.hSub (α := Ω → ℝ) 1 X ω
Tactic: filter_upwards [hXY] with ω hω
-- 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[X; μ | m] =ᶠ[ae μ] μ[X | m] * μ[1 - X | m]
have μ₁ : Var[Y; μ | m] =ᶠ[ae μ] μ[Y | m] * μ[1 - Y | 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ω]