no goals
α : Type u_1
β : Type u_2
ι : Type ?u.364824
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
h : κ = η
a : α
f : β → ℝ≥0∞
x✝ : Measurable f
⊢ (∫⁻ (b : β), f b ∂↑κ a) = ∫⁻ (b : β), f b ∂↑η a
rw [h]