no goals
α : Type u_2
β : Type ?u.3500341
E : Type ?u.3500344
F : Type ?u.3500347
inst✝⁹ : MeasurableSpace α
ι : Type ?u.3500353
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type u_1
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
p : ℝ≥0∞
inst✝³ : CompleteSpace E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace ℝ F
f : α → 𝕜
hf : Integrable f
⊢ ↑(∫ (x : α), ↑IsROrC.re (f x) ∂μ) + ↑(∫ (x : α), ↑IsROrC.im (f x) ∂μ) * IsROrC.I = ∫ (x : α), f x ∂μ
rw [← integral_ofReal, ← integral_ofReal, integral_coe_re_add_coe_im hf]