no goals
α : Type u_1
β : Type ?u.1688682
γ : Type ?u.1688685
δ : Type ?u.1688688
m : MeasurableSpace α
μ ν : Measure α
inst✝ : MeasurableSpace α
a : α
f : α → ℝ≥0∞
hf : Measurable f
⊢ (∫⁻ (a : α), f a ∂dirac a) = f a
simp [lintegral_congr_ae (ae_eq_dirac' hf)]