internlm/Lean-Github huggingface dataset:
Theorem: ENNReal.le_on_subset
Proof state before:
case h
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
⊢ Ef ⊆ E ∧ MeasurableSet Ef ∧ μ E ≤ 2 * μ Ef ∧ ((∀ x ∈ Ef, a / 2 ≤ f x) ∨ ∀ x ∈ Ef, a / 2 ≤ g x)
Tactic:
constructor
Proof state after:
case h.left
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
⊢ Ef ⊆ E

case h.right
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
⊢ MeasurableSet Ef ∧ μ E ≤ 2 * μ Ef ∧ ((∀ x ∈ Ef, a / 2 ≤ f x) ∨ ∀ x ∈ Ef, a / 2 ≤ g x)
Theorem: ENNReal.le_on_subset
Proof state before:
case h.left
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
⊢ Ef ⊆ E

case h.right
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
⊢ MeasurableSet Ef ∧ μ E ≤ 2 * μ Ef ∧ ((∀ x ∈ Ef, a / 2 ≤ f x) ∨ ∀ x ∈ Ef, a / 2 ≤ g x)
Tactic:
. apply Set.inter_subset_left
Proof state after:
case h.right
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
⊢ MeasurableSet Ef ∧ μ E ≤ 2 * μ Ef ∧ ((∀ x ∈ Ef, a / 2 ≤ f x) ∨ ∀ x ∈ Ef, a / 2 ≤ g x)
Theorem: ENNReal.le_on_subset
Proof state before:
case h.right
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
⊢ MeasurableSet Ef ∧ μ E ≤ 2 * μ Ef ∧ ((∀ x ∈ Ef, a / 2 ≤ f x) ∨ ∀ x ∈ Ef, a / 2 ≤ g x)
Tactic:
constructor
Proof state after:
case h.right.left
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
⊢ MeasurableSet Ef

case h.right.right
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 ≤ 2 * μ Ef ∧ ((∀ x ∈ Ef, a / 2 ≤ f x) ∨ ∀ x ∈ Ef, a / 2 ≤ g x)
Theorem: ENNReal.le_on_subset
Proof state before:
case h.right.left
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
⊢ MeasurableSet Ef

case h.right.right
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 ≤ 2 * μ Ef ∧ ((∀ x ∈ Ef, a / 2 ≤ f x) ∨ ∀ x ∈ Ef, a / 2 ≤ g x)
Tactic:
. apply MeasurableSet.inter hE
  apply hf measurableSet_Ici
