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

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

State before:
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t✝ s t u : Set α
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
hu : μ u = ⊤
⊢ μ.real (s ∆ u) ≤ μ.real (s ∆ t) + μ.real (t ∆ u)
Tactic:
have : μ (s ∆ u) = ∞ := measure_symmDiff_eq_top h₁ hu
State after:
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t✝ s t u : Set α
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
hu : μ u = ⊤
this : μ (s ∆ u) = ⊤
⊢ μ.real (s ∆ u) ≤ μ.real (s ∆ t) + μ.real (t ∆ u)

State before:
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t✝ s t u : Set α
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
hu : μ u = ⊤
this : μ (s ∆ u) = ⊤
⊢ μ.real (s ∆ u) ≤ μ.real (s ∆ t) + μ.real (t ∆ u)
Tactic:
simp only [measureReal_def, this, 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 t u : Set α
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
hu : μ u = ⊤
this : μ (s ∆ u) = ⊤
⊢ 0 ≤ (μ (s ∆ t)).toReal + (μ (t ∆ u)).toReal

State before:
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t✝ s t u : Set α
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
hu : μ u = ⊤
this : μ (s ∆ u) = ⊤
⊢ 0 ≤ (μ (s ∆ t)).toReal + (μ (t ∆ u)).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 t u : Set α
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
hu : μ u < ⊤
⊢ μ.real (s ∆ u) ≤ μ.real (s ∆ t) + μ.real (t ∆ u)
Tactic:
apply le_trans _ (measureReal_union_le (s ∆ t) (t ∆ u))
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t✝ s t u : Set α
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
hu : μ u < ⊤
⊢ μ.real (s ∆ u) ≤ μ.real (s ∆ t ∪ t ∆ u)

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t✝ s t u : Set α
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
hu : μ u < ⊤
⊢ μ.real (s ∆ u) ≤ μ.real (s ∆ t ∪ t ∆ u)
Tactic:
apply measureReal_mono (symmDiff_triangle s t u) ?_
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t✝ s t u : Set α
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
hu : μ u < ⊤
⊢ μ (s ∆ t ⊔ t ∆ u) ≠ ⊤

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t✝ s t u : Set α
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
hu : μ u < ⊤
⊢ μ (s ∆ t ⊔ t ∆ u) ≠ ⊤
Tactic:
exact measure_union_ne_top (measure_symmDiff_ne_top h₁ h₂) (measure_symmDiff_ne_top h₂ hu.ne)
State after:
no goals