no goals
E : Type u_2
X : Type u_1
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace ℝ X
inst✝⁶ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
inst✝⁵ : MeasurableSpace E
μ : MeasureTheory.Measure E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : Measure.IsOpenPosMeasure μ
inst✝ : CompleteSpace X
z : X
⊢ (∫ (x : E), ContDiffBump.normed f μ x • z ∂μ) = z
simp_rw [integral_smul_const, f.integral_normed (μ := μ), one_smul]