no goals
α : Type u_1
E : Type u_2
F : Type ?u.1486181
𝕜 : Type ?u.1486184
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : SMulCommClass ℝ 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1488875
inst✝³ : TopologicalSpace X
inst✝² : FirstCountableTopology X
ν : Measure α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
f : α → E
a : α
⊢ (∫ (x : α), f a ∂Measure.dirac a) = f a
simp [Measure.dirac_apply_of_mem]