Theorem: MeasureTheory.exists_nonempty_inter_of_measureReal_univ_lt_sum_measureReal (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 α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : μ.real univ < ∑ i ∈ s, μ.real (t i)
⊢ ∃ i ∈ s, ∃ j ∈ s, ∃ (_ : i ≠ j), (t i ∩ t j).Nonempty
Tactic:
apply exists_nonempty_inter_of_measure_univ_lt_sum_measure μ 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 α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : μ.real univ < ∑ i ∈ s, μ.real (t i)
⊢ μ univ < ∑ i ∈ s, μ (t i)

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ✝ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : μ.real univ < ∑ i ∈ s, μ.real (t i)
⊢ μ univ < ∑ i ∈ s, μ (t i)
Tactic:
apply (ENNReal.toReal_lt_toReal (measure_ne_top _ _) _).1
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ✝ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : μ.real univ < ∑ i ∈ s, μ.real (t i)
⊢ (μ univ).toReal < (∑ i ∈ s, μ (t i)).toReal

ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ✝ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : μ.real univ < ∑ i ∈ s, μ.real (t i)
⊢ ∑ i ∈ s, μ (t i) ≠ ⊤

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ✝ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : μ.real univ < ∑ i ∈ s, μ.real (t i)
⊢ (μ univ).toReal < (∑ i ∈ s, μ (t i)).toReal
Tactic:
convert H
State after:
case h.e'_4
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ✝ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : μ.real univ < ∑ i ∈ s, μ.real (t i)
⊢ (∑ i ∈ s, μ (t i)).toReal = ∑ i ∈ s, μ.real (t i)

State before:
case h.e'_4
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ✝ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : μ.real univ < ∑ i ∈ s, μ.real (t i)
⊢ (∑ i ∈ s, μ (t i)).toReal = ∑ i ∈ s, μ.real (t i)
Tactic:
rw [ENNReal.toReal_sum (fun i hi ↦ measure_ne_top _ _)]
State after:
case h.e'_4
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ✝ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : μ.real univ < ∑ i ∈ s, μ.real (t i)
⊢ ∑ a ∈ s, (μ (t a)).toReal = ∑ i ∈ s, μ.real (t i)

State before:
case h.e'_4
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ✝ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : μ.real univ < ∑ i ∈ s, μ.real (t i)
⊢ ∑ a ∈ s, (μ (t a)).toReal = ∑ i ∈ s, μ.real (t i)
Tactic:
rfl
State after:
no goals

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ✝ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : μ.real univ < ∑ i ∈ s, μ.real (t i)
⊢ ∑ i ∈ s, μ (t i) ≠ ⊤
Tactic:
exact (ENNReal.sum_lt_top (fun i hi ↦ measure_ne_top _ _)).ne
State after:
no goals