-- Mathlib/MeasureTheory/Measure/WithDensity.lean
lemma IsLocallyFiniteMeasure.withDensity_coe {f : α → ℝ≥0} (hf : Continuous f) :
    IsLocallyFiniteMeasure (μ.withDensity fun x ↦ f x)

Proof state:
case intro.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → ℝ≥0
hf : Continuous f
x : α
U : Set α
hμU : μ U < ⊤
hUf : U ⊆ {x_1 | (fun a => f a ≤ f x + 1) x_1}
hUx : U ∈ nhds x
hUo : IsOpen U
⊢ ∫⁻ (a : α) in U, ↑(f a) ∂μ < ⊤

Tactic:
exact setLIntegral_lt_top_of_bddAbove hμU.ne ⟨f x + 1, forall_mem_image.2 hUf⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → ℝ≥0
hf : Continuous f
x : α
U : Set α
hμU : μ U < ⊤
hUf : U ⊆ {x_1 | (fun a => f a ≤ f x + 1) x_1}
hUx : U ∈ nhds x
hUo : IsOpen U
⊢ (μ.withDensity fun x => ↑(f x)).FiniteAtFilter (nhds x)

Tactic:
refine ⟨U, hUx, ?_⟩

Result:
case intro.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → ℝ≥0
hf : Continuous f
x : α
U : Set α
hμU : μ U < ⊤
hUf : U ⊆ {x_1 | (fun a => f a ≤ f x + 1) x_1}
hUx : U ∈ nhds x
hUo : IsOpen U
⊢ (μ.withDensity fun x => ↑(f x)) U < ⊤

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → ℝ≥0
hf : Continuous f
⊢ IsLocallyFiniteMeasure (μ.withDensity fun x => ↑(f x))

Tactic:
refine ⟨fun x ↦ ?_⟩

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → ℝ≥0
hf : Continuous f
x : α
⊢ (μ.withDensity fun x => ↑(f x)).FiniteAtFilter (nhds x)

Proof state:
case intro.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → ℝ≥0
hf : Continuous f
x : α
U : Set α
hμU : μ U < ⊤
hUf : U ⊆ {x_1 | (fun a => f a ≤ f x + 1) x_1}
hUx : U ∈ nhds x
hUo : IsOpen U
⊢ (μ.withDensity fun x => ↑(f x)) U < ⊤

Tactic:
rw [withDensity_apply _ hUo.measurableSet]

Result:
case intro.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → ℝ≥0
hf : Continuous f
x : α
U : Set α
hμU : μ U < ⊤
hUf : U ⊆ {x_1 | (fun a => f a ≤ f x + 1) x_1}
hUx : U ∈ nhds x
hUo : IsOpen U
⊢ ∫⁻ (a : α) in U, ↑(f a) ∂μ < ⊤

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → ℝ≥0
hf : Continuous f
x : α
⊢ (μ.withDensity fun x => ↑(f x)).FiniteAtFilter (nhds x)

Tactic:
rcases (μ.finiteAt_nhds x).exists_mem_basis ((nhds_basis_opens' x).restrict_subset
  ((hf.tendsto x).eventually_le_const (lt_add_one _))) with ⟨U, ⟨⟨hUx, hUo⟩, hUf⟩, hμU⟩

Result:
case intro.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → ℝ≥0
hf : Continuous f
x : α
U : Set α
hμU : μ U < ⊤
hUf : U ⊆ {x_1 | (fun a => f a ≤ f x + 1) x_1}
hUx : U ∈ nhds x
hUo : IsOpen U
⊢ (μ.withDensity fun x => ↑(f x)).FiniteAtFilter (nhds x)