α : Type u_1
β : Type ?u.889363
γ : Type ?u.889366
δ : Type ?u.889369
m : MeasurableSpace α
μ ν : Measure α
c : ℝ≥0∞
⊢ ∑ x in SimpleFunc.range (const α c), x * ↑↑μ (↑(const α c) ⁻¹' {x}) = c * ↑↑μ univ
α : Type u_1
β : Type ?u.889363
γ : Type ?u.889366
δ : Type ?u.889369
m : MeasurableSpace α
μ ν : Measure α
c : ℝ≥0∞
⊢ lintegral (const α c) μ = c * ↑↑μ univ
rw [lintegral]
case inl
α : Type u_1
β : Type ?u.889363
γ : Type ?u.889366
δ : Type ?u.889369
m : MeasurableSpace α
μ ν : Measure α
c : ℝ≥0∞
h✝ : IsEmpty α
⊢ ∑ x in SimpleFunc.range (const α c), x * ↑↑μ (↑(const α c) ⁻¹' {x}) = c * ↑↑μ univ

case inr
α : Type u_1
β : Type ?u.889363
γ : Type ?u.889366
δ : Type ?u.889369
m : MeasurableSpace α
μ ν : Measure α
c : ℝ≥0∞
h✝ : Nonempty α
⊢ ∑ x in SimpleFunc.range (const α c), x * ↑↑μ (↑(const α c) ⁻¹' {x}) = c * ↑↑μ univ
α : Type u_1
β : Type ?u.889363
γ : Type ?u.889366
δ : Type ?u.889369
m : MeasurableSpace α
μ ν : Measure α
c : ℝ≥0∞
⊢ ∑ x in SimpleFunc.range (const α c), x * ↑↑μ (↑(const α c) ⁻¹' {x}) = c * ↑↑μ univ
cases isEmpty_or_nonempty α
no goals
case inl
α : Type u_1
β : Type ?u.889363
γ : Type ?u.889366
δ : Type ?u.889369
m : MeasurableSpace α
μ ν : Measure α
c : ℝ≥0∞
h✝ : IsEmpty α
⊢ ∑ x in SimpleFunc.range (const α c), x * ↑↑μ (↑(const α c) ⁻¹' {x}) = c * ↑↑μ univ
simp [μ.eq_zero_of_isEmpty]
case inr
α : Type u_1
β : Type ?u.889363
γ : Type ?u.889366
δ : Type ?u.889369
m : MeasurableSpace α
μ ν : Measure α
c : ℝ≥0∞
h✝ : Nonempty α
⊢ c * ↑↑μ (Function.const α c ⁻¹' {c}) = c * ↑↑μ univ
case inr
α : Type u_1
β : Type ?u.889363
γ : Type ?u.889366
δ : Type ?u.889369
m : MeasurableSpace α
μ ν : Measure α
c : ℝ≥0∞
h✝ : Nonempty α
⊢ ∑ x in SimpleFunc.range (const α c), x * ↑↑μ (↑(const α c) ⁻¹' {x}) = c * ↑↑μ univ
simp
case inr
α : Type u_1
β : Type ?u.889363
γ : Type ?u.889366
δ : Type ?u.889369
m : MeasurableSpace α
μ ν : Measure α
c : ℝ≥0∞
h✝ : Nonempty α
⊢ c * ↑↑μ ((fun x => c) ⁻¹' {c}) = c * ↑↑μ univ
case inr
α : Type u_1
β : Type ?u.889363
γ : Type ?u.889366
δ : Type ?u.889369
m : MeasurableSpace α
μ ν : Measure α
c : ℝ≥0∞
h✝ : Nonempty α
⊢ c * ↑↑μ (Function.const α c ⁻¹' {c}) = c * ↑↑μ univ
unfold Function.const
no goals
case inr
α : Type u_1
β : Type ?u.889363
γ : Type ?u.889366
δ : Type ?u.889369
m : MeasurableSpace α
μ ν : Measure α
c : ℝ≥0∞
h✝ : Nonempty α
⊢ c * ↑↑μ ((fun x => c) ⁻¹' {c}) = c * ↑↑μ univ
rw [preimage_const_of_mem (mem_singleton c)]