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

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁✝ s₂✝ t s₁ s₂ : Set α
⊢ μ.real (s₁ ∪ s₂) ≤ μ.real s₁ + μ.real s₂
Tactic:
rcases eq_top_or_lt_top (μ (s₁ ∪ s₂)) with h|h
State after:
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁✝ s₂✝ t s₁ s₂ : Set α
h : μ (s₁ ∪ s₂) = ⊤
⊢ μ.real (s₁ ∪ s₂) ≤ μ.real s₁ + μ.real s₂

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

State before:
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁✝ s₂✝ t s₁ s₂ : Set α
h : μ (s₁ ∪ s₂) = ⊤
⊢ μ.real (s₁ ∪ s₂) ≤ μ.real s₁ + μ.real s₂
Tactic:
simp only [Measure.real, h, ENNReal.top_toReal]
State after:
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁✝ s₂✝ t s₁ s₂ : Set α
h : μ (s₁ ∪ s₂) = ⊤
⊢ 0 ≤ (μ s₁).toReal + (μ s₂).toReal

State before:
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁✝ s₂✝ t s₁ s₂ : Set α
h : μ (s₁ ∪ s₂) = ⊤
⊢ 0 ≤ (μ s₁).toReal + (μ s₂).toReal
Tactic:
exact add_nonneg ENNReal.toReal_nonneg ENNReal.toReal_nonneg
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 s₁ s₂ : Set α
h : μ (s₁ ∪ s₂) < ⊤
⊢ μ.real (s₁ ∪ s₂) ≤ μ.real s₁ + μ.real s₂
Tactic:
have A : μ s₁ ≠ ∞ := measure_ne_top_of_subset subset_union_left h.ne
State after:
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁✝ s₂✝ t s₁ s₂ : Set α
h : μ (s₁ ∪ s₂) < ⊤
A : μ s₁ ≠ ⊤
⊢ μ.real (s₁ ∪ s₂) ≤ μ.real s₁ + μ.real s₂

State before:
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁✝ s₂✝ t s₁ s₂ : Set α
h : μ (s₁ ∪ s₂) < ⊤
A : μ s₁ ≠ ⊤
⊢ μ.real (s₁ ∪ s₂) ≤ μ.real s₁ + μ.real s₂
Tactic:
have B : μ s₂ ≠ ∞ := measure_ne_top_of_subset subset_union_right h.ne
State after:
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁✝ s₂✝ t s₁ s₂ : Set α
h : μ (s₁ ∪ s₂) < ⊤
A : μ s₁ ≠ ⊤
B : μ s₂ ≠ ⊤
⊢ μ.real (s₁ ∪ s₂) ≤ μ.real s₁ + μ.real s₂

State before:
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁✝ s₂✝ t s₁ s₂ : Set α
h : μ (s₁ ∪ s₂) < ⊤
A : μ s₁ ≠ ⊤
B : μ s₂ ≠ ⊤
⊢ μ.real (s₁ ∪ s₂) ≤ μ.real s₁ + μ.real s₂
Tactic:
simp only [Measure.real, ← ENNReal.toReal_add A B]
State after:
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁✝ s₂✝ t s₁ s₂ : Set α
h : μ (s₁ ∪ s₂) < ⊤
A : μ s₁ ≠ ⊤
B : μ s₂ ≠ ⊤
⊢ (μ (s₁ ∪ s₂)).toReal ≤ (μ s₁ + μ s₂).toReal

State before:
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁✝ s₂✝ t s₁ s₂ : Set α
h : μ (s₁ ∪ s₂) < ⊤
A : μ s₁ ≠ ⊤
B : μ s₂ ≠ ⊤
⊢ (μ (s₁ ∪ s₂)).toReal ≤ (μ s₁ + μ s₂).toReal
Tactic:
exact ENNReal.toReal_mono (by simp [A, B]) (measure_union_le _ _)
State after:
no goals

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁✝ s₂✝ t s₁ s₂ : Set α
h : μ (s₁ ∪ s₂) < ⊤
A : μ s₁ ≠ ⊤
B : μ s₂ ≠ ⊤
⊢ μ s₁ + μ s₂ ≠ ⊤
Tactic:
simp [A, B]
State after:
no goals