Proof state after:
case h.right.right
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 ≤ 2 * μ Ef ∧ ((∀ x ∈ Ef, a / 2 ≤ f x) ∨ ∀ x ∈ Ef, a / 2 ≤ g x)
Theorem: ENNReal.le_on_subset
Proof state before:
case h.right.right
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 ≤ 2 * μ Ef ∧ ((∀ x ∈ Ef, a / 2 ≤ f x) ∨ ∀ x ∈ Ef, a / 2 ≤ g x)
Tactic:
use hEf
Proof state after:
case right
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
⊢ (∀ x ∈ Ef, a / 2 ≤ f x) ∨ ∀ x ∈ Ef, a / 2 ≤ g x
Theorem: ENNReal.le_on_subset
Proof state before:
case right
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
⊢ (∀ x ∈ Ef, a / 2 ≤ f x) ∨ ∀ x ∈ Ef, a / 2 ≤ g x
Tactic:
left
Proof state after:
case right.h
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
⊢ ∀ x ∈ Ef, a / 2 ≤ f x
Theorem: ENNReal.le_on_subset
Proof state before:
case right.h
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
⊢ ∀ x ∈ Ef, a / 2 ≤ f x
Tactic:
rw [Ef_def]
Proof state after:
case right.h
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
⊢ ∀ x ∈ E ∩ f ⁻¹' Set.Ici (a / 2), a / 2 ≤ f x
Theorem: ENNReal.le_on_subset
Proof state before:
case right.h
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
⊢ ∀ x ∈ E ∩ f ⁻¹' Set.Ici (a / 2), a / 2 ≤ f x
Tactic:
simp
Proof state after:
no goals
Theorem: ENNReal.le_on_subset
Proof state before:
case h.left
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
⊢ Ef ⊆ E
Tactic:
apply Set.inter_subset_left
Proof state after:
no goals
Theorem: ENNReal.le_on_subset
Proof state before:
case h.right.left
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
⊢ MeasurableSet Ef
Tactic:
apply MeasurableSet.inter hE
Proof state after:
case h.right.left
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
⊢ MeasurableSet (f ⁻¹' Set.Ici (a / 2))
Theorem: ENNReal.le_on_subset
Proof state before:
case h.right.left
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
⊢ MeasurableSet (f ⁻¹' Set.Ici (a / 2))
Tactic:
apply hf measurableSet_Ici
Proof state after:
no goals
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
Proof state after:
case h
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
⊢ Eg ⊆ E ∧ MeasurableSet Eg ∧ μ E ≤ 2 * μ Eg ∧ ((∀ x ∈ Eg, a / 2 ≤ f x) ∨ ∀ x ∈ Eg, a / 2 ≤ g x)
Theorem: ENNReal.le_on_subset
Proof state before:
case h
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
⊢ Eg ⊆ E ∧ MeasurableSet Eg ∧ μ E ≤ 2 * μ Eg ∧ ((∀ x ∈ Eg, a / 2 ≤ f x) ∨ ∀ x ∈ Eg, a / 2 ≤ g x)
Tactic:
constructor
Proof state after:
case h.left
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
⊢ Eg ⊆ E

case h.right
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
⊢ MeasurableSet Eg ∧ μ E ≤ 2 * μ Eg ∧ ((∀ x ∈ Eg, a / 2 ≤ f x) ∨ ∀ x ∈ Eg, a / 2 ≤ g x)
Theorem: ENNReal.le_on_subset
Proof state before:
case h.left
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
⊢ Eg ⊆ E

case h.right
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
⊢ MeasurableSet Eg ∧ μ E ≤ 2 * μ Eg ∧ ((∀ x ∈ Eg, a / 2 ≤ f x) ∨ ∀ x ∈ Eg, a / 2 ≤ g x)
Tactic:
. apply Set.inter_subset_left
Proof state after:
case h.right
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
⊢ MeasurableSet Eg ∧ μ E ≤ 2 * μ Eg ∧ ((∀ x ∈ Eg, a / 2 ≤ f x) ∨ ∀ x ∈ Eg, a / 2 ≤ g x)
Theorem: ENNReal.le_on_subset
Proof state before:
case h.right
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
⊢ MeasurableSet Eg ∧ μ E ≤ 2 * μ Eg ∧ ((∀ x ∈ Eg, a / 2 ≤ f x) ∨ ∀ x ∈ Eg, a / 2 ≤ g x)
Tactic:
constructor
Proof state after:
case h.right.left
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
⊢ MeasurableSet Eg

case h.right.right
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 ≤ 2 * μ Eg ∧ ((∀ x ∈ Eg, a / 2 ≤ f x) ∨ ∀ x ∈ Eg, a / 2 ≤ g x)
Theorem: ENNReal.le_on_subset
Proof state before:
case h.right.left
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
⊢ MeasurableSet Eg

case h.right.right
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 ≤ 2 * μ Eg ∧ ((∀ x ∈ Eg, a / 2 ≤ f x) ∨ ∀ x ∈ Eg, a / 2 ≤ g x)
Tactic:
. apply MeasurableSet.inter hE
  apply hg measurableSet_Ici
Proof state after:
case h.right.right
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 ≤ 2 * μ Eg ∧ ((∀ x ∈ Eg, a / 2 ≤ f x) ∨ ∀ x ∈ Eg, a / 2 ≤ g x)
Theorem: ENNReal.le_on_subset
Proof state before:
case h.right.right
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 ≤ 2 * μ Eg ∧ ((∀ x ∈ Eg, a / 2 ≤ f x) ∨ ∀ x ∈ Eg, a / 2 ≤ g x)
Tactic:
use hEg
Proof state after:
case right
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
⊢ (∀ x ∈ Eg, a / 2 ≤ f x) ∨ ∀ x ∈ Eg, a / 2 ≤ g x
Theorem: ENNReal.le_on_subset
Proof state before:
case right
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
⊢ (∀ x ∈ Eg, a / 2 ≤ f x) ∨ ∀ x ∈ Eg, a / 2 ≤ g x
Tactic:
right
Proof state after:
case right.h
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
⊢ ∀ x ∈ Eg, a / 2 ≤ g x
Theorem: ENNReal.le_on_subset
Proof state before:
case right.h
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
⊢ ∀ x ∈ Eg, a / 2 ≤ g x
Tactic:
rw [Eg_def]
Proof state after:
case right.h
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
⊢ ∀ x ∈ E ∩ g ⁻¹' Set.Ici (a / 2), a / 2 ≤ g x
Theorem: ENNReal.le_on_subset
Proof state before:
case right.h
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
⊢ ∀ x ∈ E ∩ g ⁻¹' Set.Ici (a / 2), a / 2 ≤ g x
Tactic:
simp
Proof state after:
no goals
Theorem: ENNReal.le_on_subset
Proof state before:
case h.left
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
⊢ Eg ⊆ E
Tactic:
apply Set.inter_subset_left
Proof state after:
no goals
Theorem: ENNReal.le_on_subset
Proof state before:
case h.right.left
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
⊢ MeasurableSet Eg
Tactic:
apply MeasurableSet.inter hE
Proof state after:
case h.right.left
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
⊢ MeasurableSet (g ⁻¹' Set.Ici (a / 2))
Theorem: ENNReal.le_on_subset
Proof state before:
case h.right.left
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
⊢ MeasurableSet (g ⁻¹' Set.Ici (a / 2))
Tactic:
apply hg measurableSet_Ici
Proof state after:
no goals
Theorem: intervalIntegral.integral_conj'
Proof state before:
μ : MeasureTheory.Measure ℝ
𝕜 : Type
inst✝ : RCLike 𝕜
f : ℝ → 𝕜
a b : ℝ
⊢ ∫ (x : ℝ) in a..b, (starRingEnd 𝕜) (f x) ∂μ = (starRingEnd 𝕜) (∫ (x : ℝ) in a..b, f x ∂μ)
Tactic:
rw [intervalIntegral_eq_integral_uIoc, integral_conj, intervalIntegral_eq_integral_uIoc,
    RCLike.real_smul_eq_coe_mul, RCLike.real_smul_eq_coe_mul, map_mul]
Proof state after:
μ : MeasureTheory.Measure ℝ
𝕜 : Type
inst✝ : RCLike 𝕜
f : ℝ → 𝕜
a b : ℝ
⊢ ↑(if a ≤ b then 1 else -1) * (starRingEnd 𝕜) (∫ (x : ℝ) in Ι a b, f x ∂μ) =
    (starRingEnd 𝕜) ↑(if a ≤ b then 1 else -1) * (starRingEnd 𝕜) (∫ (x : ℝ) in Ι a b, f x ∂μ)