internlm/Lean-Github huggingface dataset:
Theorem: MeasureTheory.nonempty_inter_of_measureReal_lt_add
Proof 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 α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : μ.real u < μ.real s + μ.real t
hu : autoParam (μ u ≠ ⊤) _auto✝
⊢ μ s + μ t ≠ ⊤
Tactic:
exact ENNReal.add_ne_top.2 ⟨measure_ne_top_of_subset h's hu, measure_ne_top_of_subset h't hu⟩
Proof state after:
no goals
Theorem: MeasureTheory.nonempty_inter_of_measureReal_lt_add'
Proof 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
Proof 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
Theorem: MeasureTheory.nonempty_inter_of_measureReal_lt_add'
Proof 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]
Proof 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
Theorem: MeasureTheory.nonempty_inter_of_measureReal_lt_add'
Proof 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
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_prod_prod
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ✝ : Measure α
s✝ s₁ s₂ t✝ : Set α
μ : Measure α
ν : Measure β
inst✝ : SigmaFinite ν
s : Set α
t : Set β
⊢ (μ.prod ν).real (s ×ˢ t) = μ.real s * ν.real t
Tactic:
simp only [measureReal_def, prod_prod, ENNReal.toReal_mul]
Proof state after:
no goals
Theorem: MeasureTheory.Measure.ext_iff_singleton
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
S : Type u_4
inst✝² : Fintype S
inst✝¹ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ1 μ2 : Measure S
⊢ μ1 = μ2 ↔ ∀ (x : S), μ1 {x} = μ2 {x}
Tactic:
constructor
Proof state after:
case mp
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
S : Type u_4
inst✝² : Fintype S
inst✝¹ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ1 μ2 : Measure S
⊢ μ1 = μ2 → ∀ (x : S), μ1 {x} = μ2 {x}

