Theorem: MeasureTheory.measureReal_diff_lt_of_lt_add (Carleson/ToMathlib/MeasureReal.lean)

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
hs : MeasurableSet s
hst : s ⊆ t
ε : ℝ
h : μ.real t < μ.real s + ε
ht' : autoParam (μ t ≠ ⊤) _auto✝
⊢ μ.real (t \ s) < ε
Tactic:
rw [measureReal_diff hst hs ht']
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
hs : MeasurableSet s
hst : s ⊆ t
ε : ℝ
h : μ.real t < μ.real s + ε
ht' : autoParam (μ t ≠ ⊤) _auto✝
⊢ μ.real t - μ.real s < ε

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
hs : MeasurableSet s
hst : s ⊆ t
ε : ℝ
h : μ.real t < μ.real s + ε
ht' : autoParam (μ t ≠ ⊤) _auto✝
⊢ μ.real t - μ.real s < ε
Tactic:
linarith
State after:
no goals