α : Type u_1
β : Type ?u.953229
γ : Type ?u.953232
δ : Type ?u.953235
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
this : ∀ᵐ (x : α) ∂μ, x ∈ {x | f x = r} → f x = r
⊢ (∫⁻ (x : α) in {x | f x = r}, f x ∂μ) = r * ↑↑μ {x | f x = r}
α : Type u_1
β : Type ?u.953229
γ : Type ?u.953232
δ : Type ?u.953235
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
⊢ (∫⁻ (x : α) in {x | f x = r}, f x ∂μ) = r * ↑↑μ {x | f x = r}
have : ∀ᵐ x ∂μ, x ∈ { x | f x = r } → f x = r := ae_of_all μ fun _ hx => hx
α : Type u_1
β : Type ?u.953229
γ : Type ?u.953232
δ : Type ?u.953235
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
this : ∀ᵐ (x : α) ∂μ, x ∈ {x | f x = r} → f x = r
⊢ (∫⁻ (x : α) in {x | f x = r}, r ∂μ) = r * ↑↑μ {x | f x = r}

α : Type u_1
β : Type ?u.953229
γ : Type ?u.953232
δ : Type ?u.953235
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
this : ∀ᵐ (x : α) ∂μ, x ∈ {x | f x = r} → f x = r
⊢ MeasurableSet {x | f x = r}
α : Type u_1
β : Type ?u.953229
γ : Type ?u.953232
δ : Type ?u.953235
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
this : ∀ᵐ (x : α) ∂μ, x ∈ {x | f x = r} → f x = r
⊢ (∫⁻ (x : α) in {x | f x = r}, f x ∂μ) = r * ↑↑μ {x | f x = r}
rw [set_lintegral_congr_fun _ this]
α : Type u_1
β : Type ?u.953229
γ : Type ?u.953232
δ : Type ?u.953235
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
this : ∀ᵐ (x : α) ∂μ, x ∈ {x | f x = r} → f x = r
⊢ (∫⁻ (x : α) in {x | f x = r}, r ∂μ) = r * ↑↑μ {x | f x = r}

α : Type u_1
β : Type ?u.953229
γ : Type ?u.953232
δ : Type ?u.953235
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
this : ∀ᵐ (x : α) ∂μ, x ∈ {x | f x = r} → f x = r
⊢ MeasurableSet {x | f x = r}
α : Type u_1
β : Type ?u.953229
γ : Type ?u.953232
δ : Type ?u.953235
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
this : ∀ᵐ (x : α) ∂μ, x ∈ {x | f x = r} → f x = r
⊢ (∫⁻ (x : α) in {x | f x = r}, r ∂μ) = r * ↑↑μ {x | f x = r}

α : Type u_1
β : Type ?u.953229
γ : Type ?u.953232
δ : Type ?u.953235
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
this : ∀ᵐ (x : α) ∂μ, x ∈ {x | f x = r} → f x = r
⊢ MeasurableSet {x | f x = r}
dsimp
α : Type u_1
β : Type ?u.953229
γ : Type ?u.953232
δ : Type ?u.953235
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
this : ∀ᵐ (x : α) ∂μ, x ∈ {x | f x = r} → f x = r
⊢ MeasurableSet {x | f x = r}
α : Type u_1
β : Type ?u.953229
γ : Type ?u.953232
δ : Type ?u.953235
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
this : ∀ᵐ (x : α) ∂μ, x ∈ {x | f x = r} → f x = r
⊢ (∫⁻ (x : α) in {x | f x = r}, r ∂μ) = r * ↑↑μ {x | f x = r}

α : Type u_1
β : Type ?u.953229
γ : Type ?u.953232
δ : Type ?u.953235
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
this : ∀ᵐ (x : α) ∂μ, x ∈ {x | f x = r} → f x = r
⊢ MeasurableSet {x | f x = r}
rw [lintegral_const, Measure.restrict_apply MeasurableSet.univ, Set.univ_inter]
no goals
α : Type u_1
β : Type ?u.953229
γ : Type ?u.953232
δ : Type ?u.953235
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
this : ∀ᵐ (x : α) ∂μ, x ∈ {x | f x = r} → f x = r
⊢ MeasurableSet {x | f x = r}
exact hf (measurableSet_singleton r)