case intro
α✝ : Type ?u.1753837
β : Type ?u.1753840
γ : Type ?u.1753843
δ : Type ?u.1753846
m : MeasurableSpace α✝
μ✝ ν : Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
μ_fin : IsFiniteMeasure μ
f : α → ℝ≥0∞
c : ℝ≥0
hc : ∀ (x : α), f x ≤ ↑c
⊢ (∫⁻ (x : α), f x ∂μ) < ⊤
α✝ : Type ?u.1753837
β : Type ?u.1753840
γ : Type ?u.1753843
δ : Type ?u.1753846
m : MeasurableSpace α✝
μ✝ ν : Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
μ_fin : IsFiniteMeasure μ
f : α → ℝ≥0∞
f_bdd : ∃ c, ∀ (x : α), f x ≤ ↑c
⊢ (∫⁻ (x : α), f x ∂μ) < ⊤
cases' f_bdd with c hc
case intro
α✝ : Type ?u.1753837
β : Type ?u.1753840
γ : Type ?u.1753843
δ : Type ?u.1753846
m : MeasurableSpace α✝
μ✝ ν : Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
μ_fin : IsFiniteMeasure μ
f : α → ℝ≥0∞
c : ℝ≥0
hc : ∀ (x : α), f x ≤ ↑c
⊢ (∫⁻ (a : α), ↑c ∂μ) < ⊤
case intro
α✝ : Type ?u.1753837
β : Type ?u.1753840
γ : Type ?u.1753843
δ : Type ?u.1753846
m : MeasurableSpace α✝
μ✝ ν : Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
μ_fin : IsFiniteMeasure μ
f : α → ℝ≥0∞
c : ℝ≥0
hc : ∀ (x : α), f x ≤ ↑c
⊢ (∫⁻ (x : α), f x ∂μ) < ⊤
apply lt_of_le_of_lt (@lintegral_mono _ _ μ _ _ hc)
case intro
α✝ : Type ?u.1753837
β : Type ?u.1753840
γ : Type ?u.1753843
δ : Type ?u.1753846
m : MeasurableSpace α✝
μ✝ ν : Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
μ_fin : IsFiniteMeasure μ
f : α → ℝ≥0∞
c : ℝ≥0
hc : ∀ (x : α), f x ≤ ↑c
⊢ ↑c * ↑↑μ univ < ⊤
case intro
α✝ : Type ?u.1753837
β : Type ?u.1753840
γ : Type ?u.1753843
δ : Type ?u.1753846
m : MeasurableSpace α✝
μ✝ ν : Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
μ_fin : IsFiniteMeasure μ
f : α → ℝ≥0∞
c : ℝ≥0
hc : ∀ (x : α), f x ≤ ↑c
⊢ (∫⁻ (a : α), ↑c ∂μ) < ⊤
rw [lintegral_const]
no goals
case intro
α✝ : Type ?u.1753837
β : Type ?u.1753840
γ : Type ?u.1753843
δ : Type ?u.1753846
m : MeasurableSpace α✝
μ✝ ν : Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
μ_fin : IsFiniteMeasure μ
f : α → ℝ≥0∞
c : ℝ≥0
hc : ∀ (x : α), f x ≤ ↑c
⊢ ↑c * ↑↑μ univ < ⊤
exact ENNReal.mul_lt_top ENNReal.coe_lt_top.ne μ_fin.measure_univ_lt_top.ne