α : Type u_2
β : Type ?u.62682
m : MeasurableSpace α
μ ν : Measure α
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g✝ f g : α → E
hf : Integrable f
hg : Integrable g
hfg : withDensityᵥ μ f = withDensityᵥ μ g
i : Set α
hi : MeasurableSet i
x✝ : ↑↑μ i < ⊤
⊢ (∫ (x : α) in i, f x ∂μ) = ∫ (x : α) in i, g x ∂μ
α : Type u_2
β : Type ?u.62682
m : MeasurableSpace α
μ ν : Measure α
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g✝ f g : α → E
hf : Integrable f
hg : Integrable g
hfg : withDensityᵥ μ f = withDensityᵥ μ g
⊢ f =ᶠ[ae μ] g
refine' hf.ae_eq_of_forall_set_integral_eq f g hg fun i hi _ => _
no goals
α : Type u_2
β : Type ?u.62682
m : MeasurableSpace α
μ ν : Measure α
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g✝ f g : α → E
hf : Integrable f
hg : Integrable g
hfg : withDensityᵥ μ f = withDensityᵥ μ g
i : Set α
hi : MeasurableSet i
x✝ : ↑↑μ i < ⊤
⊢ (∫ (x : α) in i, f x ∂μ) = ∫ (x : α) in i, g x ∂μ
rw [← withDensityᵥ_apply hf hi, hfg, withDensityᵥ_apply hg hi]