internlm/Lean-Github huggingface dataset:
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 ∈ E ∩ f ⁻¹' Set.Ici (a / 2) ∪ E ∩ g ⁻¹' Set.Ici (a / 2)
Tactic:
simp
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 ∧ 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)
x : X
hx : x ∈ E
⊢ x ∈ E ∧ a / 2 ≤ f x ∨ x ∈ E ∧ a / 2 ≤ g x
Tactic:
by_contra 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
hx' : ¬(x ∈ E ∧ a / 2 ≤ f x ∨ x ∈ E ∧ a / 2 ≤ g x)
⊢ False
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
hx' : ¬(x ∈ E ∧ a / 2 ≤ f x ∨ x ∈ E ∧ a / 2 ≤ g x)
⊢ False
Tactic:
push_neg at 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
hx' : (x ∈ E → f x < a / 2) ∧ (x ∈ E → g x < a / 2)
⊢ False
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
hx' : (x ∈ E → f x < a / 2) ∧ (x ∈ E → g x < a / 2)
⊢ False
Tactic:
absurd le_refl a
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
hx' : (x ∈ E → f x < a / 2) ∧ (x ∈ E → g x < a / 2)
⊢ ¬a ≤ a
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
hx' : (x ∈ E → f x < a / 2) ∧ (x ∈ E → g x < a / 2)
⊢ ¬a ≤ a
Tactic:
push_neg
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
hx' : (x ∈ E → f x < a / 2) ∧ (x ∈ E → g x < a / 2)
⊢ a < a
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
hx' : (x ∈ E → f x < a / 2) ∧ (x ∈ E → g x < a / 2)
⊢ a < a
Tactic:
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:
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)
x : X
hx : x ∈ E
hx' : (x ∈ E → f x < a / 2) ∧ (x ∈ E → g x < a / 2)
⊢ f x + g x < a / 2 + a / 2
Tactic:
gcongr
Proof state after:
case ac
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
hx' : (x ∈ E → f x < a / 2) ∧ (x ∈ E → g x < a / 2)
⊢ f x < a / 2

case bd
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
hx' : (x ∈ E → f x < a / 2) ∧ (x ∈ E → g x < a / 2)
⊢ g x < a / 2
Theorem: ENNReal.le_on_subset
Proof state before:
case ac
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
hx' : (x ∈ E → f x < a / 2) ∧ (x ∈ E → g x < a / 2)
⊢ f x < a / 2

