no goals
α : Type u_1
β : Type ?u.294840
γ : Type ?u.294843
δ : Type ?u.294846
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s t : Set α
h : s =ᵐ[μ] t
⊢ (∫⁻ (x : α) in s, f x ∂μ) = ∫⁻ (x : α) in t, f x ∂μ
rw [Measure.restrict_congr_set h]