case h.e'_5.h
α : Type u_1
𝕜 : Type u_2
inst✝¹ : IsROrC 𝕜
inst✝ : MeasurableSpace α
f : α → 𝕜
μ : MeasureTheory.Measure α
hre : Measurable fun x => ↑IsROrC.re (f x)
him : Measurable fun x => ↑IsROrC.im (f x)
x✝ : α
⊢ f x✝ = (IsROrC.ofReal ∘ fun x => ↑IsROrC.re (f x)) x✝ + (IsROrC.ofReal ∘ fun x => ↑IsROrC.im (f x)) x✝ * IsROrC.I
α : Type u_1
𝕜 : Type u_2
inst✝¹ : IsROrC 𝕜
inst✝ : MeasurableSpace α
f : α → 𝕜
μ : MeasureTheory.Measure α
hre : Measurable fun x => ↑IsROrC.re (f x)
him : Measurable fun x => ↑IsROrC.im (f x)
⊢ Measurable f
convert Measurable.add (M := 𝕜) (IsROrC.measurable_ofReal.comp hre)
    ((IsROrC.measurable_ofReal.comp him).mul_const IsROrC.I)
no goals
case h.e'_5.h
α : Type u_1
𝕜 : Type u_2
inst✝¹ : IsROrC 𝕜
inst✝ : MeasurableSpace α
f : α → 𝕜
μ : MeasureTheory.Measure α
hre : Measurable fun x => ↑IsROrC.re (f x)
him : Measurable fun x => ↑IsROrC.im (f x)
x✝ : α
⊢ f x✝ = (IsROrC.ofReal ∘ fun x => ↑IsROrC.re (f x)) x✝ + (IsROrC.ofReal ∘ fun x => ↑IsROrC.im (f x)) x✝ * IsROrC.I
exact (IsROrC.re_add_im _).symm