α : Type u_1
β : Type ?u.918859
γ : Type ?u.918862
δ : Type ?u.918865
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f✝ : α →ₛ β
f : α →ₛ ℝ≥0∞
hm : SimpleFunc.FinMeasSupp f μ
hf : ∀ᵐ (a : α) ∂μ, ↑f a ≠ ⊤
a : ℝ≥0∞
ha : a ∈ SimpleFunc.range f
⊢ a * ↑↑μ (↑f ⁻¹' {a}) ≠ ⊤
α : Type u_1
β : Type ?u.918859
γ : Type ?u.918862
δ : Type ?u.918865
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f✝ : α →ₛ β
f : α →ₛ ℝ≥0∞
hm : SimpleFunc.FinMeasSupp f μ
hf : ∀ᵐ (a : α) ∂μ, ↑f a ≠ ⊤
⊢ lintegral f μ < ⊤
refine' sum_lt_top fun a ha => _
case inl
α : Type u_1
β : Type ?u.918859
γ : Type ?u.918862
δ : Type ?u.918865
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f✝ : α →ₛ β
f : α →ₛ ℝ≥0∞
hm : SimpleFunc.FinMeasSupp f μ
hf : ∀ᵐ (a : α) ∂μ, ↑f a ≠ ⊤
ha : ⊤ ∈ SimpleFunc.range f
⊢ ⊤ * ↑↑μ (↑f ⁻¹' {⊤}) ≠ ⊤

case inr
α : Type u_1
β : Type ?u.918859
γ : Type ?u.918862
δ : Type ?u.918865
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f✝ : α →ₛ β
f : α →ₛ ℝ≥0∞
hm : SimpleFunc.FinMeasSupp f μ
hf : ∀ᵐ (a : α) ∂μ, ↑f a ≠ ⊤
a : ℝ≥0∞
ha✝ : a ∈ SimpleFunc.range f
ha : a ≠ ⊤
⊢ a * ↑↑μ (↑f ⁻¹' {a}) ≠ ⊤
α : Type u_1
β : Type ?u.918859
γ : Type ?u.918862
δ : Type ?u.918865
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f✝ : α →ₛ β
f : α →ₛ ℝ≥0∞
hm : SimpleFunc.FinMeasSupp f μ
hf : ∀ᵐ (a : α) ∂μ, ↑f a ≠ ⊤
a : ℝ≥0∞
ha : a ∈ SimpleFunc.range f
⊢ a * ↑↑μ (↑f ⁻¹' {a}) ≠ ⊤
rcases eq_or_ne a ∞ with (rfl | ha)
case inl
α : Type u_1
β : Type ?u.918859
γ : Type ?u.918862
δ : Type ?u.918865
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f✝ : α →ₛ β
f : α →ₛ ℝ≥0∞
hm : SimpleFunc.FinMeasSupp f μ
ha : ⊤ ∈ SimpleFunc.range f
hf : ↑↑μ {a | ↑f a = ⊤} = 0
⊢ ⊤ * ↑↑μ (↑f ⁻¹' {⊤}) ≠ ⊤
case inl
α : Type u_1
β : Type ?u.918859
γ : Type ?u.918862
δ : Type ?u.918865
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f✝ : α →ₛ β
f : α →ₛ ℝ≥0∞
hm : SimpleFunc.FinMeasSupp f μ
hf : ∀ᵐ (a : α) ∂μ, ↑f a ≠ ⊤
ha : ⊤ ∈ SimpleFunc.range f
⊢ ⊤ * ↑↑μ (↑f ⁻¹' {⊤}) ≠ ⊤
simp only [ae_iff, Ne.def, Classical.not_not] at hf
no goals
case inl
α : Type u_1
β : Type ?u.918859
γ : Type ?u.918862
δ : Type ?u.918865
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f✝ : α →ₛ β
f : α →ₛ ℝ≥0∞
hm : SimpleFunc.FinMeasSupp f μ
ha : ⊤ ∈ SimpleFunc.range f
hf : ↑↑μ {a | ↑f a = ⊤} = 0
⊢ ⊤ * ↑↑μ (↑f ⁻¹' {⊤}) ≠ ⊤
simp [Set.preimage, hf]
case pos
α : Type u_1
β : Type ?u.918859
γ : Type ?u.918862
δ : Type ?u.918865
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f✝ : α →ₛ β
f : α →ₛ ℝ≥0∞
hm : SimpleFunc.FinMeasSupp f μ
hf : ∀ᵐ (a : α) ∂μ, ↑f a ≠ ⊤
a : ℝ≥0∞
ha✝ : a ∈ SimpleFunc.range f
ha : a ≠ ⊤
ha0 : a = 0
⊢ a * ↑↑μ (↑f ⁻¹' {a}) ≠ ⊤

case neg
α : Type u_1
β : Type ?u.918859
γ : Type ?u.918862
δ : Type ?u.918865
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f✝ : α →ₛ β
f : α →ₛ ℝ≥0∞
hm : SimpleFunc.FinMeasSupp f μ
hf : ∀ᵐ (a : α) ∂μ, ↑f a ≠ ⊤
a : ℝ≥0∞
ha✝ : a ∈ SimpleFunc.range f
ha : a ≠ ⊤
ha0 : ¬a = 0
⊢ a * ↑↑μ (↑f ⁻¹' {a}) ≠ ⊤
case inr
α : Type u_1
β : Type ?u.918859
γ : Type ?u.918862
δ : Type ?u.918865
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f✝ : α →ₛ β
f : α →ₛ ℝ≥0∞
hm : SimpleFunc.FinMeasSupp f μ
hf : ∀ᵐ (a : α) ∂μ, ↑f a ≠ ⊤
a : ℝ≥0∞
ha✝ : a ∈ SimpleFunc.range f
ha : a ≠ ⊤
⊢ a * ↑↑μ (↑f ⁻¹' {a}) ≠ ⊤
by_cases ha0 : a = 0
case pos
α : Type u_1
β : Type ?u.918859
γ : Type ?u.918862
δ : Type ?u.918865
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f✝ : α →ₛ β
f : α →ₛ ℝ≥0∞
hm : SimpleFunc.FinMeasSupp f μ
hf : ∀ᵐ (a : α) ∂μ, ↑f a ≠ ⊤
ha✝ : 0 ∈ SimpleFunc.range f
ha : 0 ≠ ⊤
⊢ 0 * ↑↑μ (↑f ⁻¹' {0}) ≠ ⊤
case pos
α : Type u_1
β : Type ?u.918859
γ : Type ?u.918862
δ : Type ?u.918865
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f✝ : α →ₛ β
f : α →ₛ ℝ≥0∞
hm : SimpleFunc.FinMeasSupp f μ
hf : ∀ᵐ (a : α) ∂μ, ↑f a ≠ ⊤
a : ℝ≥0∞
ha✝ : a ∈ SimpleFunc.range f
ha : a ≠ ⊤
ha0 : a = 0
⊢ a * ↑↑μ (↑f ⁻¹' {a}) ≠ ⊤
subst a
no goals
case pos
α : Type u_1
β : Type ?u.918859
γ : Type ?u.918862
δ : Type ?u.918865
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f✝ : α →ₛ β
f : α →ₛ ℝ≥0∞
hm : SimpleFunc.FinMeasSupp f μ
hf : ∀ᵐ (a : α) ∂μ, ↑f a ≠ ⊤
ha✝ : 0 ∈ SimpleFunc.range f
ha : 0 ≠ ⊤
⊢ 0 * ↑↑μ (↑f ⁻¹' {0}) ≠ ⊤
rwa [MulZeroClass.zero_mul]
no goals
case neg
α : Type u_1
β : Type ?u.918859
γ : Type ?u.918862
δ : Type ?u.918865
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f✝ : α →ₛ β
f : α →ₛ ℝ≥0∞
hm : SimpleFunc.FinMeasSupp f μ
hf : ∀ᵐ (a : α) ∂μ, ↑f a ≠ ⊤
a : ℝ≥0∞
ha✝ : a ∈ SimpleFunc.range f
ha : a ≠ ⊤
ha0 : ¬a = 0
⊢ a * ↑↑μ (↑f ⁻¹' {a}) ≠ ⊤
exact mul_ne_top ha (finMeasSupp_iff.1 hm _ ha0).ne