no goals
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_le : restrict μ s ≤ restrict ν s
h_meas_s : MeasurableSet s
⊢ ↑↑(μ - ν) s = 0
rw [← restrict_apply_self, restrict_sub_eq_restrict_sub_restrict, sub_eq_zero_of_le] <;> simp [*]