∀ {X : Type u_1} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝕜 : Type u_6} [inst_1 : RCLike 𝕜]
  {f : X → 𝕜},
  MeasureTheory.Integrable f μ →
    ↑(∫ (x : X), RCLike.re (f x) ∂μ) + ↑(∫ (x : X), RCLike.im (f x) ∂μ) * RCLike.I = ∫ (x : X), f x ∂μ