no goals
α : Type u_1
β : Type ?u.1728971
γ : Type ?u.1728974
δ : Type ?u.1728977
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ (∫⁻ (x : α) in {a}, f x ∂μ) = f a * ↑↑μ {a}
simp only [restrict_singleton, lintegral_smul_measure, lintegral_dirac' _ hf, mul_comm]