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]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
B : SimpleFunc Ω ℝ
p : ℝ≥0
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
h : Bernoulli B p μ
⊢ SimpleFunc.integral μ B = ↑p
no goals