case h_ind
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ∫⁻ (x : α), ↑(↑(piecewise s hs (const α c) (const α 0)) x) ∂μ
⊢ ∃ g,
    (∀ (x : α), ↑g x ≤ ↑(piecewise s hs (const α c) (const α 0)) x) ∧
      (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ

case h_add
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hL : L < ∫⁻ (x : α), ↑(↑(f₁ + f₂) x) ∂μ
⊢ ∃ g, (∀ (x : α), ↑g x ≤ ↑(f₁ + f₂) x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L : ℝ≥0∞
hL : L < ∫⁻ (x : α), ↑(↑f x) ∂μ
⊢ ∃ g, (∀ (x : α), ↑g x ≤ ↑f x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
induction' f using MeasureTheory.SimpleFunc.induction with c s hs f₁ f₂ _ h₁ h₂ generalizing L
case h_ind
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * ↑↑μ s
⊢ ∃ g,
    (∀ (x : α), ↑g x ≤ ↑(piecewise s hs (const α c) (const α 0)) x) ∧
      (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
case h_ind
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ∫⁻ (x : α), ↑(↑(piecewise s hs (const α c) (const α 0)) x) ∂μ
⊢ ∃ g,
    (∀ (x : α), ↑g x ≤ ↑(piecewise s hs (const α c) (const α 0)) x) ∧
      (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
simp only [hs, const_zero, coe_piecewise, coe_const, SimpleFunc.coe_zero, univ_inter,
  piecewise_eq_indicator, lintegral_indicator, lintegral_const, Measure.restrict_apply',
  ENNReal.coe_indicator, Function.const_apply] at hL
case h_ind
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * ↑↑μ s
c_ne_zero : c ≠ 0
⊢ ∃ g,
    (∀ (x : α), ↑g x ≤ ↑(piecewise s hs (const α c) (const α 0)) x) ∧
      (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
case h_ind
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * ↑↑μ s
⊢ ∃ g,
    (∀ (x : α), ↑g x ≤ ↑(piecewise s hs (const α c) (const α 0)) x) ∧
      (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
have c_ne_zero : c ≠ 0 := by
  intro hc
  simp only [hc, ENNReal.coe_zero, MulZeroClass.zero_mul, not_lt_zero] at hL
case h_ind.intro.intro.intro.intro
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * ↑↑μ s
c_ne_zero : c ≠ 0
this : L / ↑c < ↑↑μ s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / ↑c < ↑↑μ t
t_top : ↑↑μ t < ⊤
⊢ ∃ g,
    (∀ (x : α), ↑g x ≤ ↑(piecewise s hs (const α c) (const α 0)) x) ∧
      (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
case h_ind
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * ↑↑μ s
c_ne_zero : c ≠ 0
this : L / ↑c < ↑↑μ s
⊢ ∃ g,
    (∀ (x : α), ↑g x ≤ ↑(piecewise s hs (const α c) (const α 0)) x) ∧
      (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
obtain ⟨t, ht, ts, mlt, t_top⟩ :
  ∃ t : Set α, MeasurableSet t ∧ t ⊆ s ∧ L / ↑c < μ t ∧ μ t < ∞ :=
  Measure.exists_subset_measure_lt_top hs this
case h_ind.intro.intro.intro.intro.refine'_1
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * ↑↑μ s
c_ne_zero : c ≠ 0
this : L / ↑c < ↑↑μ s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / ↑c < ↑↑μ t
t_top : ↑↑μ t < ⊤
x : α
⊢ ↑(piecewise t ht (const α c) (const α 0)) x ≤ ↑(piecewise s hs (const α c) (const α 0)) x

case h_ind.intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * ↑↑μ s
c_ne_zero : c ≠ 0
this : L / ↑c < ↑↑μ s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / ↑c < ↑↑μ t
t_top : ↑↑μ t < ⊤
⊢ (∫⁻ (x : α), ↑(↑(piecewise t ht (const α c) (const α 0)) x) ∂μ) < ⊤

case h_ind.intro.intro.intro.intro.refine'_3
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * ↑↑μ s
c_ne_zero : c ≠ 0
this : L / ↑c < ↑↑μ s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / ↑c < ↑↑μ t
t_top : ↑↑μ t < ⊤
⊢ L < ∫⁻ (x : α), ↑(↑(piecewise t ht (const α c) (const α 0)) x) ∂μ
case h_ind.intro.intro.intro.intro
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * ↑↑μ s
c_ne_zero : c ≠ 0
this : L / ↑c < ↑↑μ s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / ↑c < ↑↑μ t
t_top : ↑↑μ t < ⊤
⊢ ∃ g,
    (∀ (x : α), ↑g x ≤ ↑(piecewise s hs (const α c) (const α 0)) x) ∧
      (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
refine' ⟨piecewise t ht (const α c) (const α 0), fun x => _, _, _⟩
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * ↑↑μ s
hc : c = 0
⊢ False
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * ↑↑μ s
⊢ c ≠ 0
intro hc
no goals
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * ↑↑μ s
hc : c = 0
⊢ False
simp only [hc, ENNReal.coe_zero, MulZeroClass.zero_mul, not_lt_zero] at hL
case h0
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * ↑↑μ s
c_ne_zero : c ≠ 0
⊢ ↑c ≠ 0 ∨ L ≠ 0

case ht
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * ↑↑μ s
c_ne_zero : c ≠ 0
⊢ ↑c ≠ ⊤ ∨ L ≠ ⊤
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * ↑↑μ s
c_ne_zero : c ≠ 0
⊢ L / ↑c < ↑↑μ s
rwa [ENNReal.div_lt_iff, mul_comm]
no goals
case h0
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * ↑↑μ s
c_ne_zero : c ≠ 0
⊢ ↑c ≠ 0 ∨ L ≠ 0
simp only [c_ne_zero, Ne.def, coe_eq_zero, not_false_iff, true_or_iff]
no goals
case ht
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * ↑↑μ s
c_ne_zero : c ≠ 0
⊢ ↑c ≠ ⊤ ∨ L ≠ ⊤
simp only [Ne.def, coe_ne_top, not_false_iff, true_or_iff]
case h_ind.intro.intro.intro.intro.refine'_1
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * ↑↑μ s
c_ne_zero : c ≠ 0
this : L / ↑c < ↑↑μ s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / ↑c < ↑↑μ t
t_top : ↑↑μ t < ⊤
x✝ x : α
⊢ 0 ≤ ↑(const α c) x
case h_ind.intro.intro.intro.intro.refine'_1
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * ↑↑μ s
c_ne_zero : c ≠ 0
this : L / ↑c < ↑↑μ s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / ↑c < ↑↑μ t
t_top : ↑↑μ t < ⊤
x : α
⊢ ↑(piecewise t ht (const α c) (const α 0)) x ≤ ↑(piecewise s hs (const α c) (const α 0)) x
refine indicator_le_indicator_of_subset ts (fun x => ?_) x
no goals
case h_ind.intro.intro.intro.intro.refine'_1
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * ↑↑μ s
c_ne_zero : c ≠ 0
this : L / ↑c < ↑↑μ s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / ↑c < ↑↑μ t
t_top : ↑↑μ t < ⊤
x✝ x : α
⊢ 0 ≤ ↑(const α c) x
exact zero_le _
no goals
case h_ind.intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * ↑↑μ s
c_ne_zero : c ≠ 0
this : L / ↑c < ↑↑μ s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / ↑c < ↑↑μ t
t_top : ↑↑μ t < ⊤
⊢ (∫⁻ (x : α), ↑(↑(piecewise t ht (const α c) (const α 0)) x) ∂μ) < ⊤
simp only [ht, const_zero, coe_piecewise, coe_const, SimpleFunc.coe_zero, univ_inter,
  piecewise_eq_indicator, ENNReal.coe_indicator, Function.const_apply, lintegral_indicator,
  lintegral_const, Measure.restrict_apply', ENNReal.mul_lt_top ENNReal.coe_ne_top t_top.ne]
case h_ind.intro.intro.intro.intro.refine'_3
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * ↑↑μ s
c_ne_zero : c ≠ 0
this : L / ↑c < ↑↑μ s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / ↑c < ↑↑μ t
t_top : ↑↑μ t < ⊤
⊢ L < ↑c * ↑↑μ t
case h_ind.intro.intro.intro.intro.refine'_3
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * ↑↑μ s
c_ne_zero : c ≠ 0
this : L / ↑c < ↑↑μ s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / ↑c < ↑↑μ t
t_top : ↑↑μ t < ⊤
⊢ L < ∫⁻ (x : α), ↑(↑(piecewise t ht (const α c) (const α 0)) x) ∂μ
simp only [ht, const_zero, coe_piecewise, coe_const, SimpleFunc.coe_zero,
  piecewise_eq_indicator, ENNReal.coe_indicator, Function.const_apply, lintegral_indicator,
  lintegral_const, Measure.restrict_apply', univ_inter]
case h_ind.intro.intro.intro.intro.refine'_3.h0
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * ↑↑μ s
c_ne_zero : c ≠ 0
this : L / ↑c < ↑↑μ s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / ↑c < ↑↑μ t
t_top : ↑↑μ t < ⊤
⊢ ↑c ≠ 0 ∨ L ≠ 0

case h_ind.intro.intro.intro.intro.refine'_3.ht
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * ↑↑μ s
c_ne_zero : c ≠ 0
this : L / ↑c < ↑↑μ s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / ↑c < ↑↑μ t
t_top : ↑↑μ t < ⊤
⊢ ↑c ≠ ⊤ ∨ L ≠ ⊤
case h_ind.intro.intro.intro.intro.refine'_3
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * ↑↑μ s
c_ne_zero : c ≠ 0
this : L / ↑c < ↑↑μ s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / ↑c < ↑↑μ t
t_top : ↑↑μ t < ⊤
⊢ L < ↑c * ↑↑μ t
rwa [mul_comm, ← ENNReal.div_lt_iff]
no goals
case h_ind.intro.intro.intro.intro.refine'_3.h0
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * ↑↑μ s
c_ne_zero : c ≠ 0
this : L / ↑c < ↑↑μ s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / ↑c < ↑↑μ t
t_top : ↑↑μ t < ⊤
⊢ ↑c ≠ 0 ∨ L ≠ 0
simp only [c_ne_zero, Ne.def, coe_eq_zero, not_false_iff, true_or_iff]
no goals
case h_ind.intro.intro.intro.intro.refine'_3.ht
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * ↑↑μ s
c_ne_zero : c ≠ 0
this : L / ↑c < ↑↑μ s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / ↑c < ↑↑μ t
t_top : ↑↑μ t < ⊤
⊢ ↑c ≠ ⊤ ∨ L ≠ ⊤
simp only [Ne.def, coe_ne_top, not_false_iff, true_or_iff]
case hL
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hL : L < ∫⁻ (x : α), ↑(↑(f₁ + f₂) x) ∂μ
⊢ L < (∫⁻ (x : α), ↑(↑f₁ x) ∂μ) + ∫⁻ (x : α), ↑(↑f₂ x) ∂μ

case h_add
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hL : L < (∫⁻ (x : α), ↑(↑f₁ x) ∂μ) + ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
⊢ ∃ g, (∀ (x : α), ↑g x ≤ ↑(f₁ + f₂) x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
case h_add
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hL : L < ∫⁻ (x : α), ↑(↑(f₁ + f₂) x) ∂μ
⊢ ∃ g, (∀ (x : α), ↑g x ≤ ↑(f₁ + f₂) x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
replace hL : L < (∫⁻ x, f₁ x ∂μ) + ∫⁻ x, f₂ x ∂μ
case pos
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hL : L < (∫⁻ (x : α), ↑(↑f₁ x) ∂μ) + ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hf₁ : (∫⁻ (x : α), ↑(↑f₁ x) ∂μ) = 0
⊢ ∃ g, (∀ (x : α), ↑g x ≤ ↑(f₁ + f₂) x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ

case neg
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hL : L < (∫⁻ (x : α), ↑(↑f₁ x) ∂μ) + ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hf₁ : ¬(∫⁻ (x : α), ↑(↑f₁ x) ∂μ) = 0
⊢ ∃ g, (∀ (x : α), ↑g x ≤ ↑(f₁ + f₂) x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
case h_add
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hL : L < (∫⁻ (x : α), ↑(↑f₁ x) ∂μ) + ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
⊢ ∃ g, (∀ (x : α), ↑g x ≤ ↑(f₁ + f₂) x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
by_cases hf₁ : (∫⁻ x, f₁ x ∂μ) = 0
case pos
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hL : L < (∫⁻ (x : α), ↑(↑f₁ x) ∂μ) + ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hf₁ : ¬(∫⁻ (x : α), ↑(↑f₁ x) ∂μ) = 0
hf₂ : (∫⁻ (x : α), ↑(↑f₂ x) ∂μ) = 0
⊢ ∃ g, (∀ (x : α), ↑g x ≤ ↑(f₁ + f₂) x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ

case neg
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hL : L < (∫⁻ (x : α), ↑(↑f₁ x) ∂μ) + ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hf₁ : ¬(∫⁻ (x : α), ↑(↑f₁ x) ∂μ) = 0
hf₂ : ¬(∫⁻ (x : α), ↑(↑f₂ x) ∂μ) = 0
⊢ ∃ g, (∀ (x : α), ↑g x ≤ ↑(f₁ + f₂) x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
case neg
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hL : L < (∫⁻ (x : α), ↑(↑f₁ x) ∂μ) + ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hf₁ : ¬(∫⁻ (x : α), ↑(↑f₁ x) ∂μ) = 0
⊢ ∃ g, (∀ (x : α), ↑g x ≤ ↑(f₁ + f₂) x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
by_cases hf₂ : (∫⁻ x, f₂ x ∂μ) = 0
case neg.intro.intro.intro.intro
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝¹ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hL✝ : L < (∫⁻ (x : α), ↑(↑f₁ x) ∂μ) + ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hf₁ : ¬(∫⁻ (x : α), ↑(↑f₁ x) ∂μ) = 0
hf₂ : ¬(∫⁻ (x : α), ↑(↑f₂ x) ∂μ) = 0
L₁ L₂ : ℝ≥0∞
hL₁ : L₁ < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ
hL₂ : L₂ < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hL : L < L₁ + L₂
⊢ ∃ g, (∀ (x : α), ↑g x ≤ ↑(f₁ + f₂) x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
case neg
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hL : L < (∫⁻ (x : α), ↑(↑f₁ x) ∂μ) + ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hf₁ : ¬(∫⁻ (x : α), ↑(↑f₁ x) ∂μ) = 0
hf₂ : ¬(∫⁻ (x : α), ↑(↑f₂ x) ∂μ) = 0
⊢ ∃ g, (∀ (x : α), ↑g x ≤ ↑(f₁ + f₂) x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
obtain ⟨L₁, L₂, hL₁, hL₂, hL⟩ :
  ∃ L₁ L₂ : ℝ≥0∞, (L₁ < ∫⁻ x, f₁ x ∂μ) ∧ (L₂ < ∫⁻ x, f₂ x ∂μ) ∧ L < L₁ + L₂ :=
  ENNReal.exists_lt_add_of_lt_add hL hf₁ hf₂
case neg.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝¹ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hL✝ : L < (∫⁻ (x : α), ↑(↑f₁ x) ∂μ) + ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hf₁ : ¬(∫⁻ (x : α), ↑(↑f₁ x) ∂μ) = 0
hf₂ : ¬(∫⁻ (x : α), ↑(↑f₂ x) ∂μ) = 0
L₁ L₂ : ℝ≥0∞
hL₁ : L₁ < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ
hL₂ : L₂ < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hL : L < L₁ + L₂
g₁ : α →ₛ ℝ≥0
g₁_le : ∀ (x : α), ↑g₁ x ≤ ↑f₁ x
g₁_top : (∫⁻ (x : α), ↑(↑g₁ x) ∂μ) < ⊤
hg₁ : L₁ < ∫⁻ (x : α), ↑(↑g₁ x) ∂μ
⊢ ∃ g, (∀ (x : α), ↑g x ≤ ↑(f₁ + f₂) x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
case neg.intro.intro.intro.intro
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝¹ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hL✝ : L < (∫⁻ (x : α), ↑(↑f₁ x) ∂μ) + ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hf₁ : ¬(∫⁻ (x : α), ↑(↑f₁ x) ∂μ) = 0
hf₂ : ¬(∫⁻ (x : α), ↑(↑f₂ x) ∂μ) = 0
L₁ L₂ : ℝ≥0∞
hL₁ : L₁ < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ
hL₂ : L₂ < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hL : L < L₁ + L₂
⊢ ∃ g, (∀ (x : α), ↑g x ≤ ↑(f₁ + f₂) x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
rcases h₁ hL₁ with ⟨g₁, g₁_le, g₁_top, hg₁⟩
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝¹ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hL✝ : L < (∫⁻ (x : α), ↑(↑f₁ x) ∂μ) + ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hf₁ : ¬(∫⁻ (x : α), ↑(↑f₁ x) ∂μ) = 0
hf₂ : ¬(∫⁻ (x : α), ↑(↑f₂ x) ∂μ) = 0
L₁ L₂ : ℝ≥0∞
hL₁ : L₁ < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ
hL₂ : L₂ < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hL : L < L₁ + L₂
g₁ : α →ₛ ℝ≥0
g₁_le : ∀ (x : α), ↑g₁ x ≤ ↑f₁ x
g₁_top : (∫⁻ (x : α), ↑(↑g₁ x) ∂μ) < ⊤
hg₁ : L₁ < ∫⁻ (x : α), ↑(↑g₁ x) ∂μ
g₂ : α →ₛ ℝ≥0
g₂_le : ∀ (x : α), ↑g₂ x ≤ ↑f₂ x
g₂_top : (∫⁻ (x : α), ↑(↑g₂ x) ∂μ) < ⊤
hg₂ : L₂ < ∫⁻ (x : α), ↑(↑g₂ x) ∂μ
⊢ ∃ g, (∀ (x : α), ↑g x ≤ ↑(f₁ + f₂) x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
case neg.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝¹ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hL✝ : L < (∫⁻ (x : α), ↑(↑f₁ x) ∂μ) + ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hf₁ : ¬(∫⁻ (x : α), ↑(↑f₁ x) ∂μ) = 0
hf₂ : ¬(∫⁻ (x : α), ↑(↑f₂ x) ∂μ) = 0
L₁ L₂ : ℝ≥0∞
hL₁ : L₁ < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ
hL₂ : L₂ < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hL : L < L₁ + L₂
g₁ : α →ₛ ℝ≥0
g₁_le : ∀ (x : α), ↑g₁ x ≤ ↑f₁ x
g₁_top : (∫⁻ (x : α), ↑(↑g₁ x) ∂μ) < ⊤
hg₁ : L₁ < ∫⁻ (x : α), ↑(↑g₁ x) ∂μ
⊢ ∃ g, (∀ (x : α), ↑g x ≤ ↑(f₁ + f₂) x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
rcases h₂ hL₂ with ⟨g₂, g₂_le, g₂_top, hg₂⟩
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝¹ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hL✝ : L < (∫⁻ (x : α), ↑(↑f₁ x) ∂μ) + ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hf₁ : ¬(∫⁻ (x : α), ↑(↑f₁ x) ∂μ) = 0
hf₂ : ¬(∫⁻ (x : α), ↑(↑f₂ x) ∂μ) = 0
L₁ L₂ : ℝ≥0∞
hL₁ : L₁ < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ
hL₂ : L₂ < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hL : L < L₁ + L₂
g₁ : α →ₛ ℝ≥0
g₁_le : ∀ (x : α), ↑g₁ x ≤ ↑f₁ x
g₁_top : (∫⁻ (x : α), ↑(↑g₁ x) ∂μ) < ⊤
hg₁ : L₁ < ∫⁻ (x : α), ↑(↑g₁ x) ∂μ
g₂ : α →ₛ ℝ≥0
g₂_le : ∀ (x : α), ↑g₂ x ≤ ↑f₂ x
g₂_top : (∫⁻ (x : α), ↑(↑g₂ x) ∂μ) < ⊤
hg₂ : L₂ < ∫⁻ (x : α), ↑(↑g₂ x) ∂μ
⊢ (∫⁻ (x : α), ↑(↑(g₁ + g₂) x) ∂μ) < ⊤

case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝¹ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hL✝ : L < (∫⁻ (x : α), ↑(↑f₁ x) ∂μ) + ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hf₁ : ¬(∫⁻ (x : α), ↑(↑f₁ x) ∂μ) = 0
hf₂ : ¬(∫⁻ (x : α), ↑(↑f₂ x) ∂μ) = 0
L₁ L₂ : ℝ≥0∞
hL₁ : L₁ < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ
hL₂ : L₂ < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hL : L < L₁ + L₂
g₁ : α →ₛ ℝ≥0
g₁_le : ∀ (x : α), ↑g₁ x ≤ ↑f₁ x
g₁_top : (∫⁻ (x : α), ↑(↑g₁ x) ∂μ) < ⊤
hg₁ : L₁ < ∫⁻ (x : α), ↑(↑g₁ x) ∂μ
g₂ : α →ₛ ℝ≥0
g₂_le : ∀ (x : α), ↑g₂ x ≤ ↑f₂ x
g₂_top : (∫⁻ (x : α), ↑(↑g₂ x) ∂μ) < ⊤
hg₂ : L₂ < ∫⁻ (x : α), ↑(↑g₂ x) ∂μ
⊢ L < ∫⁻ (x : α), ↑(↑(g₁ + g₂) x) ∂μ
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝¹ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hL✝ : L < (∫⁻ (x : α), ↑(↑f₁ x) ∂μ) + ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hf₁ : ¬(∫⁻ (x : α), ↑(↑f₁ x) ∂μ) = 0
hf₂ : ¬(∫⁻ (x : α), ↑(↑f₂ x) ∂μ) = 0
L₁ L₂ : ℝ≥0∞
hL₁ : L₁ < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ
hL₂ : L₂ < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hL : L < L₁ + L₂
g₁ : α →ₛ ℝ≥0
g₁_le : ∀ (x : α), ↑g₁ x ≤ ↑f₁ x
g₁_top : (∫⁻ (x : α), ↑(↑g₁ x) ∂μ) < ⊤
hg₁ : L₁ < ∫⁻ (x : α), ↑(↑g₁ x) ∂μ
g₂ : α →ₛ ℝ≥0
g₂_le : ∀ (x : α), ↑g₂ x ≤ ↑f₂ x
g₂_top : (∫⁻ (x : α), ↑(↑g₂ x) ∂μ) < ⊤
hg₂ : L₂ < ∫⁻ (x : α), ↑(↑g₂ x) ∂μ
⊢ ∃ g, (∀ (x : α), ↑g x ≤ ↑(f₁ + f₂) x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
refine' ⟨g₁ + g₂, fun x => add_le_add (g₁_le x) (g₂_le x), _, _⟩
no goals
case hL
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hL : L < ∫⁻ (x : α), ↑(↑(f₁ + f₂) x) ∂μ
⊢ L < (∫⁻ (x : α), ↑(↑f₁ x) ∂μ) + ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
rwa [← lintegral_add_left f₁.measurable.coe_nnreal_ennreal]
case pos
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hf₁ : (∫⁻ (x : α), ↑(↑f₁ x) ∂μ) = 0
hL : L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
⊢ ∃ g, (∀ (x : α), ↑g x ≤ ↑(f₁ + f₂) x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
case pos
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hL : L < (∫⁻ (x : α), ↑(↑f₁ x) ∂μ) + ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hf₁ : (∫⁻ (x : α), ↑(↑f₁ x) ∂μ) = 0
⊢ ∃ g, (∀ (x : α), ↑g x ≤ ↑(f₁ + f₂) x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
simp only [hf₁, zero_add] at hL
case pos.intro.intro.intro
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hf₁ : (∫⁻ (x : α), ↑(↑f₁ x) ∂μ) = 0
hL : L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
g : α →ₛ ℝ≥0
g_le : ∀ (x : α), ↑g x ≤ ↑f₂ x
g_top : (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤
gL : L < ∫⁻ (x : α), ↑(↑g x) ∂μ
⊢ ∃ g, (∀ (x : α), ↑g x ≤ ↑(f₁ + f₂) x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
case pos
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hf₁ : (∫⁻ (x : α), ↑(↑f₁ x) ∂μ) = 0
hL : L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
⊢ ∃ g, (∀ (x : α), ↑g x ≤ ↑(f₁ + f₂) x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
rcases h₂ hL with ⟨g, g_le, g_top, gL⟩
case pos.intro.intro.intro
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hf₁ : (∫⁻ (x : α), ↑(↑f₁ x) ∂μ) = 0
hL : L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
g : α →ₛ ℝ≥0
g_le : ∀ (x : α), ↑g x ≤ ↑f₂ x
g_top : (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤
gL : L < ∫⁻ (x : α), ↑(↑g x) ∂μ
x : α
⊢ ↑f₂ x ≤ ↑(f₁ + f₂) x
case pos.intro.intro.intro
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hf₁ : (∫⁻ (x : α), ↑(↑f₁ x) ∂μ) = 0
hL : L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
g : α →ₛ ℝ≥0
g_le : ∀ (x : α), ↑g x ≤ ↑f₂ x
g_top : (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤
gL : L < ∫⁻ (x : α), ↑(↑g x) ∂μ
⊢ ∃ g, (∀ (x : α), ↑g x ≤ ↑(f₁ + f₂) x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
refine' ⟨g, fun x => (g_le x).trans _, g_top, gL⟩
no goals
case pos.intro.intro.intro
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hf₁ : (∫⁻ (x : α), ↑(↑f₁ x) ∂μ) = 0
hL : L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
g : α →ₛ ℝ≥0
g_le : ∀ (x : α), ↑g x ≤ ↑f₂ x
g_top : (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤
gL : L < ∫⁻ (x : α), ↑(↑g x) ∂μ
x : α
⊢ ↑f₂ x ≤ ↑(f₁ + f₂) x
simp only [SimpleFunc.coe_add, Pi.add_apply, le_add_iff_nonneg_left, zero_le']
case pos
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hf₁ : ¬(∫⁻ (x : α), ↑(↑f₁ x) ∂μ) = 0
hf₂ : (∫⁻ (x : α), ↑(↑f₂ x) ∂μ) = 0
hL : L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ
⊢ ∃ g, (∀ (x : α), ↑g x ≤ ↑(f₁ + f₂) x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
case pos
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hL : L < (∫⁻ (x : α), ↑(↑f₁ x) ∂μ) + ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hf₁ : ¬(∫⁻ (x : α), ↑(↑f₁ x) ∂μ) = 0
hf₂ : (∫⁻ (x : α), ↑(↑f₂ x) ∂μ) = 0
⊢ ∃ g, (∀ (x : α), ↑g x ≤ ↑(f₁ + f₂) x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
simp only [hf₂, add_zero] at hL
case pos.intro.intro.intro
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hf₁ : ¬(∫⁻ (x : α), ↑(↑f₁ x) ∂μ) = 0
hf₂ : (∫⁻ (x : α), ↑(↑f₂ x) ∂μ) = 0
hL : L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ
g : α →ₛ ℝ≥0
g_le : ∀ (x : α), ↑g x ≤ ↑f₁ x
g_top : (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤
gL : L < ∫⁻ (x : α), ↑(↑g x) ∂μ
⊢ ∃ g, (∀ (x : α), ↑g x ≤ ↑(f₁ + f₂) x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
case pos
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hf₁ : ¬(∫⁻ (x : α), ↑(↑f₁ x) ∂μ) = 0
hf₂ : (∫⁻ (x : α), ↑(↑f₂ x) ∂μ) = 0
hL : L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ
⊢ ∃ g, (∀ (x : α), ↑g x ≤ ↑(f₁ + f₂) x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
rcases h₁ hL with ⟨g, g_le, g_top, gL⟩
case pos.intro.intro.intro
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hf₁ : ¬(∫⁻ (x : α), ↑(↑f₁ x) ∂μ) = 0
hf₂ : (∫⁻ (x : α), ↑(↑f₂ x) ∂μ) = 0
hL : L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ
g : α →ₛ ℝ≥0
g_le : ∀ (x : α), ↑g x ≤ ↑f₁ x
g_top : (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤
gL : L < ∫⁻ (x : α), ↑(↑g x) ∂μ
x : α
⊢ ↑f₁ x ≤ ↑(f₁ + f₂) x
case pos.intro.intro.intro
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hf₁ : ¬(∫⁻ (x : α), ↑(↑f₁ x) ∂μ) = 0
hf₂ : (∫⁻ (x : α), ↑(↑f₂ x) ∂μ) = 0
hL : L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ
g : α →ₛ ℝ≥0
g_le : ∀ (x : α), ↑g x ≤ ↑f₁ x
g_top : (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤
gL : L < ∫⁻ (x : α), ↑(↑g x) ∂μ
⊢ ∃ g, (∀ (x : α), ↑g x ≤ ↑(f₁ + f₂) x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
refine' ⟨g, fun x => (g_le x).trans _, g_top, gL⟩
no goals
case pos.intro.intro.intro
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hf₁ : ¬(∫⁻ (x : α), ↑(↑f₁ x) ∂μ) = 0
hf₂ : (∫⁻ (x : α), ↑(↑f₂ x) ∂μ) = 0
hL : L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ
g : α →ₛ ℝ≥0
g_le : ∀ (x : α), ↑g x ≤ ↑f₁ x
g_top : (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤
gL : L < ∫⁻ (x : α), ↑(↑g x) ∂μ
x : α
⊢ ↑f₁ x ≤ ↑(f₁ + f₂) x
simp only [SimpleFunc.coe_add, Pi.add_apply, le_add_iff_nonneg_right, zero_le']
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝¹ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hL✝ : L < (∫⁻ (x : α), ↑(↑f₁ x) ∂μ) + ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hf₁ : ¬(∫⁻ (x : α), ↑(↑f₁ x) ∂μ) = 0
hf₂ : ¬(∫⁻ (x : α), ↑(↑f₂ x) ∂μ) = 0
L₁ L₂ : ℝ≥0∞
hL₁ : L₁ < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ
hL₂ : L₂ < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hL : L < L₁ + L₂
g₁ : α →ₛ ℝ≥0
g₁_le : ∀ (x : α), ↑g₁ x ≤ ↑f₁ x
g₁_top : (∫⁻ (x : α), ↑(↑g₁ x) ∂μ) < ⊤
hg₁ : L₁ < ∫⁻ (x : α), ↑(↑g₁ x) ∂μ
g₂ : α →ₛ ℝ≥0
g₂_le : ∀ (x : α), ↑g₂ x ≤ ↑f₂ x
g₂_top : (∫⁻ (x : α), ↑(↑g₂ x) ∂μ) < ⊤
hg₂ : L₂ < ∫⁻ (x : α), ↑(↑g₂ x) ∂μ
⊢ (∫⁻ (x : α), ↑(↑(g₁ + g₂) x) ∂μ) ≤ (∫⁻ (x : α), ↑(↑g₁ x) ∂μ) + ∫⁻ (x : α), ↑(↑g₂ x) ∂μ
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝¹ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hL✝ : L < (∫⁻ (x : α), ↑(↑f₁ x) ∂μ) + ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hf₁ : ¬(∫⁻ (x : α), ↑(↑f₁ x) ∂μ) = 0
hf₂ : ¬(∫⁻ (x : α), ↑(↑f₂ x) ∂μ) = 0
L₁ L₂ : ℝ≥0∞
hL₁ : L₁ < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ
hL₂ : L₂ < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hL : L < L₁ + L₂
g₁ : α →ₛ ℝ≥0
g₁_le : ∀ (x : α), ↑g₁ x ≤ ↑f₁ x
g₁_top : (∫⁻ (x : α), ↑(↑g₁ x) ∂μ) < ⊤
hg₁ : L₁ < ∫⁻ (x : α), ↑(↑g₁ x) ∂μ
g₂ : α →ₛ ℝ≥0
g₂_le : ∀ (x : α), ↑g₂ x ≤ ↑f₂ x
g₂_top : (∫⁻ (x : α), ↑(↑g₂ x) ∂μ) < ⊤
hg₂ : L₂ < ∫⁻ (x : α), ↑(↑g₂ x) ∂μ
⊢ (∫⁻ (x : α), ↑(↑(g₁ + g₂) x) ∂μ) < ⊤
apply lt_of_le_of_lt _ (add_lt_top.2 ⟨g₁_top, g₂_top⟩)
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝¹ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hL✝ : L < (∫⁻ (x : α), ↑(↑f₁ x) ∂μ) + ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hf₁ : ¬(∫⁻ (x : α), ↑(↑f₁ x) ∂μ) = 0
hf₂ : ¬(∫⁻ (x : α), ↑(↑f₂ x) ∂μ) = 0
L₁ L₂ : ℝ≥0∞
hL₁ : L₁ < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ
hL₂ : L₂ < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hL : L < L₁ + L₂
g₁ : α →ₛ ℝ≥0
g₁_le : ∀ (x : α), ↑g₁ x ≤ ↑f₁ x
g₁_top : (∫⁻ (x : α), ↑(↑g₁ x) ∂μ) < ⊤
hg₁ : L₁ < ∫⁻ (x : α), ↑(↑g₁ x) ∂μ
g₂ : α →ₛ ℝ≥0
g₂_le : ∀ (x : α), ↑g₂ x ≤ ↑f₂ x
g₂_top : (∫⁻ (x : α), ↑(↑g₂ x) ∂μ) < ⊤
hg₂ : L₂ < ∫⁻ (x : α), ↑(↑g₂ x) ∂μ
⊢ (∫⁻ (x : α), ↑(↑(g₁ + g₂) x) ∂μ) ≤ ∫⁻ (a : α), ↑(↑g₁ a) + ↑(↑g₂ a) ∂μ
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝¹ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hL✝ : L < (∫⁻ (x : α), ↑(↑f₁ x) ∂μ) + ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hf₁ : ¬(∫⁻ (x : α), ↑(↑f₁ x) ∂μ) = 0
hf₂ : ¬(∫⁻ (x : α), ↑(↑f₂ x) ∂μ) = 0
L₁ L₂ : ℝ≥0∞
hL₁ : L₁ < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ
hL₂ : L₂ < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hL : L < L₁ + L₂
g₁ : α →ₛ ℝ≥0
g₁_le : ∀ (x : α), ↑g₁ x ≤ ↑f₁ x
g₁_top : (∫⁻ (x : α), ↑(↑g₁ x) ∂μ) < ⊤
hg₁ : L₁ < ∫⁻ (x : α), ↑(↑g₁ x) ∂μ
g₂ : α →ₛ ℝ≥0
g₂_le : ∀ (x : α), ↑g₂ x ≤ ↑f₂ x
g₂_top : (∫⁻ (x : α), ↑(↑g₂ x) ∂μ) < ⊤
hg₂ : L₂ < ∫⁻ (x : α), ↑(↑g₂ x) ∂μ
⊢ (∫⁻ (x : α), ↑(↑(g₁ + g₂) x) ∂μ) ≤ (∫⁻ (x : α), ↑(↑g₁ x) ∂μ) + ∫⁻ (x : α), ↑(↑g₂ x) ∂μ
rw [← lintegral_add_left g₁.measurable.coe_nnreal_ennreal]
no goals
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝¹ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hL✝ : L < (∫⁻ (x : α), ↑(↑f₁ x) ∂μ) + ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hf₁ : ¬(∫⁻ (x : α), ↑(↑f₁ x) ∂μ) = 0
hf₂ : ¬(∫⁻ (x : α), ↑(↑f₂ x) ∂μ) = 0
L₁ L₂ : ℝ≥0∞
hL₁ : L₁ < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ
hL₂ : L₂ < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hL : L < L₁ + L₂
g₁ : α →ₛ ℝ≥0
g₁_le : ∀ (x : α), ↑g₁ x ≤ ↑f₁ x
g₁_top : (∫⁻ (x : α), ↑(↑g₁ x) ∂μ) < ⊤
hg₁ : L₁ < ∫⁻ (x : α), ↑(↑g₁ x) ∂μ
g₂ : α →ₛ ℝ≥0
g₂_le : ∀ (x : α), ↑g₂ x ≤ ↑f₂ x
g₂_top : (∫⁻ (x : α), ↑(↑g₂ x) ∂μ) < ⊤
hg₂ : L₂ < ∫⁻ (x : α), ↑(↑g₂ x) ∂μ
⊢ (∫⁻ (x : α), ↑(↑(g₁ + g₂) x) ∂μ) ≤ ∫⁻ (a : α), ↑(↑g₁ a) + ↑(↑g₂ a) ∂μ
exact le_rfl
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝¹ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hL✝ : L < (∫⁻ (x : α), ↑(↑f₁ x) ∂μ) + ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hf₁ : ¬(∫⁻ (x : α), ↑(↑f₁ x) ∂μ) = 0
hf₂ : ¬(∫⁻ (x : α), ↑(↑f₂ x) ∂μ) = 0
L₁ L₂ : ℝ≥0∞
hL₁ : L₁ < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ
hL₂ : L₂ < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hL : L < L₁ + L₂
g₁ : α →ₛ ℝ≥0
g₁_le : ∀ (x : α), ↑g₁ x ≤ ↑f₁ x
g₁_top : (∫⁻ (x : α), ↑(↑g₁ x) ∂μ) < ⊤
hg₁ : L₁ < ∫⁻ (x : α), ↑(↑g₁ x) ∂μ
g₂ : α →ₛ ℝ≥0
g₂_le : ∀ (x : α), ↑g₂ x ≤ ↑f₂ x
g₂_top : (∫⁻ (x : α), ↑(↑g₂ x) ∂μ) < ⊤
hg₂ : L₂ < ∫⁻ (x : α), ↑(↑g₂ x) ∂μ
⊢ ((∫⁻ (x : α), ↑(↑g₁ x) ∂μ) + ∫⁻ (x : α), ↑(↑g₂ x) ∂μ) ≤ ∫⁻ (x : α), ↑(↑(g₁ + g₂) x) ∂μ
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝¹ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hL✝ : L < (∫⁻ (x : α), ↑(↑f₁ x) ∂μ) + ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hf₁ : ¬(∫⁻ (x : α), ↑(↑f₁ x) ∂μ) = 0
hf₂ : ¬(∫⁻ (x : α), ↑(↑f₂ x) ∂μ) = 0
L₁ L₂ : ℝ≥0∞
hL₁ : L₁ < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ
hL₂ : L₂ < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hL : L < L₁ + L₂
g₁ : α →ₛ ℝ≥0
g₁_le : ∀ (x : α), ↑g₁ x ≤ ↑f₁ x
g₁_top : (∫⁻ (x : α), ↑(↑g₁ x) ∂μ) < ⊤
hg₁ : L₁ < ∫⁻ (x : α), ↑(↑g₁ x) ∂μ
g₂ : α →ₛ ℝ≥0
g₂_le : ∀ (x : α), ↑g₂ x ≤ ↑f₂ x
g₂_top : (∫⁻ (x : α), ↑(↑g₂ x) ∂μ) < ⊤
hg₂ : L₂ < ∫⁻ (x : α), ↑(↑g₂ x) ∂μ
⊢ L < ∫⁻ (x : α), ↑(↑(g₁ + g₂) x) ∂μ
apply hL.trans ((ENNReal.add_lt_add hg₁ hg₂).trans_le _)
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝¹ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hL✝ : L < (∫⁻ (x : α), ↑(↑f₁ x) ∂μ) + ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hf₁ : ¬(∫⁻ (x : α), ↑(↑f₁ x) ∂μ) = 0
hf₂ : ¬(∫⁻ (x : α), ↑(↑f₂ x) ∂μ) = 0
L₁ L₂ : ℝ≥0∞
hL₁ : L₁ < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ
hL₂ : L₂ < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hL : L < L₁ + L₂
g₁ : α →ₛ ℝ≥0
g₁_le : ∀ (x : α), ↑g₁ x ≤ ↑f₁ x
g₁_top : (∫⁻ (x : α), ↑(↑g₁ x) ∂μ) < ⊤
hg₁ : L₁ < ∫⁻ (x : α), ↑(↑g₁ x) ∂μ
g₂ : α →ₛ ℝ≥0
g₂_le : ∀ (x : α), ↑g₂ x ≤ ↑f₂ x
g₂_top : (∫⁻ (x : α), ↑(↑g₂ x) ∂μ) < ⊤
hg₂ : L₂ < ∫⁻ (x : α), ↑(↑g₂ x) ∂μ
⊢ (∫⁻ (a : α), ↑(↑g₁ a) + ↑(↑g₂ a) ∂μ) ≤ ∫⁻ (x : α), ↑(↑(g₁ + g₂) x) ∂μ
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝¹ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hL✝ : L < (∫⁻ (x : α), ↑(↑f₁ x) ∂μ) + ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hf₁ : ¬(∫⁻ (x : α), ↑(↑f₁ x) ∂μ) = 0
hf₂ : ¬(∫⁻ (x : α), ↑(↑f₂ x) ∂μ) = 0
L₁ L₂ : ℝ≥0∞
hL₁ : L₁ < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ
hL₂ : L₂ < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hL : L < L₁ + L₂
g₁ : α →ₛ ℝ≥0
g₁_le : ∀ (x : α), ↑g₁ x ≤ ↑f₁ x
g₁_top : (∫⁻ (x : α), ↑(↑g₁ x) ∂μ) < ⊤
hg₁ : L₁ < ∫⁻ (x : α), ↑(↑g₁ x) ∂μ
g₂ : α →ₛ ℝ≥0
g₂_le : ∀ (x : α), ↑g₂ x ≤ ↑f₂ x
g₂_top : (∫⁻ (x : α), ↑(↑g₂ x) ∂μ) < ⊤
hg₂ : L₂ < ∫⁻ (x : α), ↑(↑g₂ x) ∂μ
⊢ ((∫⁻ (x : α), ↑(↑g₁ x) ∂μ) + ∫⁻ (x : α), ↑(↑g₂ x) ∂μ) ≤ ∫⁻ (x : α), ↑(↑(g₁ + g₂) x) ∂μ
rw [← lintegral_add_left g₁.measurable.coe_nnreal_ennreal]
no goals
α : Type u_1
β : Type ?u.1832831
γ : Type ?u.1832834
δ : Type ?u.1832837
m✝ m0 : MeasurableSpace α
E : Type ?u.1832846
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L✝ : ℝ≥0∞
hL✝¹ : L✝ < ∫⁻ (x : α), ↑(↑f x) ∂μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ↑f₁) (support ↑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    (L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ) →
      ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
L : ℝ≥0∞
hL✝ : L < (∫⁻ (x : α), ↑(↑f₁ x) ∂μ) + ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hf₁ : ¬(∫⁻ (x : α), ↑(↑f₁ x) ∂μ) = 0
hf₂ : ¬(∫⁻ (x : α), ↑(↑f₂ x) ∂μ) = 0
L₁ L₂ : ℝ≥0∞
hL₁ : L₁ < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ
hL₂ : L₂ < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ
hL : L < L₁ + L₂
g₁ : α →ₛ ℝ≥0
g₁_le : ∀ (x : α), ↑g₁ x ≤ ↑f₁ x
g₁_top : (∫⁻ (x : α), ↑(↑g₁ x) ∂μ) < ⊤
hg₁ : L₁ < ∫⁻ (x : α), ↑(↑g₁ x) ∂μ
g₂ : α →ₛ ℝ≥0
g₂_le : ∀ (x : α), ↑g₂ x ≤ ↑f₂ x
g₂_top : (∫⁻ (x : α), ↑(↑g₂ x) ∂μ) < ⊤
hg₂ : L₂ < ∫⁻ (x : α), ↑(↑g₂ x) ∂μ
⊢ (∫⁻ (a : α), ↑(↑g₁ a) + ↑(↑g₂ a) ∂μ) ≤ ∫⁻ (x : α), ↑(↑(g₁ + g₂) x) ∂μ
exact le_rfl