case mpr
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
S : Type u_4
inst✝² : Fintype S
inst✝¹ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ1 μ2 : Measure S
⊢ (∀ (x : S), μ1 {x} = μ2 {x}) → μ1 = μ2
Theorem: MeasureTheory.Measure.ext_iff_singleton
Proof state before:
case mp
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
S : Type u_4
inst✝² : Fintype S
inst✝¹ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ1 μ2 : Measure S
⊢ μ1 = μ2 → ∀ (x : S), μ1 {x} = μ2 {x}
Tactic:
rintro rfl
Proof state after:
case mp
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
S : Type u_4
inst✝² : Fintype S
inst✝¹ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ1 : Measure S
⊢ ∀ (x : S), μ1 {x} = μ1 {x}
Theorem: MeasureTheory.Measure.ext_iff_singleton
Proof state before:
case mp
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
S : Type u_4
inst✝² : Fintype S
inst✝¹ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ1 : Measure S
⊢ ∀ (x : S), μ1 {x} = μ1 {x}
Tactic:
simp
Proof state after:
no goals
Theorem: MeasureTheory.Measure.ext_iff_singleton
Proof state before:
case mpr
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
S : Type u_4
inst✝² : Fintype S
inst✝¹ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ1 μ2 : Measure S
⊢ (∀ (x : S), μ1 {x} = μ2 {x}) → μ1 = μ2
Tactic:
intro h
Proof state after:
case mpr
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
S : Type u_4
inst✝² : Fintype S
inst✝¹ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ1 μ2 : Measure S
h : ∀ (x : S), μ1 {x} = μ2 {x}
⊢ μ1 = μ2
Theorem: MeasureTheory.Measure.ext_iff_singleton
Proof state before:
case mpr
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
S : Type u_4
inst✝² : Fintype S
inst✝¹ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ1 μ2 : Measure S
h : ∀ (x : S), μ1 {x} = μ2 {x}
⊢ μ1 = μ2
Tactic:
ext s
Proof state after:
case mpr.h
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t : Set α
S : Type u_4
inst✝² : Fintype S
inst✝¹ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ1 μ2 : Measure S
h : ∀ (x : S), μ1 {x} = μ2 {x}
s : Set S
a✝ : MeasurableSet s
⊢ μ1 s = μ2 s
Theorem: MeasureTheory.Measure.ext_iff_singleton
Proof state before:
case mpr.h
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t : Set α
S : Type u_4
inst✝² : Fintype S
inst✝¹ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ1 μ2 : Measure S
h : ∀ (x : S), μ1 {x} = μ2 {x}
s : Set S
a✝ : MeasurableSet s
⊢ μ1 s = μ2 s
Tactic:
have hs : Set.Finite s := Set.toFinite s
Proof state after:
case mpr.h
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t : Set α
S : Type u_4
inst✝² : Fintype S
inst✝¹ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ1 μ2 : Measure S
h : ∀ (x : S), μ1 {x} = μ2 {x}
s : Set S
a✝ : MeasurableSet s
hs : s.Finite
⊢ μ1 s = μ2 s
Theorem: MeasureTheory.Measure.ext_iff_singleton
Proof state before:
case mpr.h
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t : Set α
S : Type u_4
inst✝² : Fintype S
inst✝¹ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ1 μ2 : Measure S
h : ∀ (x : S), μ1 {x} = μ2 {x}
s : Set S
a✝ : MeasurableSet s
hs : s.Finite
⊢ μ1 s = μ2 s
Tactic:
rw [← hs.coe_toFinset, ← Finset.sum_measure_singleton μ1, ← Finset.sum_measure_singleton μ2]
Proof state after:
case mpr.h
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t : Set α
S : Type u_4
inst✝² : Fintype S
inst✝¹ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ1 μ2 : Measure S
h : ∀ (x : S), μ1 {x} = μ2 {x}
s : Set S
a✝ : MeasurableSet s
hs : s.Finite
⊢ ∑ x ∈ hs.toFinset, μ1 {x} = ∑ x ∈ hs.toFinset, μ2 {x}
Theorem: MeasureTheory.Measure.ext_iff_singleton
Proof state before:
case mpr.h
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t : Set α
S : Type u_4
inst✝² : Fintype S
inst✝¹ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ1 μ2 : Measure S
h : ∀ (x : S), μ1 {x} = μ2 {x}
s : Set S
a✝ : MeasurableSet s
hs : s.Finite
⊢ ∑ x ∈ hs.toFinset, μ1 {x} = ∑ x ∈ hs.toFinset, μ2 {x}
Tactic:
simp_rw [h]
Proof state after:
no goals
Theorem: MeasureTheory.ext_iff_measureReal_singleton
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
S : Type u_4
inst✝⁴ : Fintype S
inst✝³ : MeasurableSpace S
inst✝² : MeasurableSingletonClass S
μ1 μ2 : Measure S
inst✝¹ : IsFiniteMeasure μ1
inst✝ : IsFiniteMeasure μ2
⊢ μ1 = μ2 ↔ ∀ (x : S), μ1.real {x} = μ2.real {x}
Tactic:
rw [Measure.ext_iff_singleton]
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
S : Type u_4
inst✝⁴ : Fintype S
inst✝³ : MeasurableSpace S
inst✝² : MeasurableSingletonClass S
μ1 μ2 : Measure S
inst✝¹ : IsFiniteMeasure μ1
inst✝ : IsFiniteMeasure μ2
⊢ (∀ (x : S), μ1 {x} = μ2 {x}) ↔ ∀ (x : S), μ1.real {x} = μ2.real {x}
Theorem: MeasureTheory.ext_iff_measureReal_singleton
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
S : Type u_4
inst✝⁴ : Fintype S
inst✝³ : MeasurableSpace S
inst✝² : MeasurableSingletonClass S
μ1 μ2 : Measure S
inst✝¹ : IsFiniteMeasure μ1
inst✝ : IsFiniteMeasure μ2
⊢ (∀ (x : S), μ1 {x} = μ2 {x}) ↔ ∀ (x : S), μ1.real {x} = μ2.real {x}
Tactic:
congr! with x
Proof state after:
case a.h.a
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
S : Type u_4
inst✝⁴ : Fintype S
inst✝³ : MeasurableSpace S
inst✝² : MeasurableSingletonClass S
μ1 μ2 : Measure S
inst✝¹ : IsFiniteMeasure μ1
inst✝ : IsFiniteMeasure μ2
x : S
⊢ μ1 {x} = μ2 {x} ↔ μ1.real {x} = μ2.real {x}
Theorem: MeasureTheory.ext_iff_measureReal_singleton
Proof state before:
case a.h.a
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
S : Type u_4
inst✝⁴ : Fintype S
inst✝³ : MeasurableSpace S
inst✝² : MeasurableSingletonClass S
μ1 μ2 : Measure S
inst✝¹ : IsFiniteMeasure μ1
inst✝ : IsFiniteMeasure μ2
x : S
⊢ μ1 {x} = μ2 {x} ↔ μ1.real {x} = μ2.real {x}
Tactic:
have h1 : μ1 {x} ≠ ⊤ := by finiteness
Proof state after:
case a.h.a
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
S : Type u_4
inst✝⁴ : Fintype S
inst✝³ : MeasurableSpace S
inst✝² : MeasurableSingletonClass S
μ1 μ2 : Measure S
inst✝¹ : IsFiniteMeasure μ1
inst✝ : IsFiniteMeasure μ2
x : S
h1 : μ1 {x} ≠ ⊤
⊢ μ1 {x} = μ2 {x} ↔ μ1.real {x} = μ2.real {x}
Theorem: MeasureTheory.ext_iff_measureReal_singleton
Proof state before:
case a.h.a
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
S : Type u_4
inst✝⁴ : Fintype S
inst✝³ : MeasurableSpace S
inst✝² : MeasurableSingletonClass S
μ1 μ2 : Measure S
inst✝¹ : IsFiniteMeasure μ1
inst✝ : IsFiniteMeasure μ2
x : S
h1 : μ1 {x} ≠ ⊤
⊢ μ1 {x} = μ2 {x} ↔ μ1.real {x} = μ2.real {x}
Tactic:
have h2 : μ2 {x} ≠ ⊤ := by finiteness
Proof state after:
case a.h.a
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
S : Type u_4
inst✝⁴ : Fintype S
inst✝³ : MeasurableSpace S
inst✝² : MeasurableSingletonClass S
μ1 μ2 : Measure S
inst✝¹ : IsFiniteMeasure μ1
inst✝ : IsFiniteMeasure μ2
x : S
h1 : μ1 {x} ≠ ⊤
h2 : μ2 {x} ≠ ⊤
⊢ μ1 {x} = μ2 {x} ↔ μ1.real {x} = μ2.real {x}
Theorem: MeasureTheory.ext_iff_measureReal_singleton
Proof state before:
case a.h.a
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
S : Type u_4
inst✝⁴ : Fintype S
inst✝³ : MeasurableSpace S
inst✝² : MeasurableSingletonClass S
μ1 μ2 : Measure S
inst✝¹ : IsFiniteMeasure μ1
inst✝ : IsFiniteMeasure μ2
x : S
h1 : μ1 {x} ≠ ⊤
h2 : μ2 {x} ≠ ⊤
⊢ μ1 {x} = μ2 {x} ↔ μ1.real {x} = μ2.real {x}
Tactic:
rw [measureReal_def, measureReal_def, ENNReal.toReal_eq_toReal_iff]
Proof state after:
case a.h.a
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
S : Type u_4
inst✝⁴ : Fintype S
inst✝³ : MeasurableSpace S
inst✝² : MeasurableSingletonClass S
μ1 μ2 : Measure S
inst✝¹ : IsFiniteMeasure μ1
inst✝ : IsFiniteMeasure μ2
x : S
h1 : μ1 {x} ≠ ⊤
h2 : μ2 {x} ≠ ⊤
⊢ μ1 {x} = μ2 {x} ↔ μ1 {x} = μ2 {x} ∨ μ1 {x} = 0 ∧ μ2 {x} = ⊤ ∨ μ1 {x} = ⊤ ∧ μ2 {x} = 0
Theorem: MeasureTheory.ext_iff_measureReal_singleton
Proof state before:
case a.h.a
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
S : Type u_4
inst✝⁴ : Fintype S
inst✝³ : MeasurableSpace S
inst✝² : MeasurableSingletonClass S
μ1 μ2 : Measure S
inst✝¹ : IsFiniteMeasure μ1
inst✝ : IsFiniteMeasure μ2
x : S
h1 : μ1 {x} ≠ ⊤
h2 : μ2 {x} ≠ ⊤
⊢ μ1 {x} = μ2 {x} ↔ μ1 {x} = μ2 {x} ∨ μ1 {x} = 0 ∧ μ2 {x} = ⊤ ∨ μ1 {x} = ⊤ ∧ μ2 {x} = 0
Tactic:
simp [h1, h2]
Proof state after:
no goals
Theorem: MeasureTheory.ext_iff_measureReal_singleton
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
S : Type u_4
inst✝⁴ : Fintype S
inst✝³ : MeasurableSpace S
inst✝² : MeasurableSingletonClass S
μ1 μ2 : Measure S
inst✝¹ : IsFiniteMeasure μ1
inst✝ : IsFiniteMeasure μ2
x : S
⊢ μ1 {x} ≠ ⊤
Tactic:
finiteness
Proof state after:
no goals
Theorem: MeasureTheory.ext_iff_measureReal_singleton
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
S : Type u_4
inst✝⁴ : Fintype S
inst✝³ : MeasurableSpace S
inst✝² : MeasurableSingletonClass S
μ1 μ2 : Measure S
inst✝¹ : IsFiniteMeasure μ1
inst✝ : IsFiniteMeasure μ2
x : S
h1 : μ1 {x} ≠ ⊤
⊢ μ2 {x} ≠ ⊤
Tactic:
finiteness
Proof state after:
no goals
Theorem: ENNReal.le_on_subset
Proof state before:
X : Type
inst✝ : MeasurableSpace X
μ : MeasureTheory.Measure X
f g : X → ℝ≥0∞
E : Set X
hE : MeasurableSet E
hf : Measurable f
hg : Measurable g
a : ℝ≥0∞
h : ∀ x ∈ E, a ≤ f x + g x
⊢ ∃ E' ⊆ E, MeasurableSet E' ∧ μ E ≤ 2 * μ E' ∧ ((∀ x ∈ E', a / 2 ≤ f x) ∨ ∀ x ∈ E', a / 2 ≤ g x)
Tactic:
set Ef := E ∩ f⁻¹' (Set.Ici (a / 2)) with Ef_def
Proof state after:
X : Type
inst✝ : MeasurableSpace X
μ : MeasureTheory.Measure X
f g : X → ℝ≥0∞
E : Set X
hE : MeasurableSet E
hf : Measurable f
hg : Measurable g
a : ℝ≥0∞
h : ∀ x ∈ E, a ≤ f x + g x
Ef : Set X := E ∩ f ⁻¹' Set.Ici (a / 2)
Ef_def : Ef = E ∩ f ⁻¹' Set.Ici (a / 2)
⊢ ∃ E' ⊆ E, MeasurableSet E' ∧ μ E ≤ 2 * μ E' ∧ ((∀ x ∈ E', a / 2 ≤ f x) ∨ ∀ x ∈ E', a / 2 ≤ g x)
Theorem: ENNReal.le_on_subset
Proof state before:
X : Type
inst✝ : MeasurableSpace X
μ : MeasureTheory.Measure X
f g : X → ℝ≥0∞
E : Set X
hE : MeasurableSet E
hf : Measurable f
hg : Measurable g
a : ℝ≥0∞
h : ∀ x ∈ E, a ≤ f x + g x
Ef : Set X := E ∩ f ⁻¹' Set.Ici (a / 2)
Ef_def : Ef = E ∩ f ⁻¹' Set.Ici (a / 2)
⊢ ∃ E' ⊆ E, MeasurableSet E' ∧ μ E ≤ 2 * μ E' ∧ ((∀ x ∈ E', a / 2 ≤ f x) ∨ ∀ x ∈ E', a / 2 ≤ g x)
Tactic:
set Eg := E ∩ g⁻¹' (Set.Ici (a / 2)) with Eg_def
Proof state after:
X : Type
inst✝ : MeasurableSpace X
μ : MeasureTheory.Measure X
f g : X → ℝ≥0∞
E : Set X
hE : MeasurableSet E
hf : Measurable f
hg : Measurable g
a : ℝ≥0∞
h : ∀ x ∈ E, a ≤ f x + g x
Ef : Set X := E ∩ f ⁻¹' Set.Ici (a / 2)
Ef_def : Ef = E ∩ f ⁻¹' Set.Ici (a / 2)
Eg : Set X := E ∩ g ⁻¹' Set.Ici (a / 2)
Eg_def : Eg = E ∩ g ⁻¹' Set.Ici (a / 2)
⊢ ∃ E' ⊆ E, MeasurableSet E' ∧ μ E ≤ 2 * μ E' ∧ ((∀ x ∈ E', a / 2 ≤ f x) ∨ ∀ x ∈ E', a / 2 ≤ g x)
Theorem: ENNReal.le_on_subset
Proof state before:
X : Type
inst✝ : MeasurableSpace X
μ : MeasureTheory.Measure X
f g : X → ℝ≥0∞
E : Set X
hE : MeasurableSet E
hf : Measurable f
hg : Measurable g
a : ℝ≥0∞
h : ∀ x ∈ E, a ≤ f x + g x
Ef : Set X := E ∩ f ⁻¹' Set.Ici (a / 2)
Ef_def : Ef = E ∩ f ⁻¹' Set.Ici (a / 2)
Eg : Set X := E ∩ g ⁻¹' Set.Ici (a / 2)
Eg_def : Eg = E ∩ g ⁻¹' Set.Ici (a / 2)
⊢ ∃ E' ⊆ E, MeasurableSet E' ∧ μ E ≤ 2 * μ E' ∧ ((∀ x ∈ E', a / 2 ≤ f x) ∨ ∀ x ∈ E', a / 2 ≤ g x)
Tactic:
have : E ⊆ Ef ∪ Eg := by
  intro x hx
  rw [Ef_def, Eg_def]
  simp
  by_contra hx'
  push_neg at hx'
  absurd le_refl a
  push_neg
  calc a
    _ ≤ f x + g x := h x hx
    _ < a / 2 + a / 2 := by
      gcongr
      . exact hx'.1 hx
      . exact hx'.2 hx
    _ = a := by
      ring_nf
      apply ENNReal.div_mul_cancel <;> norm_num
