-- Mathlib/MeasureTheory/Measure/WithDensity.lean
theorem aemeasurable_withDensity_ennreal_iff' {f : α → ℝ≥0}
    (hf : AEMeasurable f μ) {g : α → ℝ≥0∞} :
    AEMeasurable g (μ.withDensity fun x => (f x : ℝ≥0∞)) ↔
      AEMeasurable (fun x => (f x : ℝ≥0∞) * g x) μ

Proof state:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᶠ[ae (μ.withDensity fun x => ↑(f x))] g'
A : MeasurableSet {x | f' x ≠ 0}
a : α
ha : f a = 0
ha_null✝ : a ∈ {x | f' x ≠ 0}ᶜ
ha_null : f' a = 0
⊢ ↑(f a) * g a = ↑0 * g' a

Tactic:
rw [ha]

Result:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᶠ[ae (μ.withDensity fun x => ↑(f x))] g'
A : MeasurableSet {x | f' x ≠ 0}
a : α
ha : f a = 0
ha_null✝ : a ∈ {x | f' x ≠ 0}ᶜ
ha_null : f' a = 0
⊢ ↑0 * g a = ↑0 * g' a

Proof state:
case intro.intro.mp.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᶠ[ae (μ.withDensity fun x => ↑(f x))] g'
A : MeasurableSet {x | f' x ≠ 0}
⊢ AEMeasurable (fun x => ↑(f x) * g x) μ

Tactic:
refine ⟨fun x => f' x * g' x, hf'_m.coe_nnreal_ennreal.smul g'meas, ?_⟩

Result:
case intro.intro.mp.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᶠ[ae (μ.withDensity fun x => ↑(f x))] g'
A : MeasurableSet {x | f' x ≠ 0}
⊢ (fun x => ↑(f x) * g x) =ᶠ[ae μ] fun x => ↑(f' x) * g' x

Proof state:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᶠ[ae (μ.withDensity fun x => ↑(f x))] g'
A : MeasurableSet {x | f' x ≠ 0}
a : α
ha : f a = f' a
ha_null✝ : a ∈ {x | f' x ≠ 0}ᶜ
ha_null : f' a = 0
⊢ ↑(f a) * g a = ↑(f' a) * g' a

Tactic:
rw [ha_null] at ha ⊢

Result:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᶠ[ae (μ.withDensity fun x => ↑(f x))] g'
A : MeasurableSet {x | f' x ≠ 0}
a : α
ha : f a = 0
ha_null✝ : a ∈ {x | f' x ≠ 0}ᶜ
ha_null : f' a = 0
⊢ ↑(f a) * g a = ↑0 * g' a

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
⊢ AEMeasurable g (μ.withDensity fun x => ↑(f x)) ↔ AEMeasurable (fun x => ↑(f x) * g x) μ

Tactic:
have t : ∃ f', Measurable f' ∧ f =ᵐ[μ] f' := hf

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
t : ∃ f', Measurable f' ∧ f =ᶠ[ae μ] f'
⊢ AEMeasurable g (μ.withDensity fun x => ↑(f x)) ↔ AEMeasurable (fun x => ↑(f x) * g x) μ

Proof state:
case intro.intro.mp
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
⊢ AEMeasurable g (μ.withDensity fun x => ↑(f x)) → AEMeasurable (fun x => ↑(f x) * g x) μ

Tactic:
rintro ⟨g', g'meas, hg'⟩

Result:
case intro.intro.mp.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᶠ[ae (μ.withDensity fun x => ↑(f x))] g'
⊢ AEMeasurable (fun x => ↑(f x) * g x) μ

Proof state:
case intro.intro.mpr.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : (fun x => ↑(f x) * g x) =ᶠ[ae μ] g'
⊢ g =ᶠ[ae (μ.withDensity fun x => ↑(f x))] fun x => (↑(f' x))⁻¹ * g' x

Tactic:
rw [EventuallyEq, ae_withDensity_iff' hf.coe_nnreal_ennreal]

Result:
case intro.intro.mpr.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : (fun x => ↑(f x) * g x) =ᶠ[ae μ] g'
⊢ ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = (↑(f' x))⁻¹ * g' x

Proof state:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : (fun x => ↑(f x) * g x) =ᶠ[ae μ] g'
a : α
hfga : ↑(f a) * g a = g' a
hff'a : f a = f' a
h'a : ↑(f a) ≠ 0
⊢ g a = (↑(f' a))⁻¹ * g' a

Tactic:
rw [hff'a] at hfga h'a

Result:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : (fun x => ↑(f x) * g x) =ᶠ[ae μ] g'
a : α
hfga : ↑(f' a) * g a = g' a
hff'a : f a = f' a
h'a : ↑(f' a) ≠ 0
⊢ g a = (↑(f' a))⁻¹ * g' a

Proof state:
case intro.intro.mpr.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : (fun x => ↑(f x) * g x) =ᶠ[ae μ] g'
⊢ AEMeasurable g (μ.withDensity fun x => ↑(f x))

Tactic:
refine ⟨fun x => ((f' x)⁻¹ : ℝ≥0∞) * g' x, hf'_m.coe_nnreal_ennreal.inv.smul g'meas, ?_⟩

Result:
case intro.intro.mpr.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : (fun x => ↑(f x) * g x) =ᶠ[ae μ] g'
⊢ g =ᶠ[ae (μ.withDensity fun x => ↑(f x))] fun x => (↑(f' x))⁻¹ * g' x

Proof state:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᶠ[ae (μ.withDensity fun x => ↑(f x))] g'
A : MeasurableSet {x | f' x ≠ 0}
a : α
ha : f a = f' a
ha_null : a ∈ {x | f' x ≠ 0}ᶜ
⊢ ↑(f a) * g a = ↑(f' a) * g' a

Tactic:
have ha_null : f' a = 0 := Function.nmem_support.mp ha_null

Result:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᶠ[ae (μ.withDensity fun x => ↑(f x))] g'
A : MeasurableSet {x | f' x ≠ 0}
a : α
ha : f a = f' a
ha_null✝ : a ∈ {x | f' x ≠ 0}ᶜ
ha_null : f' a = 0
⊢ ↑(f a) * g a = ↑(f' a) * g' a

Proof state:
case intro.intro.mpr.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : (fun x => ↑(f x) * g x) =ᶠ[ae μ] g'
⊢ ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = (↑(f' x))⁻¹ * g' x

Tactic:
filter_upwards [hg', hf'_ae] with a hfga hff'a h'a

Result:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : (fun x => ↑(f x) * g x) =ᶠ[ae μ] g'
a : α
hfga : ↑(f a) * g a = g' a
hff'a : f a = f' a
h'a : ↑(f a) ≠ 0
⊢ g a = (↑(f' a))⁻¹ * g' a