Theorem: MeasureTheory.measureReal_union_null_iff (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₁ : autoParam (μ s₁ ≠ ⊤) _auto✝
h₂ : autoParam (μ s₂ ≠ ⊤) _auto✝
⊢ μ.real (s₁ ∪ s₂) = 0 ↔ μ.real s₁ = 0 ∧ μ.real s₂ = 0
Tactic:
have : μ (s₁ ∪ s₂) ≠ ∞ := measure_union_ne_top h₁ h₂
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h₁ : autoParam (μ s₁ ≠ ⊤) _auto✝
h₂ : autoParam (μ s₂ ≠ ⊤) _auto✝
this : μ (s₁ ∪ s₂) ≠ ⊤
⊢ μ.real (s₁ ∪ s₂) = 0 ↔ μ.real s₁ = 0 ∧ μ.real s₂ = 0

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h₁ : autoParam (μ s₁ ≠ ⊤) _auto✝
h₂ : autoParam (μ s₂ ≠ ⊤) _auto✝
this : μ (s₁ ∪ s₂) ≠ ⊤
⊢ μ.real (s₁ ∪ s₂) = 0 ↔ μ.real s₁ = 0 ∧ μ.real s₂ = 0
Tactic:
refine ⟨fun h => ⟨?_, ?_⟩, fun h => measureReal_union_null h.1 h.2⟩
State after:
case refine_1
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h₁ : autoParam (μ s₁ ≠ ⊤) _auto✝
h₂ : autoParam (μ s₂ ≠ ⊤) _auto✝
this : μ (s₁ ∪ s₂) ≠ ⊤
h : μ.real (s₁ ∪ s₂) = 0
⊢ μ.real s₁ = 0

case refine_2
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h₁ : autoParam (μ s₁ ≠ ⊤) _auto✝
h₂ : autoParam (μ s₂ ≠ ⊤) _auto✝
this : μ (s₁ ∪ s₂) ≠ ⊤
h : μ.real (s₁ ∪ s₂) = 0
⊢ μ.real s₂ = 0

State before:
case refine_1
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h₁ : autoParam (μ s₁ ≠ ⊤) _auto✝
h₂ : autoParam (μ s₂ ≠ ⊤) _auto✝
this : μ (s₁ ∪ s₂) ≠ ⊤
h : μ.real (s₁ ∪ s₂) = 0
⊢ μ.real s₁ = 0
Tactic:
exact measureReal_mono_null subset_union_left h this
State after:
no goals

State before:
case refine_2
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h₁ : autoParam (μ s₁ ≠ ⊤) _auto✝
h₂ : autoParam (μ s₂ ≠ ⊤) _auto✝
this : μ (s₁ ∪ s₂) ≠ ⊤
h : μ.real (s₁ ∪ s₂) = 0
⊢ μ.real s₂ = 0
Tactic:
exact measureReal_mono_null subset_union_right h this
State after:
no goals