Proof state after:
X : Type
inst✝ : MeasurableSpace X
μ : MeasureTheory.Measure X
f g : X → ℝ≥0∞
E : Set X
hE : MeasurableSet E
hf : Measurable f
hg : Measurable g
a : ℝ≥0∞
h : ∀ x ∈ E, a ≤ f x + g x
Ef : Set X := E ∩ f ⁻¹' Set.Ici (a / 2)
Ef_def : Ef = E ∩ f ⁻¹' Set.Ici (a / 2)
Eg : Set X := E ∩ g ⁻¹' Set.Ici (a / 2)
Eg_def : Eg = E ∩ g ⁻¹' Set.Ici (a / 2)
this : E ⊆ Ef ∪ Eg
⊢ ∃ E' ⊆ E, MeasurableSet E' ∧ μ E ≤ 2 * μ E' ∧ ((∀ x ∈ E', a / 2 ≤ f x) ∨ ∀ x ∈ E', a / 2 ≤ g x)
Theorem: ENNReal.le_on_subset
Proof state before:
X : Type
inst✝ : MeasurableSpace X
μ : MeasureTheory.Measure X
f g : X → ℝ≥0∞
E : Set X
hE : MeasurableSet E
hf : Measurable f
hg : Measurable g
a : ℝ≥0∞
h : ∀ x ∈ E, a ≤ f x + g x
Ef : Set X := E ∩ f ⁻¹' Set.Ici (a / 2)
Ef_def : Ef = E ∩ f ⁻¹' Set.Ici (a / 2)
Eg : Set X := E ∩ g ⁻¹' Set.Ici (a / 2)
Eg_def : Eg = E ∩ g ⁻¹' Set.Ici (a / 2)
this : E ⊆ Ef ∪ Eg
⊢ ∃ E' ⊆ E, MeasurableSet E' ∧ μ E ≤ 2 * μ E' ∧ ((∀ x ∈ E', a / 2 ≤ f x) ∨ ∀ x ∈ E', a / 2 ≤ g x)
Tactic:
have : μ E ≤ 2 * μ Ef ∨ μ E ≤ 2 * μ Eg := by
  by_contra hEfg
  push_neg at hEfg
  absurd le_refl (2 * μ E)
  push_neg
  calc 2 * μ E
  _ ≤ 2 * μ (Ef ∪ Eg) := by
    gcongr
  _ ≤ 2 * (μ Ef + μ Eg) := by
    gcongr
    apply MeasureTheory.measure_union_le
  _ = 2 * μ Ef + 2 * μ Eg := by ring
  _ < μ E + μ E := by
    gcongr
    . exact hEfg.1
    . exact hEfg.2
  _ = 2 * μ E := by ring