case bd
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
hx' : (x ∈ E → f x < a / 2) ∧ (x ∈ E → g x < a / 2)
⊢ g x < a / 2
Tactic:
. exact hx'.1 hx
Proof state after:
case bd
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
hx' : (x ∈ E → f x < a / 2) ∧ (x ∈ E → g x < a / 2)
⊢ g x < a / 2
Theorem: ENNReal.le_on_subset
Proof state before:
case bd
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
hx' : (x ∈ E → f x < a / 2) ∧ (x ∈ E → g x < a / 2)
⊢ g x < a / 2
Tactic:
. exact hx'.2 hx
Proof state after:
no goals
Theorem: ENNReal.le_on_subset
Proof state before:
case ac
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
hx' : (x ∈ E → f x < a / 2) ∧ (x ∈ E → g x < a / 2)
⊢ f x < a / 2
Tactic:
exact hx'.1 hx
Proof state after:
no goals
Theorem: ENNReal.le_on_subset
Proof state before:
case bd
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
hx' : (x ∈ E → f x < a / 2) ∧ (x ∈ E → g x < a / 2)
⊢ g x < a / 2
Tactic:
exact hx'.2 hx
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)
x : X
hx : x ∈ E
hx' : (x ∈ E → f x < a / 2) ∧ (x ∈ E → g x < a / 2)
⊢ a / 2 + a / 2 = a
Tactic:
ring_nf
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
hx' : (x ∈ E → f x < a / 2) ∧ (x ∈ E → g x < a / 2)
⊢ a / 2 * 2 = a
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
hx' : (x ∈ E → f x < a / 2) ∧ (x ∈ E → g x < a / 2)
⊢ a / 2 * 2 = a
Tactic:
apply ENNReal.div_mul_cancel <;> norm_num
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)
this : E ⊆ Ef ∪ Eg
⊢ μ E ≤ 2 * μ Ef ∨ μ E ≤ 2 * μ Eg
Tactic:
by_contra hEfg
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
hEfg : ¬(μ E ≤ 2 * μ Ef ∨ μ E ≤ 2 * μ Eg)
⊢ False
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
hEfg : ¬(μ E ≤ 2 * μ Ef ∨ μ E ≤ 2 * μ Eg)
⊢ False
Tactic:
push_neg at hEfg
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
hEfg : 2 * μ Ef < μ E ∧ 2 * μ Eg < μ E
⊢ False
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
hEfg : 2 * μ Ef < μ E ∧ 2 * μ Eg < μ E
⊢ False
Tactic:
absurd le_refl (2 * μ E)
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
hEfg : 2 * μ Ef < μ E ∧ 2 * μ Eg < μ E
⊢ ¬2 * μ E ≤ 2 * μ E
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
hEfg : 2 * μ Ef < μ E ∧ 2 * μ Eg < μ E
⊢ ¬2 * μ E ≤ 2 * μ E
Tactic:
push_neg
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
hEfg : 2 * μ Ef < μ E ∧ 2 * μ Eg < μ E
⊢ 2 * μ E < 2 * μ E
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
hEfg : 2 * μ Ef < μ E ∧ 2 * μ Eg < μ E
⊢ 2 * μ E < 2 * μ E
Tactic:
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:
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)
this : E ⊆ Ef ∪ Eg
hEfg : 2 * μ Ef < μ E ∧ 2 * μ Eg < μ E
⊢ 2 * μ E ≤ 2 * μ (Ef ∪ Eg)
Tactic:
gcongr
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)
this : E ⊆ Ef ∪ Eg
hEfg : 2 * μ Ef < μ E ∧ 2 * μ Eg < μ E
⊢ 2 * μ (Ef ∪ Eg) ≤ 2 * (μ Ef + μ Eg)
Tactic:
gcongr
Proof state after:
case bc
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
hEfg : 2 * μ Ef < μ E ∧ 2 * μ Eg < μ E
⊢ μ (Ef ∪ Eg) ≤ μ Ef + μ Eg
Theorem: ENNReal.le_on_subset
Proof state before:
case bc
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
hEfg : 2 * μ Ef < μ E ∧ 2 * μ Eg < μ E
⊢ μ (Ef ∪ Eg) ≤ μ Ef + μ Eg
Tactic:
apply MeasureTheory.measure_union_le
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)
this : E ⊆ Ef ∪ Eg
hEfg : 2 * μ Ef < μ E ∧ 2 * μ Eg < μ E
⊢ 2 * (μ Ef + μ Eg) = 2 * μ Ef + 2 * μ Eg
Tactic:
ring
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)
this : E ⊆ Ef ∪ Eg
hEfg : 2 * μ Ef < μ E ∧ 2 * μ Eg < μ E
⊢ 2 * μ Ef + 2 * μ Eg < μ E + μ E
Tactic:
gcongr
Proof state after:
case ac
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
hEfg : 2 * μ Ef < μ E ∧ 2 * μ Eg < μ E
⊢ 2 * μ Ef < μ E

case bd
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
hEfg : 2 * μ Ef < μ E ∧ 2 * μ Eg < μ E
⊢ 2 * μ Eg < μ E
Theorem: ENNReal.le_on_subset
Proof state before:
case ac
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
hEfg : 2 * μ Ef < μ E ∧ 2 * μ Eg < μ E
⊢ 2 * μ Ef < μ E

case bd
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
hEfg : 2 * μ Ef < μ E ∧ 2 * μ Eg < μ E
⊢ 2 * μ Eg < μ E
Tactic:
. exact hEfg.1
Proof state after:
case bd
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
hEfg : 2 * μ Ef < μ E ∧ 2 * μ Eg < μ E
⊢ 2 * μ Eg < μ E
Theorem: ENNReal.le_on_subset
Proof state before:
case bd
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
hEfg : 2 * μ Ef < μ E ∧ 2 * μ Eg < μ E
⊢ 2 * μ Eg < μ E
Tactic:
. exact hEfg.2
Proof state after:
no goals
Theorem: ENNReal.le_on_subset
Proof state before:
case ac
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
hEfg : 2 * μ Ef < μ E ∧ 2 * μ Eg < μ E
⊢ 2 * μ Ef < μ E
Tactic:
exact hEfg.1
Proof state after:
no goals
Theorem: ENNReal.le_on_subset
Proof state before:
case bd
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
hEfg : 2 * μ Ef < μ E ∧ 2 * μ Eg < μ E
⊢ 2 * μ Eg < μ E
Tactic:
exact hEfg.2
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)
this : E ⊆ Ef ∪ Eg
hEfg : 2 * μ Ef < μ E ∧ 2 * μ Eg < μ E
⊢ μ E + μ E = 2 * μ E
Tactic:
ring
Proof state after:
no goals
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)
Tactic:
use Ef
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
hEf : μ E ≤ 2 * μ Ef
⊢ Ef ⊆ E ∧ MeasurableSet Ef ∧ μ E ≤ 2 * μ Ef ∧ ((∀ x ∈ Ef, a / 2 ≤ f x) ∨ ∀ x ∈ Ef, a / 2 ≤ g x)