awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.SetBernoulli
Goal:
ι : Type u_1
u : Set ι
p : (↑I : Type)
inst : Countable ι
i : ι
hi : i ∉ u
i₁ :
  Eq (α := ℝ≥0∞) ((setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) ({s : Set ι | i ∈ s} ∩ {s : Set ι | i ∉ u}) : ℝ≥0∞)
    ((setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) {s : Set ι | i ∈ s} : ℝ≥0∞)
i₂ :
  Eq (α := ℝ≥0∞) ((setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) {s : Set ι | i ∈ s} : ℝ≥0∞)
    (((infinitePi (X := fun (i : ι) ↦ Prop) fun (i : ι) ↦
              HSMul.hSMul (β := Measure Prop) (toNNReal p) (dirac (i ∈ u)) +
                HSMul.hSMul (β := Measure Prop) (toNNReal (σ p)) (dirac False) :
            Measure ((i : ι) → Prop)) :
          (a : Set ((i : ι) → Prop)) → ℝ≥0∞)
        (cylinder (α := fun (i : ι) ↦ Prop) {i} {fun (x : ↥{i}) ↦ True}) :
      ℝ≥0∞)
i₃ :
  Eq (α := ℝ≥0∞)
    (((infinitePi (X := fun (i : ι) ↦ Prop) fun (i : ι) ↦
              HSMul.hSMul (β := Measure Prop) (toNNReal p) (dirac (i ∈ u)) +
                HSMul.hSMul (β := Measure Prop) (toNNReal (σ p)) (dirac False) :
            Measure ((i : ι) → Prop)) :
          (a : Set ((i : ι) → Prop)) → ℝ≥0∞)
        (cylinder (α := fun (i : ι) ↦ Prop) {i} {fun (x : ↥{i}) ↦ True}) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) ({a : Set ι | i ∈ a} ∩ {a : Set ι | i ∉ u}) : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