Proof state after:
X : Type
inst✝ : MeasurableSpace X
μ : MeasureTheory.Measure X
f g : X → ℝ≥0∞
E : Set X
hE : MeasurableSet E
hf : Measurable f
hg : Measurable g
a : ℝ≥0∞
h : ∀ x ∈ E, a ≤ f x + g x
Ef : Set X := E ∩ f ⁻¹' Set.Ici (a / 2)
Ef_def : Ef = E ∩ f ⁻¹' Set.Ici (a / 2)
Eg : Set X := E ∩ g ⁻¹' Set.Ici (a / 2)
Eg_def : Eg = E ∩ g ⁻¹' Set.Ici (a / 2)
this✝ : E ⊆ Ef ∪ Eg
this : μ E ≤ 2 * μ Ef ∨ μ E ≤ 2 * μ Eg
⊢ ∃ E' ⊆ E, MeasurableSet E' ∧ μ E ≤ 2 * μ E' ∧ ((∀ x ∈ E', a / 2 ≤ f x) ∨ ∀ x ∈ E', a / 2 ≤ g x)
Theorem: ENNReal.le_on_subset
Proof state before:
X : Type
inst✝ : MeasurableSpace X
μ : MeasureTheory.Measure X
f g : X → ℝ≥0∞
E : Set X
hE : MeasurableSet E
hf : Measurable f
hg : Measurable g
a : ℝ≥0∞
h : ∀ x ∈ E, a ≤ f x + g x
Ef : Set X := E ∩ f ⁻¹' Set.Ici (a / 2)
Ef_def : Ef = E ∩ f ⁻¹' Set.Ici (a / 2)
Eg : Set X := E ∩ g ⁻¹' Set.Ici (a / 2)
Eg_def : Eg = E ∩ g ⁻¹' Set.Ici (a / 2)
this✝ : E ⊆ Ef ∪ Eg
this : μ E ≤ 2 * μ Ef ∨ μ E ≤ 2 * μ Eg
⊢ ∃ E' ⊆ E, MeasurableSet E' ∧ μ E ≤ 2 * μ E' ∧ ((∀ x ∈ E', a / 2 ≤ f x) ∨ ∀ x ∈ E', a / 2 ≤ g x)
Tactic:
rcases this with hEf | hEg
Proof state after:
case inl
X : Type
inst✝ : MeasurableSpace X
μ : MeasureTheory.Measure X
f g : X → ℝ≥0∞
E : Set X
hE : MeasurableSet E
hf : Measurable f
hg : Measurable g
a : ℝ≥0∞
h : ∀ x ∈ E, a ≤ f x + g x
Ef : Set X := E ∩ f ⁻¹' Set.Ici (a / 2)
Ef_def : Ef = E ∩ f ⁻¹' Set.Ici (a / 2)
Eg : Set X := E ∩ g ⁻¹' Set.Ici (a / 2)
Eg_def : Eg = E ∩ g ⁻¹' Set.Ici (a / 2)
this : E ⊆ Ef ∪ Eg
hEf : μ E ≤ 2 * μ Ef
⊢ ∃ E' ⊆ E, MeasurableSet E' ∧ μ E ≤ 2 * μ E' ∧ ((∀ x ∈ E', a / 2 ≤ f x) ∨ ∀ x ∈ E', a / 2 ≤ g x)

