-- 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:
α : 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' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f' x ≠ 0}
a : α
ha : ↑(f a) ≠ 0 → g a = g' a
h'a : f a = f' a
h_a_nonneg : f' a ≠ 0
⊢ ↑(f' a) ≠ 0

Tactic:
simpa only [Ne, ENNReal.coe_eq_zero] using h_a_nonneg

Result:
no goals

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}
⊢ (fun x => ↑(f x) * g x) =ᶠ[ae μ] fun x => ↑(f' x) * g' x

Tactic:
apply ae_of_ae_restrict_of_ae_restrict_compl { x | f' x ≠ 0 }

Result:
case intro.intro.mp.intro.intro.ht
α : 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}
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f' x ≠ 0}, (fun x => ↑(f x) * g x) x = (fun x => ↑(f' x) * g' x) x

case intro.intro.mp.intro.intro.htc
α : 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}
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f' x ≠ 0}ᶜ, (fun x => ↑(f x) * g x) x = (fun x => ↑(f' x) * g' x) x

Proof state:
case intro.intro.mp.intro.intro.htc
α : 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}
⊢ ∀ᵐ (x : α) ∂μ, x ∈ {x | f' x ≠ 0}ᶜ → (fun x => ↑(f x) * g x) x = (fun x => ↑(f' x) * g' x) x

Tactic:
filter_upwards [hf'_ae] with a ha 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}ᶜ
⊢ ↑(f a) * g a = ↑(f' a) * g' a

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 [← hfga, ← mul_assoc, ENNReal.inv_mul_cancel h'a ENNReal.coe_ne_top, one_mul]

Result:
no goals

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' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f' x ≠ 0}
a : α
ha : ↑(f a) ≠ 0 → g a = g' a
h'a : f a = f' a
h_a_nonneg : f' a ≠ 0
this : ↑(f a) ≠ 0
⊢ ↑(f a) * g a = ↑(f a) * g' a

Tactic:
rw [ha this]

Result:
no goals

Proof state:
case intro.intro.mp.intro.intro.ht
α : 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' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f' x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ, x ∈ {x | f' x ≠ 0} → (fun x => ↑(f x) * g x) x = (fun x => ↑(f' x) * g' x) x

Tactic:
filter_upwards [hg', hf'_ae] with a ha h'a h_a_nonneg

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' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f' x ≠ 0}
a : α
ha : ↑(f a) ≠ 0 → g a = g' a
h'a : f a = f' a
h_a_nonneg : f' a ≠ 0
⊢ ↑(f a) * g a = ↑(f' a) * g' a