Theorem: bernoulli_expectation (RandomGraphs/bernoulli.lean)

State before:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
B : SimpleFunc Ω ℝ
p : ℝ≥0
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
h : Bernoulli B p μ
⊢ ∫ (ω : Ω), ↑B ω ∂μ = ↑p
Tactic:
rw [←SimpleFunc.integral_eq_integral B (integrable B μ)]
State after:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
B : SimpleFunc Ω ℝ
p : ℝ≥0
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
h : Bernoulli B p μ
⊢ SimpleFunc.integral μ B = ↑p

State before:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
B : SimpleFunc Ω ℝ
p : ℝ≥0
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
h : Bernoulli B p μ
⊢ SimpleFunc.integral μ B = ↑p
Tactic:
simp only [SimpleFunc.integral_eq, h.range, Finset.mem_singleton, zero_ne_one, smul_eq_mul,
  not_false_eq_true, Finset.sum_insert, mul_zero, Finset.sum_singleton, h.prob_1,
  ENNReal.coe_toReal, mul_one, zero_add]
State after:
no goals