α : Type u_1
β : Type ?u.1845716
γ : Type ?u.1845719
δ : Type ?u.1845722
m✝ m0 : MeasurableSpace α
E : Type ?u.1845731
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
hL : ∃ i i_1, L < SimpleFunc.lintegral (SimpleFunc.map ENNReal.some i) μ
⊢ ∃ g, (∀ (x : α), ↑g x ≤ f x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
α : Type u_1
β : Type ?u.1845716
γ : Type ?u.1845719
δ : Type ?u.1845722
m✝ m0 : MeasurableSpace α
E : Type ?u.1845731
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) ∂μ
simp_rw [lintegral_eq_nnreal, lt_iSup_iff] at hL
case intro.intro
α : Type u_1
β : Type ?u.1845716
γ : Type ?u.1845719
δ : Type ?u.1845722
m✝ m0 : MeasurableSpace α
E : Type ?u.1845731
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
g₀ : α →ₛ ℝ≥0
hg₀ : ∀ (x : α), ↑(↑g₀ x) ≤ ↑(f x)
g₀L : L < SimpleFunc.lintegral (SimpleFunc.map ENNReal.some g₀) μ
⊢ ∃ g, (∀ (x : α), ↑g x ≤ f x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
α : Type u_1
β : Type ?u.1845716
γ : Type ?u.1845719
δ : Type ?u.1845722
m✝ m0 : MeasurableSpace α
E : Type ?u.1845731
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
hL : ∃ i i_1, L < SimpleFunc.lintegral (SimpleFunc.map ENNReal.some i) μ
⊢ ∃ g, (∀ (x : α), ↑g x ≤ f x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
rcases hL with ⟨g₀, hg₀, g₀L⟩
case intro.intro
α : Type u_1
β : Type ?u.1845716
γ : Type ?u.1845719
δ : Type ?u.1845722
m✝ m0 : MeasurableSpace α
E : Type ?u.1845731
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
g₀ : α →ₛ ℝ≥0
hg₀ : ∀ (x : α), ↑(↑g₀ x) ≤ ↑(f x)
g₀L : L < SimpleFunc.lintegral (SimpleFunc.map ENNReal.some g₀) μ
h'L : L < ∫⁻ (x : α), ↑(↑g₀ x) ∂μ
⊢ ∃ g, (∀ (x : α), ↑g x ≤ f x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
case intro.intro
α : Type u_1
β : Type ?u.1845716
γ : Type ?u.1845719
δ : Type ?u.1845722
m✝ m0 : MeasurableSpace α
E : Type ?u.1845731
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
g₀ : α →ₛ ℝ≥0
hg₀ : ∀ (x : α), ↑(↑g₀ x) ≤ ↑(f x)
g₀L : L < SimpleFunc.lintegral (SimpleFunc.map ENNReal.some g₀) μ
⊢ ∃ g, (∀ (x : α), ↑g x ≤ f x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
have h'L : L < ∫⁻ x, g₀ x ∂μ := by
  convert g₀L
  rw [← SimpleFunc.lintegral_eq_lintegral]
  rfl
case intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.1845716
γ : Type ?u.1845719
δ : Type ?u.1845722
m✝ m0 : MeasurableSpace α
E : Type ?u.1845731
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
g₀ : α →ₛ ℝ≥0
hg₀ : ∀ (x : α), ↑(↑g₀ x) ≤ ↑(f x)
g₀L : L < SimpleFunc.lintegral (SimpleFunc.map ENNReal.some g₀) μ
h'L : L < ∫⁻ (x : α), ↑(↑g₀ x) ∂μ
g : α →ₛ ℝ≥0
hg : ∀ (x : α), ↑g x ≤ ↑g₀ x
gL : (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤
gtop : L < ∫⁻ (x : α), ↑(↑g x) ∂μ
⊢ ∃ g, (∀ (x : α), ↑g x ≤ f x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
case intro.intro
α : Type u_1
β : Type ?u.1845716
γ : Type ?u.1845719
δ : Type ?u.1845722
m✝ m0 : MeasurableSpace α
E : Type ?u.1845731
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
g₀ : α →ₛ ℝ≥0
hg₀ : ∀ (x : α), ↑(↑g₀ x) ≤ ↑(f x)
g₀L : L < SimpleFunc.lintegral (SimpleFunc.map ENNReal.some g₀) μ
h'L : L < ∫⁻ (x : α), ↑(↑g₀ x) ∂μ
⊢ ∃ g, (∀ (x : α), ↑g x ≤ f x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
rcases SimpleFunc.exists_lt_lintegral_simpleFunc_of_lt_lintegral h'L with ⟨g, hg, gL, gtop⟩
no goals
case intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.1845716
γ : Type ?u.1845719
δ : Type ?u.1845722
m✝ m0 : MeasurableSpace α
E : Type ?u.1845731
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
g₀ : α →ₛ ℝ≥0
hg₀ : ∀ (x : α), ↑(↑g₀ x) ≤ ↑(f x)
g₀L : L < SimpleFunc.lintegral (SimpleFunc.map ENNReal.some g₀) μ
h'L : L < ∫⁻ (x : α), ↑(↑g₀ x) ∂μ
g : α →ₛ ℝ≥0
hg : ∀ (x : α), ↑g x ≤ ↑g₀ x
gL : (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤
gtop : L < ∫⁻ (x : α), ↑(↑g x) ∂μ
⊢ ∃ g, (∀ (x : α), ↑g x ≤ f x) ∧ (∫⁻ (x : α), ↑(↑g x) ∂μ) < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
exact ⟨g, fun x => (hg x).trans (coe_le_coe.1 (hg₀ x)), gL, gtop⟩
case h.e'_4
α : Type u_1
β : Type ?u.1845716
γ : Type ?u.1845719
δ : Type ?u.1845722
m✝ m0 : MeasurableSpace α
E : Type ?u.1845731
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
g₀ : α →ₛ ℝ≥0
hg₀ : ∀ (x : α), ↑(↑g₀ x) ≤ ↑(f x)
g₀L : L < SimpleFunc.lintegral (SimpleFunc.map ENNReal.some g₀) μ
⊢ (∫⁻ (x : α), ↑(↑g₀ x) ∂μ) = SimpleFunc.lintegral (SimpleFunc.map ENNReal.some g₀) μ
α : Type u_1
β : Type ?u.1845716
γ : Type ?u.1845719
δ : Type ?u.1845722
m✝ m0 : MeasurableSpace α
E : Type ?u.1845731
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
g₀ : α →ₛ ℝ≥0
hg₀ : ∀ (x : α), ↑(↑g₀ x) ≤ ↑(f x)
g₀L : L < SimpleFunc.lintegral (SimpleFunc.map ENNReal.some g₀) μ
⊢ L < ∫⁻ (x : α), ↑(↑g₀ x) ∂μ
convert g₀L
case h.e'_4
α : Type u_1
β : Type ?u.1845716
γ : Type ?u.1845719
δ : Type ?u.1845722
m✝ m0 : MeasurableSpace α
E : Type ?u.1845731
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
g₀ : α →ₛ ℝ≥0
hg₀ : ∀ (x : α), ↑(↑g₀ x) ≤ ↑(f x)
g₀L : L < SimpleFunc.lintegral (SimpleFunc.map ENNReal.some g₀) μ
⊢ (∫⁻ (x : α), ↑(↑g₀ x) ∂μ) = ∫⁻ (a : α), ↑(SimpleFunc.map ENNReal.some g₀) a ∂μ
case h.e'_4
α : Type u_1
β : Type ?u.1845716
γ : Type ?u.1845719
δ : Type ?u.1845722
m✝ m0 : MeasurableSpace α
E : Type ?u.1845731
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
g₀ : α →ₛ ℝ≥0
hg₀ : ∀ (x : α), ↑(↑g₀ x) ≤ ↑(f x)
g₀L : L < SimpleFunc.lintegral (SimpleFunc.map ENNReal.some g₀) μ
⊢ (∫⁻ (x : α), ↑(↑g₀ x) ∂μ) = SimpleFunc.lintegral (SimpleFunc.map ENNReal.some g₀) μ
rw [← SimpleFunc.lintegral_eq_lintegral]
no goals
case h.e'_4
α : Type u_1
β : Type ?u.1845716
γ : Type ?u.1845719
δ : Type ?u.1845722
m✝ m0 : MeasurableSpace α
E : Type ?u.1845731
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
g₀ : α →ₛ ℝ≥0
hg₀ : ∀ (x : α), ↑(↑g₀ x) ≤ ↑(f x)
g₀L : L < SimpleFunc.lintegral (SimpleFunc.map ENNReal.some g₀) μ
⊢ (∫⁻ (x : α), ↑(↑g₀ x) ∂μ) = ∫⁻ (a : α), ↑(SimpleFunc.map ENNReal.some g₀) a ∂μ
rfl