no goals
α : Type u_1
β : Type ?u.25758
γ : Type ?u.25761
δ : Type ?u.25764
ι : Type ?u.25767
R : Type ?u.25770
R' : Type ?u.25773
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
hs : MeasurableSet s
hst : s ⊆ t
hs' : ↑↑μ s ≠ ⊤
ε : ℝ≥0∞
⊢ ↑↑μ (t \ s) ≤ ε ↔ ↑↑μ t ≤ ↑↑μ s + ε
rw [measure_diff hst hs hs', tsub_le_iff_left]