calc
    setBer(u, p) ({s | i ∈ s} ∩ {s | i ∉ u})
    _ = setBer(u, p) {s | i ∈ s} := by simp [hi]
    _ = infinitePi (fun i ↦ toNNReal p • dirac (i ∈ u) + toNNReal (σ p) • dirac False)
          (cylinder {i} {fun _ ↦ True}) := by
      rw [setBernoulli_apply']; congr!; ext; simp [funext_iff]
    _ = 0 := by simp [infinitePi_cylinder, hi]

Premises used: False, ProbabilityTheory.setBernoulli, setOf, Membership.mem, unitInterval.toNNReal, MeasureTheory.Measure.dirac, MeasureTheory.Measure.infinitePi, MeasureTheory.cylinder, Inter.inter, HAdd.hAdd, True, HSMul.hSMul, Singleton.singleton, unitInterval.symm, DFunLike.coe, Not
-- Module: Mathlib.Probability.Distributions.SetBernoulli
Goal:
ι : Type u_1
u : Set ι
p : (↑I : Type)
inst : Countable ι
simp simp₁ :
  ∀ (i : ι),
    Eq (α := ℝ≥0∞) ((setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) ({a : Set ι | i ∈ a} ∩ {a : Set ι | i ∉ u}) : ℝ≥0∞)
      (0 : ℝ≥0∞)
pos :
  ∀ (i : ι) (hi : i ∈ u),
    Eq (α := ℝ≥0∞) ((setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) ({a : Set ι | i ∈ a} ∩ {a : Set ι | i ∉ u}) : ℝ≥0∞)
      (0 : ℝ≥0∞)
neg neg₁ :
  ∀ (i : ι) (hi : i ∉ u),
    Eq (α := ℝ≥0∞) ((setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) ({a : Set ι | i ∈ a} ∩ {a : Set ι | i ∉ u}) : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ ∀ᵐ (s : Set ι) ∂setBer(u, p), s ⊆ u

Tactic:
classical
  simp only [Filter.Eventually, mem_ae_iff, Set.compl_setOf, Set.not_subset_iff_exists_mem_notMem,
    Set.setOf_exists, Set.setOf_and, measure_iUnion_null_iff]
  rintro i
  by_cases hi : i ∈ u
  · simp [*]
  calc
    setBer(u, p) ({s | i ∈ s} ∩ {s | i ∉ u})
    _ = setBer(u, p) {s | i ∈ s} := by simp [hi]
    _ = infinitePi (fun i ↦ toNNReal p • dirac (i ∈ u) + toNNReal (σ p) • dirac False)
          (cylinder {i} {fun _ ↦ True}) := by
      rw [setBernoulli_apply']; congr!; ext; simp [funext_iff]
    _ = 0 := by simp [infinitePi_cylinder, hi]

Premises used: Set.setOf_and, Set.not_subset_iff_exists_mem_notMem, Filter.Eventually, MeasureTheory.measure_iUnion_null_iff, Set.setOf_exists, MeasureTheory.mem_ae_iff, Set.compl_setOf
-- Module: Mathlib.Probability.Distributions.SetBernoulli
Goal:
ι : Type u_1
u : Set ι
inst : Countable ι
s : Set ι
p : (↑I : Type)
hs : ¬s ⊆ u
⊢ Subset (α := Set (Set ι)) {s} {x : Set ι | (fun (s : Set ι) ↦ s ⊆ u) x}ᶜ

Tactic:
simpa
-- Module: Mathlib.Probability.Distributions.SetBernoulli
Goal:
ι : Type u_1
inst : Countable ι
u : Set ι
p : (↑I : Type)
S : Set (Set ι)
⊢ {s : Set ι | s ∈ S ∧ s ⊆ u} ⊆ S

Tactic:
grind
-- Module: Mathlib.Probability.Distributions.SetBernoulli
Goal:
ι : Type u_1
inst : Countable ι
u : Set ι
p : (↑I : Type)
S : Set (Set ι)
apply : Eq (α := ℝ≥0∞) ((setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) (S \ {s : Set ι | s ∈ S ∧ s ⊆ u}) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) S : ℝ≥0∞)
    ((setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) {s : Set ι | s ∈ S ∧ s ⊆ u} : ℝ≥0∞)

Tactic:
apply (measure_eq_measure_of_null_diff (by grind) ?_).symm

Premises used: MeasureTheory.measure_eq_measure_of_null_diff, Eq.symm
-- Module: Mathlib.Probability.Distributions.SetBernoulli
Goal:
ι : Type u_1
inst : Countable ι
u : Set ι
p : (↑I : Type)
S : Set (Set ι)
⊢ S \ {s : Set ι | s ∈ S ∧ s ⊆ u} ⊆ {x : Set ι | (fun (s : Set ι) ↦ s ⊆ u) x}ᶜ

Tactic:
grind
-- Module: Mathlib.Probability.Distributions.SetBernoulli
Goal:
ι : Type u_1
inst : Countable ι
u : Set ι
p : (↑I : Type)
S : Set (Set ι)
⊢ Eq (α := ℝ≥0∞) ((setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) (S \ {s : Set ι | s ∈ S ∧ s ⊆ u}) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact Measure.mono_null (by grind) setBernoulli_ae_subset

Premises used: MeasureTheory.Measure.mono_null, ProbabilityTheory.setBernoulli_ae_subset
-- Module: Mathlib.Probability.Distributions.SetBernoulli
Goal:
ι : Type u_1
s u : Set ι
p : (↑I : Type)
inst : Countable ι
hsu : s ⊆ u
hu : u.Finite
⊢ u.Finite

Tactic:
hu
-- Module: Mathlib.Probability.Distributions.SetBernoulli
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 ι)),
    (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

Tactic:
lift u to Finset ι using hu

Premises used: Finset
-- Module: Mathlib.Probability.Distributions.SetBernoulli
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∞)

Tactic:
simp [setBernoulli_apply, Set.image_singleton, Set.indicator]

Premises used: Set.image_singleton, Set.indicator, ProbabilityTheory.setBernoulli_apply
-- Module: Mathlib.Probability.Distributions.SetBernoulli
Goal:
ι : Type u_1
s : Set ι
p : (↑I : Type)
inst : Countable ι
u : Finset ι
hsu : s ⊆ (↑u : Set ι)
rw :
  ∀ x ∈ u,
    ((if x ∈ u ↔ x ∈ s then (↑(toNNReal p) : ℝ≥0∞) else 0) + if x ∈ s then 0 else (↑(toNNReal (σ p)) : ℝ≥0∞)) =
      if x ∈ s then (↑(toNNReal p) : ℝ≥0∞) else (↑(toNNReal (σ p)) : ℝ≥0∞)
rw₁ :
  ∀ b ∉ u, ((if b ∈ u ↔ b ∈ s then (↑(toNNReal p) : ℝ≥0∞) else 0) + if b ∈ s then 0 else (↑(toNNReal (σ p)) : ℝ≥0∞)) = 1
⊢ 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:
rw [tprod_eq_prod, Finset.prod_congr rfl]

Premises used: Finset.prod_congr, tprod_eq_prod, rfl
-- Module: Mathlib.Probability.Distributions.SetBernoulli
Goal:
ι : Type u_1
s : Set ι
p : (↑I : Type)
inst : Countable ι
u : Finset ι
hsu : s ⊆ (↑u : Set ι)
⊢ ∀ x ∈ u,
    ((if x ∈ u ↔ x ∈ s then (↑(toNNReal p) : ℝ≥0∞) else 0) + if x ∈ s then 0 else (↑(toNNReal (σ p)) : ℝ≥0∞)) =
      if x ∈ s then (↑(toNNReal p) : ℝ≥0∞) else (↑(toNNReal (σ p)) : ℝ≥0∞)

Tactic:
simp +contextual [ite_add_ite, mt (@hsu _), ← ENNReal.coe_add]

Premises used: mt, ENNReal.coe_add, ite_add_ite
-- Module: Mathlib.Probability.Distributions.SetBernoulli
Goal:
ι : Type u_1
s : Set ι
p : (↑I : Type)
inst : Countable ι
u : Finset ι
hsu : s ⊆ (↑u : Set ι)
⊢ ∀ b ∉ u, ((if b ∈ u ↔ b ∈ s then (↑(toNNReal p) : ℝ≥0∞) else 0) + if b ∈ s then 0 else (↑(toNNReal (σ p)) : ℝ≥0∞)) = 1

Tactic:
simp +contextual [ite_add_ite, mt (@hsu _), ← ENNReal.coe_add]

Premises used: mt, ENNReal.coe_add, ite_add_ite
-- Module: Mathlib.Probability.Distributions.SetBernoulli
Goal:
ι : Type u_1
s : Set ι
p : (↑I : Type)
inst : Countable ι
u : Finset ι
hsu : s ⊆ (↑u : Set ι)
⊢ (∏ 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:
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]

Premises used: Iff.mpr, Set.setOf_and, Set.diff_eq_compl_inter, Set.inter_eq_right, Set.inter_comm, Finset.prod_ite, Set.ncard_coe_finset, Set.compl_setOf
-- Module: Mathlib.Probability.Distributions.SetBernoulli
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∞))
_₂ :
  (∏ 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
⊢ (setBer((↑u : Set ι), p) : (a : Set (Set ι)) → ℝ≥0∞) {s} =
    (↑(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]

Premises used: ProbabilityTheory.setBernoulli, unitInterval.toNNReal, SDiff.sdiff, Set.ncard, Singleton.singleton, unitInterval.symm, DFunLike.coe
-- Module: Mathlib.Probability.Distributions.SetBernoulli
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
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
⊢ (setBer(u, p) : (a : Set (Set ι)) → ℝ≥0∞) {s} =
    (↑(toNNReal p) : ℝ≥0∞) ^ s.ncard * (↑(toNNReal (σ p)) : ℝ≥0∞) ^ (u \ 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]

Premises used: Finset, ProbabilityTheory.setBernoulli, unitInterval.toNNReal, SDiff.sdiff, Set.ncard, Singleton.singleton, unitInterval.symm, DFunLike.coe
-- Module: Mathlib.Probability.Distributions.SetBernoulli
Goal:
ι : Type u_1
s u : Set ι
inst : Countable ι
p : (↑I : Type)
hsu : s ⊆ u
hu : u.Finite
⊢ setBer(u, p).real {s} = (↑p : ℝ) ^ s.ncard * (1 - (↑p : ℝ)) ^ (u \ s).ncard

Tactic:
simp [measureReal_def, setBernoulli_singleton p hsu hu]

Premises used: ProbabilityTheory.setBernoulli_singleton, MeasureTheory.measureReal_def
-- Module: Mathlib.Probability.Distributions.SetBernoulli
Goal:
ι : Type u_1
p : (↑I : Type)
inst : Countable ι
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∞)
⊢ Eq.{u_1 + 1} (α := Measure (Set ι)) setBer(∅, p) (dirac ∅)

Tactic:
ext s hs
-- Module: Mathlib.Probability.Distributions.SetBernoulli
Goal:
ι : Type u_1
p : (↑I : Type)
inst : Countable ι
s : Set (Set ι)
hs : MeasurableSet s
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∞)
⊢ Eq (α := ℝ≥0∞) (((setBer(∅, p) : Measure (Set ι)) : (a : Set (Set ι)) → ℝ≥0∞) s : ℝ≥0∞)
    (((dirac ∅ : Measure (Set ι)) : (a : Set (Set ι)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [setBernoulli_apply_eq_apply_subsets]

Premises used: ProbabilityTheory.setBernoulli_apply_eq_apply_subsets
-- Module: Mathlib.Probability.Distributions.SetBernoulli
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∞)
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∞)
⊢ 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
-- Module: Mathlib.Probability.Distributions.SetBernoulli
Goal:
ι : Type u_1
p : (↑I : Type)
inst : Countable ι
s : Set (Set ι)
hs : MeasurableSet s
h : ∅ ∈ s
⊢ Eq (α := Set (Set ι)) {t : Set ι | t ∈ s ∧ t ⊆ ∅} {∅}

Tactic:
grind
-- Module: Mathlib.Probability.Distributions.SetBernoulli
Goal:
ι : Type u_1
p : (↑I : Type)
inst : Countable ι
s : Set (Set ι)
hs : MeasurableSet s
h : ∅ ∈ s
⊢ Eq (α := Set (Set ι)) {t : Set ι | t ∈ s ∧ t ⊆ ∅} {∅}

Tactic:
have : {t | t ∈ s ∧ t ⊆ ∅} = {∅} := by grind
-- Module: Mathlib.Probability.Distributions.SetBernoulli
Goal:
ι : Type u_1
p : (↑I : Type)
inst : Countable ι
s : Set (Set ι)
hs : MeasurableSet s
h : ∅ ∈ s
this : Eq (α := 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∞)

Tactic:
simp_all
-- Module: Mathlib.Probability.Distributions.SetBernoulli
Goal:
ι : Type u_1
p : (↑I : Type)
inst : Countable ι
s : Set (Set ι)
hs : MeasurableSet s
h : ∅ ∉ s
⊢ Eq.{u_1 + 1} (α := Set (Set ι)) {t : Set ι | t ∈ s ∧ t ⊆ ∅} ∅

Tactic:
grind
-- Module: Mathlib.Probability.Distributions.SetBernoulli
Goal:
ι : Type u_1
p : (↑I : Type)
inst : Countable ι
s : Set (Set ι)
hs : MeasurableSet s
h : ∅ ∉ s
⊢ Eq.{u_1 + 1} (α := Set (Set ι)) {t : Set ι | t ∈ s ∧ t ⊆ ∅} ∅

Tactic:
have : {t | t ∈ s ∧ t ⊆ ∅} = ∅ := by grind
-- Module: Mathlib.Probability.Distributions.SetBernoulli
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 ⊆ ∅} ∅
neg :
  Eq (α := ℝ≥0∞) (((setBer(∅, p) : Measure (Set ι)) : (a : Set (Set ι)) → ℝ≥0∞) ∅ : ℝ≥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∞)

