no goals
α : Type u_1
β : Type u_2
ι : Type ?u.398136
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
f : β → ℝ≥0∞
g : α → β
a : α
hg : Measurable g
inst✝ : MeasurableSingletonClass β
⊢ (∫⁻ (x : β), f x ∂↑(deterministic g hg) a) = f (g a)
rw [kernel.deterministic_apply, lintegral_dirac (g a) f]