Theorem: MeasureTheory.measureReal_le_measureReal_union_right (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 t ≤ μ.real (s ∪ t)
Tactic:
rw [union_comm]
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 t ≤ μ.real (t ∪ 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 t ≤ μ.real (t ∪ s)
Tactic:
exact measureReal_le_measureReal_union_left h
State after:
no goals