Theorem: MeasureTheory.le_measureReal_diff (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 α
h : autoParam (μ s₂ ≠ ⊤) _auto✝
⊢ μ.real s₁ - μ.real s₂ ≤ μ.real (s₁ \ s₂)
Tactic:
simp only [tsub_le_iff_left]
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h : autoParam (μ s₂ ≠ ⊤) _auto✝
⊢ μ.real s₁ ≤ μ.real s₂ + μ.real (s₁ \ s₂)

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h : autoParam (μ s₂ ≠ ⊤) _auto✝
⊢ μ.real s₁ ≤ μ.real s₂ + μ.real (s₁ \ s₂)
Tactic:
calc
  μ.real s₁ ≤ μ.real (s₂ ∪ s₁) := measureReal_le_measureReal_union_right h
  _ = μ.real (s₂ ∪ s₁ \ s₂) := congr_arg μ.real union_diff_self.symm
  _ ≤ μ.real s₂ + μ.real (s₁ \ s₂) := measureReal_union_le _ _
State after:
no goals