case inr
X : Type
inst✝ : MeasurableSpace X
μ : MeasureTheory.Measure X
f g : X → ℝ≥0∞
E : Set X
hE : MeasurableSet E
hf : Measurable f
hg : Measurable g
a : ℝ≥0∞
h : ∀ x ∈ E, a ≤ f x + g x
Ef : Set X := E ∩ f ⁻¹' Set.Ici (a / 2)
Ef_def : Ef = E ∩ f ⁻¹' Set.Ici (a / 2)
Eg : Set X := E ∩ g ⁻¹' Set.Ici (a / 2)
Eg_def : Eg = E ∩ g ⁻¹' Set.Ici (a / 2)
this : E ⊆ Ef ∪ Eg
hEg : μ E ≤ 2 * μ Eg
⊢ ∃ E' ⊆ E, MeasurableSet E' ∧ μ E ≤ 2 * μ E' ∧ ((∀ x ∈ E', a / 2 ≤ f x) ∨ ∀ x ∈ E', a / 2 ≤ g x)
Theorem: ENNReal.le_on_subset
Proof state before:
case inl
X : Type
inst✝ : MeasurableSpace X
μ : MeasureTheory.Measure X
f g : X → ℝ≥0∞
E : Set X
hE : MeasurableSet E
hf : Measurable f
hg : Measurable g
a : ℝ≥0∞
h : ∀ x ∈ E, a ≤ f x + g x
Ef : Set X := E ∩ f ⁻¹' Set.Ici (a / 2)
Ef_def : Ef = E ∩ f ⁻¹' Set.Ici (a / 2)
Eg : Set X := E ∩ g ⁻¹' Set.Ici (a / 2)
Eg_def : Eg = E ∩ g ⁻¹' Set.Ici (a / 2)
this : E ⊆ Ef ∪ Eg
hEf : μ E ≤ 2 * μ Ef
⊢ ∃ E' ⊆ E, MeasurableSet E' ∧ μ E ≤ 2 * μ E' ∧ ((∀ x ∈ E', a / 2 ≤ f x) ∨ ∀ x ∈ E', a / 2 ≤ g x)