Tactic:
rw [this]
-- Module: Mathlib.Probability.Distributions.SetBernoulli
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∞) ∅ : ℝ≥0∞)
    (((dirac ∅ : Measure (Set ι)) : (a : Set (Set ι)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp_all
-- Module: Mathlib.Probability.Distributions.SetBernoulli
Goal:
ι : Type u_1
Ω : Type u_2
m : MeasurableSpace Ω
X Y : Ω → Set ι
u : Set ι
p : (↑I : Type)
P : Measure Ω
hXY : X =ᶠ[ae P] Y
⊢ IsSetBernoulli X u p P ↔ IsSetBernoulli Y u p P

Tactic:
hasLaw_congr hXY

Premises used: ProbabilityTheory.hasLaw_congr
-- Module: Mathlib.Probability.Distributions.SetBernoulli
Goal:
ι : Type u_1
Ω : Type u_2
m : MeasurableSpace Ω
X : Ω → Set ι
u : Set ι
p : (↑I : Type)
P : Measure Ω
inst : Countable ι
hX : IsSetBernoulli X u p P
⊢ Measurable (β := Prop) fun (x : Set ι) ↦ x ⊆ u

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.TwoValued
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hXmeas : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
⊢ AEStronglyMeasurable (m₀ := Real.measurableSpace) id (Measure.map X μ)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.TwoValued
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hXmeas : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
refine : (@integral _ _ _ _ Real.measurableSpace (Measure.map X μ) fun (y : ℝ) ↦ id y) = μ.real {ω : Ω | X ω = 1}
⊢ ∫ (x : Ω), X x ∂μ = μ.real {ω : Ω | X ω = 1}

Tactic:
refine (integral_map (f := id) hXmeas <| by fun_prop).symm.trans ?_

Premises used: MeasureTheory.integral_map, Eq.symm, Eq.trans
-- Module: Mathlib.Probability.Distributions.TwoValued
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hXmeas : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
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}
⊢ (@integral _ _ _ _ Real.measurableSpace (Measure.map X μ) fun (y : ℝ) ↦ id y) = μ.real {ω : Ω | X ω = 1}

Tactic:
rw [(Measure.ae_eq_or_eq_iff_map_eq_dirac_add_dirac hXmeas zero_ne_one).1 hX]

Premises used: MeasureTheory.Measure.ae_eq_or_eq_iff_map_eq_dirac_add_dirac, zero_ne_one, Iff.mp
-- Module: Mathlib.Probability.Distributions.TwoValued
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}
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}
⊢ ∫ (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} = ⊤

