-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem integrable_withDensity_iff_integrable_coe_smul₀ {f : α → ℝ≥0} (hf : AEMeasurable f μ)
    {g : α → E} :
    Integrable g (μ.withDensity fun x => f x) ↔ Integrable (fun x => (f x : ℝ) • g x) μ :=
  calc
    Integrable g (μ.withDensity fun x => f x) ↔
        Integrable g (μ.withDensity fun x => (hf.mk f x : ℝ≥0))

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → E
x : α
hx : f x = AEMeasurable.mk f hf x
⊢ ↑(f x) = ↑(AEMeasurable.mk f hf x)

Tactic:
simp [hx]

Result:
no goals

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → E
x : α
hx : f x = AEMeasurable.mk f hf x
⊢ ↑(AEMeasurable.mk f hf x) • g x = ↑(f x) • g x

Tactic:
simp [hx]

Result:
no goals

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → E
⊢ (fun x => ↑(AEMeasurable.mk f hf x) • g x) =ᶠ[ae μ] fun x => ↑(f x) • g x

Tactic:
filter_upwards [hf.ae_eq_mk] with x hx

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → E
x : α
hx : f x = AEMeasurable.mk f hf x
⊢ ↑(AEMeasurable.mk f hf x) • g x = ↑(f x) • g x

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → E
⊢ Integrable (fun x => ↑(AEMeasurable.mk f hf x) • g x) μ ↔ Integrable (fun x => ↑(f x) • g x) μ

Tactic:
apply integrable_congr

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → E
⊢ (fun x => ↑(AEMeasurable.mk f hf x) • g x) =ᶠ[ae μ] fun x => ↑(f x) • g x

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → E
this : (fun x => ↑(f x)) =ᶠ[ae μ] fun x => ↑(AEMeasurable.mk f hf x)
⊢ Integrable g (μ.withDensity fun x => ↑(f x)) ↔ Integrable g (μ.withDensity fun x => ↑(AEMeasurable.mk f hf x))

Tactic:
rw [withDensity_congr_ae this]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → E
⊢ (fun x => ↑(f x)) =ᶠ[ae μ] fun x => ↑(AEMeasurable.mk f hf x)

Tactic:
filter_upwards [hf.ae_eq_mk] with x hx

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → E
x : α
hx : f x = AEMeasurable.mk f hf x
⊢ ↑(f x) = ↑(AEMeasurable.mk f hf x)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → E
⊢ Integrable g (μ.withDensity fun x => ↑(f x)) ↔ Integrable g (μ.withDensity fun x => ↑(AEMeasurable.mk f hf x))

Tactic:
suffices (fun x => (f x : ℝ≥0∞)) =ᵐ[μ] (fun x => (hf.mk f x : ℝ≥0)) by
  rw [withDensity_congr_ae this]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → E
⊢ (fun x => ↑(f x)) =ᶠ[ae μ] fun x => ↑(AEMeasurable.mk f hf x)