Theorem: Probly.flip_integral (Probly/Flip.lean)

State before:
W : Type ?u.3072
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type u_1
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.3307
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.3424
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.3541
inst✝¹ : MeasurableSpace α
β : Type ?u.3547
inst✝ : MeasurableSpace β
θ : ℝ
f : Bool → X
⊢ ∫ (x : Bool), f x ∂↑(flip θ).μ = θ • f true + (1 - θ) • f false
Tactic:
simp [flip,rand_simp]
State after:
no goals