Theorem: MeasureTheory.measureReal_symmDiff_eq (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 α
hs : MeasurableSet s
ht : MeasurableSet t
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
⊢ μ.real (s ∆ t) = μ.real (s \ t) + μ.real (t \ s)
Tactic:
simp only [Measure.real]
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
⊢ (μ (s ∆ t)).toReal = (μ (s \ t)).toReal + (μ (t \ s)).toReal

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
⊢ (μ (s ∆ t)).toReal = (μ (s \ t)).toReal + (μ (t \ s)).toReal
Tactic:
rw [← ENNReal.toReal_add, measure_symmDiff_eq hs ht]
State after:
case ha
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
⊢ μ (s \ t) ≠ ⊤

case hb
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
⊢ μ (t \ s) ≠ ⊤

State before:
case ha
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
⊢ μ (s \ t) ≠ ⊤
Tactic:
exact measure_ne_top_of_subset diff_subset h₁
State after:
no goals

State before:
case hb
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
⊢ μ (t \ s) ≠ ⊤
Tactic:
exact measure_ne_top_of_subset diff_subset h₂
State after:
no goals