Theorem: ENNReal.le_on_subset (Carleson/Theorem1_1/Control_Approximation_Effect.lean)

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
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)

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
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)

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
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)

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
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)

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
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)

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
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)

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
State after:
no goals

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
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

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]
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)

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
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

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'
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

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'
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

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
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

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
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

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
State after:
no goals

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
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

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
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

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
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

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
State after:
no goals

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
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

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
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

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)
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

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
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

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
State after:
no goals

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
State after:
no goals

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
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

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
State after:
no goals

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
State after:
no goals

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
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

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
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

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
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)

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
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)

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
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)

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
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)

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
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)

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
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

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
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

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]
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

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
State after:
no goals

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
State after:
no goals

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
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))

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
State after:
no goals

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
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)

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
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)

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
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)

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
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)

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
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)

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
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

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
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

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]
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

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
State after:
no goals

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
State after:
no goals

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
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))

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
State after:
no goals