rw [set_integral_withDensity_eq_set_integral_smul₀ _ _ hs_meas]
case hq_fg
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
⊢ (∫ (x : ℝ) in s, f x ∂Measure.withDensity μ fun x => ↑‖g x‖₊) = ∫ (x : ℝ) in s, f x * g x ∂μ
case hq_fg
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
⊢ ∫ (a : ℝ) in s, ‖g a‖₊ • f a ∂μ = ∫ (x : ℝ) in s, f x * g x ∂μ

f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
⊢ AEMeasurable fun x => ‖g x‖₊