Theorem: MeasureTheory.nonempty_inter_of_measureReal_lt_add' (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 α
m : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h's : s ⊆ u
h't : t ⊆ u
h : μ.real u < μ.real s + μ.real t
hu : autoParam (μ u ≠ ⊤) _auto✝
⊢ (s ∩ t).Nonempty
Tactic:
rw [add_comm] at h
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ✝ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h's : s ⊆ u
h't : t ⊆ u
h : μ.real u < μ.real t + μ.real s
hu : autoParam (μ u ≠ ⊤) _auto✝
⊢ (s ∩ t).Nonempty

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ✝ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h's : s ⊆ u
h't : t ⊆ u
h : μ.real u < μ.real t + μ.real s
hu : autoParam (μ u ≠ ⊤) _auto✝
⊢ (s ∩ t).Nonempty
Tactic:
rw [inter_comm]
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ✝ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h's : s ⊆ u
h't : t ⊆ u
h : μ.real u < μ.real t + μ.real s
hu : autoParam (μ u ≠ ⊤) _auto✝
⊢ (t ∩ s).Nonempty

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ✝ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h's : s ⊆ u
h't : t ⊆ u
h : μ.real u < μ.real t + μ.real s
hu : autoParam (μ u ≠ ⊤) _auto✝
⊢ (t ∩ s).Nonempty
Tactic:
exact nonempty_inter_of_measureReal_lt_add μ hs h't h's h hu
State after:
no goals