α : Type u_1
β : Type ?u.921719
γ : Type ?u.921722
δ : Type ?u.921725
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f✝ : α →ₛ β
f : α →ₛ ℝ≥0∞
h : lintegral f μ ≠ ⊤
b : ℝ≥0∞
hb : b ≠ 0
⊢ ↑↑μ (↑f ⁻¹' {b}) < ⊤
α : Type u_1
β : Type ?u.921719
γ : Type ?u.921722
δ : Type ?u.921725
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f✝ : α →ₛ β
f : α →ₛ ℝ≥0∞
h : lintegral f μ ≠ ⊤
⊢ SimpleFunc.FinMeasSupp f μ
refine' finMeasSupp_iff.2 fun b hb => _
α : Type u_1
β : Type ?u.921719
γ : Type ?u.921722
δ : Type ?u.921725
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f✝ : α →ₛ β
f : α →ₛ ℝ≥0∞
b : ℝ≥0∞
h : ∑ x in insert b (SimpleFunc.range f \ {0}), x * ↑↑μ (↑f ⁻¹' {x}) ≠ ⊤
hb : b ≠ 0
⊢ ↑↑μ (↑f ⁻¹' {b}) < ⊤
α : Type u_1
β : Type ?u.921719
γ : Type ?u.921722
δ : Type ?u.921725
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f✝ : α →ₛ β
f : α →ₛ ℝ≥0∞
h : lintegral f μ ≠ ⊤
b : ℝ≥0∞
hb : b ≠ 0
⊢ ↑↑μ (↑f ⁻¹' {b}) < ⊤
rw [f.lintegral_eq_of_subset' (Finset.subset_insert b _)] at h
α : Type u_1
β : Type ?u.921719
γ : Type ?u.921722
δ : Type ?u.921725
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f✝ : α →ₛ β
f : α →ₛ ℝ≥0∞
b : ℝ≥0∞
h : ∑ x in insert b (SimpleFunc.range f \ {0}), x * ↑↑μ (↑f ⁻¹' {x}) ≠ ⊤
hb : b ≠ 0
⊢ b * ↑↑μ (↑f ⁻¹' {b}) ≠ ⊤
α : Type u_1
β : Type ?u.921719
γ : Type ?u.921722
δ : Type ?u.921725
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f✝ : α →ₛ β
f : α →ₛ ℝ≥0∞
b : ℝ≥0∞
h : ∑ x in insert b (SimpleFunc.range f \ {0}), x * ↑↑μ (↑f ⁻¹' {x}) ≠ ⊤
hb : b ≠ 0
⊢ ↑↑μ (↑f ⁻¹' {b}) < ⊤
refine' ENNReal.lt_top_of_mul_ne_top_right _ hb
no goals
α : Type u_1
β : Type ?u.921719
γ : Type ?u.921722
δ : Type ?u.921725
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f✝ : α →ₛ β
f : α →ₛ ℝ≥0∞
b : ℝ≥0∞
h : ∑ x in insert b (SimpleFunc.range f \ {0}), x * ↑↑μ (↑f ⁻¹' {x}) ≠ ⊤
hb : b ≠ 0
⊢ b * ↑↑μ (↑f ⁻¹' {b}) ≠ ⊤
exact (lt_top_of_sum_ne_top h (Finset.mem_insert_self _ _)).ne