no goals
α : Type u_2
β : Type u_1
ι : Type ?u.980848
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
f : β → ℝ≥0∞
μ : MeasureTheory.Measure β
a : α
s : Set β
⊢ (∫⁻ (x : β) in s, f x ∂↑(const α μ) a) = ∫⁻ (x : β) in s, f x ∂μ
rw [kernel.const_apply]