Theorem: MeasureTheory.measureReal_le_measureReal_union_left (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 (μ t ≠ ⊤) _auto✝
⊢ μ.real s ≤ μ.real (s ∪ t)
Tactic:
rcases eq_top_or_lt_top (μ s) with hs|hs
State after:
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h : autoParam (μ t ≠ ⊤) _auto✝
hs : μ s = ⊤
⊢ μ.real s ≤ μ.real (s ∪ t)

case inr
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h : autoParam (μ t ≠ ⊤) _auto✝
hs : μ s < ⊤
⊢ μ.real s ≤ μ.real (s ∪ t)

State before:
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h : autoParam (μ t ≠ ⊤) _auto✝
hs : μ s = ⊤
⊢ μ.real s ≤ μ.real (s ∪ t)
Tactic:
simp [Measure.real, hs]
State after:
no goals

State before:
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h : autoParam (μ t ≠ ⊤) _auto✝
hs : μ s < ⊤
⊢ μ.real s ≤ μ.real (s ∪ t)
Tactic:
exact measureReal_mono subset_union_left (measure_union_lt_top hs h.lt_top).ne
State after:
no goals