[GOAL]
α : 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
[PROOFSTEP]
convert
  Measurable.add (M := 𝕜) (IsROrC.measurable_ofReal.comp hre) ((IsROrC.measurable_ofReal.comp him).mul_const IsROrC.I)
[GOAL]
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
[PROOFSTEP]
exact (IsROrC.re_add_im _).symm
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : IsROrC 𝕜
inst✝ : MeasurableSpace α
f : α → 𝕜
μ : MeasureTheory.Measure α
hre : AEMeasurable fun x => ↑IsROrC.re (f x)
him : AEMeasurable fun x => ↑IsROrC.im (f x)
⊢ AEMeasurable f
[PROOFSTEP]
convert
  AEMeasurable.add (M := 𝕜) (IsROrC.measurable_ofReal.comp_aemeasurable hre)
    ((IsROrC.measurable_ofReal.comp_aemeasurable him).mul_const IsROrC.I)
[GOAL]
case h.e'_5.h
α : Type u_1
𝕜 : Type u_2
inst✝¹ : IsROrC 𝕜
inst✝ : MeasurableSpace α
f : α → 𝕜
μ : MeasureTheory.Measure α
hre : AEMeasurable fun x => ↑IsROrC.re (f x)
him : AEMeasurable 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
[PROOFSTEP]
exact (IsROrC.re_add_im _).symm