Premises used: setOf, OfNat.ofNat, Eq, DFunLike.coe
-- 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)
⊢ ∫ (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:
simp [h, Measure.real, Set.preimage, integral_undef, Integrable, HasFiniteIntegral]

Premises used: MeasureTheory.integral_undef, MeasureTheory.Measure.real, MeasureTheory.Integrable, Set.preimage, MeasureTheory.HasFiniteIntegral
-- 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)
⊢ AEStronglyMeasurable id
    (HSMul.hSMul (α := ENNReal) (β := Measure ℝ) ((μ : (a : Set Ω) → ENNReal) (X ⁻¹' {0}) : ENNReal) (Measure.dirac 0))

Tactic:
fun_prop
-- 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)
⊢ HasFiniteIntegral id
    (HSMul.hSMul (α := ENNReal) (β := Measure ℝ) ((μ : (a : Set Ω) → ENNReal) (X ⁻¹' {0}) : ENNReal) (Measure.dirac 0))

Tactic:
simp [HasFiniteIntegral]

Premises used: MeasureTheory.HasFiniteIntegral
-- 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)
⊢ @Integrable ℝ _ _ _ Real.measurableSpace id (Measure.dirac 1)

Tactic:
simp [integrable_dirac]

Premises used: MeasureTheory.integrable_dirac
-- 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)
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}
⊢ ∫ (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 [integral_add_measure ⟨by fun_prop, by simp [HasFiniteIntegral]⟩ <|
    .smul_measure (by simp [integrable_dirac]) h]

Premises used: MeasureTheory.integral_add_measure, And.intro