case h
α : Type u_1
β : Type ?u.1814114
γ : Type ?u.1814117
δ : Type ?u.1814120
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
s : Set α
hs : MeasurableSet s
⊢ ↑↑(Measure.withDensity μ (f * g)) s = ↑↑(Measure.withDensity (Measure.withDensity μ f) g) s
α : Type u_1
β : Type ?u.1814114
γ : Type ?u.1814117
δ : Type ?u.1814120
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ Measure.withDensity μ (f * g) = Measure.withDensity (Measure.withDensity μ f) g
ext1 s hs
no goals
case h
α : Type u_1
β : Type ?u.1814114
γ : Type ?u.1814117
δ : Type ?u.1814120
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
s : Set α
hs : MeasurableSet s
⊢ ↑↑(Measure.withDensity μ (f * g)) s = ↑↑(Measure.withDensity (Measure.withDensity μ f) g) s
simp [withDensity_apply _ hs, restrict_withDensity hs,
  lintegral_withDensity_eq_lintegral_mul _ hf hg]