-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem lintegral_lt_top {f : α →ₛ ℝ≥0∞} (hm : f.FinMeasSupp μ) (hf : ∀ᵐ a ∂μ, f a ≠ ∞) :
    f.lintegral μ < ∞

Proof state:
case inl
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hm : f.FinMeasSupp μ
ha : ⊤ ∈ f.range
hf : μ {a | f a = ⊤} = 0
⊢ ⊤ * μ (⇑f ⁻¹' {⊤}) < ⊤

Tactic:
simp [Set.preimage, hf]

Result:
no goals

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hm : f.FinMeasSupp μ
hf : ∀ᵐ (a : α) ∂μ, f a ≠ ⊤
ha✝ : 0 ∈ f.range
ha : 0 ≠ ⊤
⊢ 0 * μ (⇑f ⁻¹' {0}) < ⊤

Tactic:
simp

Result:
no goals

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hm : f.FinMeasSupp μ
hf : ∀ᵐ (a : α) ∂μ, f a ≠ ⊤
a : ℝ≥0∞
ha✝ : a ∈ f.range
ha : a ≠ ⊤
ha0 : a = 0
⊢ a * μ (⇑f ⁻¹' {a}) < ⊤

Tactic:
subst a

Result:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hm : f.FinMeasSupp μ
hf : ∀ᵐ (a : α) ∂μ, f a ≠ ⊤
ha✝ : 0 ∈ f.range
ha : 0 ≠ ⊤
⊢ 0 * μ (⇑f ⁻¹' {0}) < ⊤

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hm : f.FinMeasSupp μ
hf : ∀ᵐ (a : α) ∂μ, f a ≠ ⊤
⊢ f.lintegral μ < ⊤

Tactic:
refine sum_lt_top.2 fun a ha => ?_

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hm : f.FinMeasSupp μ
hf : ∀ᵐ (a : α) ∂μ, f a ≠ ⊤
a : ℝ≥0∞
ha : a ∈ f.range
⊢ a * μ (⇑f ⁻¹' {a}) < ⊤

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hm : f.FinMeasSupp μ
hf : ∀ᵐ (a : α) ∂μ, f a ≠ ⊤
a : ℝ≥0∞
ha : a ∈ f.range
⊢ a * μ (⇑f ⁻¹' {a}) < ⊤

Tactic:
rcases eq_or_ne a ∞ with (rfl | ha)

Result:
case inl
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hm : f.FinMeasSupp μ
hf : ∀ᵐ (a : α) ∂μ, f a ≠ ⊤
ha : ⊤ ∈ f.range
⊢ ⊤ * μ (⇑f ⁻¹' {⊤}) < ⊤

case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hm : f.FinMeasSupp μ
hf : ∀ᵐ (a : α) ∂μ, f a ≠ ⊤
a : ℝ≥0∞
ha✝ : a ∈ f.range
ha : a ≠ ⊤
⊢ a * μ (⇑f ⁻¹' {a}) < ⊤

Proof state:
case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hm : f.FinMeasSupp μ
hf : ∀ᵐ (a : α) ∂μ, f a ≠ ⊤
a : ℝ≥0∞
ha✝ : a ∈ f.range
ha : a ≠ ⊤
⊢ a * μ (⇑f ⁻¹' {a}) < ⊤

Tactic:
by_cases ha0 : a = 0

Result:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hm : f.FinMeasSupp μ
hf : ∀ᵐ (a : α) ∂μ, f a ≠ ⊤
a : ℝ≥0∞
ha✝ : a ∈ f.range
ha : a ≠ ⊤
ha0 : a = 0
⊢ a * μ (⇑f ⁻¹' {a}) < ⊤

case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hm : f.FinMeasSupp μ
hf : ∀ᵐ (a : α) ∂μ, f a ≠ ⊤
a : ℝ≥0∞
ha✝ : a ∈ f.range
ha : a ≠ ⊤
ha0 : ¬a = 0
⊢ a * μ (⇑f ⁻¹' {a}) < ⊤

Proof state:
case inl
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hm : f.FinMeasSupp μ
hf : ∀ᵐ (a : α) ∂μ, f a ≠ ⊤
ha : ⊤ ∈ f.range
⊢ ⊤ * μ (⇑f ⁻¹' {⊤}) < ⊤

Tactic:
simp only [ae_iff, Ne, Classical.not_not] at hf

Result:
case inl
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hm : f.FinMeasSupp μ
ha : ⊤ ∈ f.range
hf : μ {a | f a = ⊤} = 0
⊢ ⊤ * μ (⇑f ⁻¹' {⊤}) < ⊤

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hm : f.FinMeasSupp μ
hf : ∀ᵐ (a : α) ∂μ, f a ≠ ⊤
a : ℝ≥0∞
ha✝ : a ∈ f.range
ha : a ≠ ⊤
ha0 : ¬a = 0
⊢ a * μ (⇑f ⁻¹' {a}) < ⊤

Tactic:
exact mul_lt_top ha.lt_top (finMeasSupp_iff.1 hm _ ha0)

Result:
no goals