no goals
α : Type u_1
β : Type ?u.1690312
γ : Type ?u.1690315
δ : Type ?u.1690318
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
f : α → ℝ≥0∞
⊢ (∫⁻ (a : α), f a ∂dirac a) = f a
simp [lintegral_congr_ae (ae_eq_dirac f)]