no goals
α : Type u_1
β : Type ?u.119005
E : Type u_2
F : Type ?u.119011
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s✝ t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
e : E
s : Set α
s_meas : MeasurableSet s
⊢ (∫ (a : α), indicator s (fun x => e) a ∂μ) = ENNReal.toReal (↑↑μ s) • e
rw [integral_indicator s_meas, ← set_integral_const]