no goals
α : Type u_1
β : Type ?u.1574917
γ : Type ?u.1574920
δ : Type ?u.1574923
inst✝³ : MeasurableSpace α
μ ν : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α →ₘ[μ] ℝ≥0∞
⊢ (∫⁻ (a : α), ↑f a ∂μ) = lintegral f
rw [← lintegral_mk, mk_coeFn]