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

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

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

State before:
case ha
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t s : Set α
ht : NullMeasurableSet t μ
h : autoParam (μ s ≠ ⊤) _auto✝
⊢ μ (s ∩ t) ≠ ⊤
Tactic:
exact measure_ne_top_of_subset inter_subset_left 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 s : Set α
ht : NullMeasurableSet t μ
h : autoParam (μ s ≠ ⊤) _auto✝
⊢ μ (s \ t) ≠ ⊤
Tactic:
exact measure_ne_top_of_subset diff_subset h
State after:
no goals