Theorem: MeasureTheory.measureReal_union_null (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₁ : μ.real s₁ = 0
h₂ : μ.real s₂ = 0
⊢ μ.real (s₁ ∪ s₂) = 0
Tactic:
apply le_antisymm _ measureReal_nonneg
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h₁ : μ.real s₁ = 0
h₂ : μ.real s₂ = 0
⊢ μ.real (s₁ ∪ s₂) ≤ 0

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h₁ : μ.real s₁ = 0
h₂ : μ.real s₂ = 0
⊢ μ.real (s₁ ∪ s₂) ≤ 0
Tactic:
exact (measureReal_union_le s₁ s₂).trans (by simp [h₁, h₂])
State after:
no goals

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h₁ : μ.real s₁ = 0
h₂ : μ.real s₂ = 0
⊢ μ.real s₁ + μ.real s₂ ≤ 0
Tactic:
simp [h₁, h₂]
State after:
no goals