case inr
X : Type
inst✝ : MeasurableSpace X
μ : MeasureTheory.Measure X
f g : X → ℝ≥0∞
E : Set X
hE : MeasurableSet E
hf : Measurable f
hg : Measurable g
a : ℝ≥0∞
h : ∀ x ∈ E, a ≤ f x + g x
Ef : Set X := E ∩ f ⁻¹' Set.Ici (a / 2)
Ef_def : Ef = E ∩ f ⁻¹' Set.Ici (a / 2)
Eg : Set X := E ∩ g ⁻¹' Set.Ici (a / 2)
Eg_def : Eg = E ∩ g ⁻¹' Set.Ici (a / 2)
this : E ⊆ Ef ∪ Eg
hEg : μ E ≤ 2 * μ Eg
⊢ ∃ E' ⊆ E, MeasurableSet E' ∧ μ E ≤ 2 * μ E' ∧ ((∀ x ∈ E', a / 2 ≤ f x) ∨ ∀ x ∈ E', a / 2 ≤ g x)
Tactic:
. use Ef
  constructor
  . apply Set.inter_subset_left
  constructor
  . apply MeasurableSet.inter hE
    apply hf measurableSet_Ici
  use hEf
  left
  rw [Ef_def]
  simp
Proof state after:
case inr
X : Type
inst✝ : MeasurableSpace X
μ : MeasureTheory.Measure X
f g : X → ℝ≥0∞
E : Set X
hE : MeasurableSet E
hf : Measurable f
hg : Measurable g
a : ℝ≥0∞
h : ∀ x ∈ E, a ≤ f x + g x
Ef : Set X := E ∩ f ⁻¹' Set.Ici (a / 2)
Ef_def : Ef = E ∩ f ⁻¹' Set.Ici (a / 2)
Eg : Set X := E ∩ g ⁻¹' Set.Ici (a / 2)
Eg_def : Eg = E ∩ g ⁻¹' Set.Ici (a / 2)
this : E ⊆ Ef ∪ Eg
hEg : μ E ≤ 2 * μ Eg
⊢ ∃ E' ⊆ E, MeasurableSet E' ∧ μ E ≤ 2 * μ E' ∧ ((∀ x ∈ E', a / 2 ≤ f x) ∨ ∀ x ∈ E', a / 2 ≤ g x)
Theorem: ENNReal.le_on_subset
Proof state before:
case inr
X : Type
inst✝ : MeasurableSpace X
μ : MeasureTheory.Measure X
f g : X → ℝ≥0∞
E : Set X
hE : MeasurableSet E
hf : Measurable f
hg : Measurable g
a : ℝ≥0∞
h : ∀ x ∈ E, a ≤ f x + g x
Ef : Set X := E ∩ f ⁻¹' Set.Ici (a / 2)
Ef_def : Ef = E ∩ f ⁻¹' Set.Ici (a / 2)
Eg : Set X := E ∩ g ⁻¹' Set.Ici (a / 2)
Eg_def : Eg = E ∩ g ⁻¹' Set.Ici (a / 2)
this : E ⊆ Ef ∪ Eg
hEg : μ E ≤ 2 * μ Eg
⊢ ∃ E' ⊆ E, MeasurableSet E' ∧ μ E ≤ 2 * μ E' ∧ ((∀ x ∈ E', a / 2 ≤ f x) ∨ ∀ x ∈ E', a / 2 ≤ g x)
Tactic:
. use Eg
  constructor
  . apply Set.inter_subset_left
  constructor
  . apply MeasurableSet.inter hE
    apply hg measurableSet_Ici
  use hEg
  right
  rw [Eg_def]
  simp
