-- Mathlib/MeasureTheory/VectorMeasure/WithDensity.lean
theorem withDensityᵥ_toReal {f : α → ℝ≥0∞} (hfm : AEMeasurable f μ) (hf : (∫⁻ x, f x ∂μ) ≠ ∞) :
    (μ.withDensityᵥ fun x => (f x).toReal) =
      @toSignedMeasure α _ (μ.withDensity f) (isFiniteMeasure_withDensity hf)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
⊢ (μ.withDensityᵥ fun x => (f x).toReal) = (μ.withDensity f).toSignedMeasure

Tactic:
have hfi := integrable_toReal_of_lintegral_ne_top hfm hf

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hfi : Integrable (fun x => (f x).toReal) μ
⊢ (μ.withDensityᵥ fun x => (f x).toReal) = (μ.withDensity f).toSignedMeasure

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hfi : Integrable (fun x => (f x).toReal) μ
this : IsFiniteMeasure (μ.withDensity f)
i : Set α
hi : MeasurableSet i
⊢ ∀ᵐ (x : α) ∂μ.restrict i, f x < ⊤

Tactic:
refine ae_lt_top' hfm.restrict (ne_top_of_le_ne_top hf ?_)

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hfi : Integrable (fun x => (f x).toReal) μ
this : IsFiniteMeasure (μ.withDensity f)
i : Set α
hi : MeasurableSet i
⊢ ∫⁻ (x : α) in i, f x ∂μ ≤ ∫⁻ (x : α), f x ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hfi : Integrable (fun x => (f x).toReal) μ
this : IsFiniteMeasure (μ.withDensity f)
⊢ (μ.withDensityᵥ fun x => (f x).toReal) = (μ.withDensity f).toSignedMeasure

Tactic:
ext i hi

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hfi : Integrable (fun x => (f x).toReal) μ
this : IsFiniteMeasure (μ.withDensity f)
i : Set α
hi : MeasurableSet i
⊢ ↑(μ.withDensityᵥ fun x => (f x).toReal) i = ↑(μ.withDensity f).toSignedMeasure i

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hfi : Integrable (fun x => (f x).toReal) μ
⊢ (μ.withDensityᵥ fun x => (f x).toReal) = (μ.withDensity f).toSignedMeasure

Tactic:
haveI := isFiniteMeasure_withDensity hf

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hfi : Integrable (fun x => (f x).toReal) μ
this : IsFiniteMeasure (μ.withDensity f)
⊢ (μ.withDensityᵥ fun x => (f x).toReal) = (μ.withDensity f).toSignedMeasure

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hfi : Integrable (fun x => (f x).toReal) μ
this : IsFiniteMeasure (μ.withDensity f)
i : Set α
hi : MeasurableSet i
⊢ ∫⁻ (x : α) in i, f x ∂μ ≤ ∫⁻ (x : α), f x ∂μ

Tactic:
conv_rhs => rw [← setLIntegral_univ]

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hfi : Integrable (fun x => (f x).toReal) μ
this : IsFiniteMeasure (μ.withDensity f)
i : Set α
hi : MeasurableSet i
⊢ ∫⁻ (x : α) in i, f x ∂μ ≤ ∫⁻ (x : α) in Set.univ, f x ∂μ

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hfi : Integrable (fun x => (f x).toReal) μ
this : IsFiniteMeasure (μ.withDensity f)
i : Set α
hi : MeasurableSet i
⊢ ∫⁻ (x : α) in i, f x ∂μ ≤ ∫⁻ (x : α) in Set.univ, f x ∂μ

Tactic:
exact lintegral_mono_set (Set.subset_univ _)

Result:
no goals

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hfi : Integrable (fun x => (f x).toReal) μ
this : IsFiniteMeasure (μ.withDensity f)
i : Set α
hi : MeasurableSet i
⊢ ↑(μ.withDensityᵥ fun x => (f x).toReal) i = ↑(μ.withDensity f).toSignedMeasure i

Tactic:
rw [withDensityᵥ_apply hfi hi, toSignedMeasure_apply_measurable hi, withDensity_apply _ hi,
  integral_toReal hfm.restrict]

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hfi : Integrable (fun x => (f x).toReal) μ
this : IsFiniteMeasure (μ.withDensity f)
i : Set α
hi : MeasurableSet i
⊢ ∀ᵐ (x : α) ∂μ.restrict i, f x < ⊤