Theorem: MeasureTheory.measureReal_diff_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₁ ∩ s₂) = 0
h' : autoParam (μ s₁ ≠ ⊤) _auto✝
⊢ μ.real (s₁ \ s₂) = μ.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 : Set α
h : μ.real (s₁ ∩ s₂) = 0
h' : autoParam (μ s₁ ≠ ⊤) _auto✝
⊢ (μ (s₁ \ s₂)).toReal = (μ s₁).toReal

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h : μ.real (s₁ ∩ s₂) = 0
h' : autoParam (μ s₁ ≠ ⊤) _auto✝
⊢ (μ (s₁ \ s₂)).toReal = (μ s₁).toReal
Tactic:
rw [measure_diff_null']
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h : μ.real (s₁ ∩ s₂) = 0
h' : autoParam (μ s₁ ≠ ⊤) _auto✝
⊢ μ (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₁ ∩ s₂) = 0
h' : autoParam (μ s₁ ≠ ⊤) _auto✝
⊢ μ (s₁ ∩ s₂) = 0
Tactic:
apply (measureReal_eq_zero_iff _).1 h
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h : μ.real (s₁ ∩ s₂) = 0
h' : autoParam (μ s₁ ≠ ⊤) _auto✝
⊢ μ (s₁ ∩ s₂) ≠ ⊤

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h : μ.real (s₁ ∩ s₂) = 0
h' : autoParam (μ s₁ ≠ ⊤) _auto✝
⊢ μ (s₁ ∩ s₂) ≠ ⊤
Tactic:
exact measure_ne_top_of_subset inter_subset_left h'
State after:
no goals