Proof state after:
no goals
Theorem: ENNReal.le_on_subset
Proof state before:
X : Type
inst✝ : MeasurableSpace X
μ : MeasureTheory.Measure X
f g : X → ℝ≥0∞
E : Set X
hE : MeasurableSet E
hf : Measurable f
hg : Measurable g
a : ℝ≥0∞
h : ∀ x ∈ E, a ≤ f x + g x
Ef : Set X := E ∩ f ⁻¹' Set.Ici (a / 2)
Ef_def : Ef = E ∩ f ⁻¹' Set.Ici (a / 2)
Eg : Set X := E ∩ g ⁻¹' Set.Ici (a / 2)
Eg_def : Eg = E ∩ g ⁻¹' Set.Ici (a / 2)
⊢ E ⊆ Ef ∪ Eg
Tactic:
intro x hx
Proof state after:
X : Type
inst✝ : MeasurableSpace X
μ : MeasureTheory.Measure X
f g : X → ℝ≥0∞
E : Set X
hE : MeasurableSet E
hf : Measurable f
hg : Measurable g
a : ℝ≥0∞
h : ∀ x ∈ E, a ≤ f x + g x
Ef : Set X := E ∩ f ⁻¹' Set.Ici (a / 2)
Ef_def : Ef = E ∩ f ⁻¹' Set.Ici (a / 2)
Eg : Set X := E ∩ g ⁻¹' Set.Ici (a / 2)
Eg_def : Eg = E ∩ g ⁻¹' Set.Ici (a / 2)
x : X
hx : x ∈ E
⊢ x ∈ Ef ∪ Eg
Theorem: ENNReal.le_on_subset
Proof state before:
X : Type
inst✝ : MeasurableSpace X
μ : MeasureTheory.Measure X
f g : X → ℝ≥0∞
E : Set X
hE : MeasurableSet E
hf : Measurable f
hg : Measurable g
a : ℝ≥0∞
h : ∀ x ∈ E, a ≤ f x + g x
Ef : Set X := E ∩ f ⁻¹' Set.Ici (a / 2)
Ef_def : Ef = E ∩ f ⁻¹' Set.Ici (a / 2)
Eg : Set X := E ∩ g ⁻¹' Set.Ici (a / 2)
Eg_def : Eg = E ∩ g ⁻¹' Set.Ici (a / 2)
x : X
hx : x ∈ E
⊢ x ∈ Ef ∪ Eg
Tactic:
rw [Ef_def, Eg_def]
Proof state after:
X : Type
inst✝ : MeasurableSpace X
μ : MeasureTheory.Measure X
f g : X → ℝ≥0∞
E : Set X
hE : MeasurableSet E
hf : Measurable f
hg : Measurable g
a : ℝ≥0∞
h : ∀ x ∈ E, a ≤ f x + g x
Ef : Set X := E ∩ f ⁻¹' Set.Ici (a / 2)
Ef_def : Ef = E ∩ f ⁻¹' Set.Ici (a / 2)
Eg : Set X := E ∩ g ⁻¹' Set.Ici (a / 2)
Eg_def : Eg = E ∩ g ⁻¹' Set.Ici (a / 2)
x : X
hx : x ∈ E
⊢ x ∈ E ∩ f ⁻¹' Set.Ici (a / 2) ∪ E ∩ g ⁻¹' Set.Ici (a / 2)