Can't rewrite with integral_ofReal

Stream: new members

[Duncan Skahan]

import Mathlib

open MeasureTheory ProbabilityTheory Complex

variable {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]

theorem test {X: Ω → ℝ} (h : ∫ (x : Ω), X x ∂P = 0) : ∫ (x : Ω), Complex.ofReal (X x) ∂P = 0 := by
  rw [integral_ofReal (μ := P) (f := X) (𝕜 := ℂ)]

gives

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  ∫ (x : Ω), ↑(X x) ∂P
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
P : Measure Ω
inst✝ : IsProbabilityMeasure P
X : Ω → ℝ
h : ∫ (x : Ω), X x ∂P = 0
⊢ ∫ (x : Ω), ↑(X x) ∂P = 0

[Duncan Skahan]

The up arrow in the target expression is @RCLike.ofReal ℂ instRCLike (X x) : ℂ and the up arrow in the goal is ofReal (X x) : ℂ.

[Ruben Van de Velde]

Huh, is there no API to link RCLike.ofReal and Complex.ofReal?

[Duncan Skahan]

But this works:

import Mathlib

open MeasureTheory ProbabilityTheory Complex

variable {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]

theorem test {X: Ω → ℝ} : ∫ (x : Ω), Complex.ofReal (X x) ∂P = ∫ (x : Ω), X x ∂P := by
  apply integral_ofReal

[Duncan Skahan]

And so does this:

import Mathlib

open MeasureTheory ProbabilityTheory Complex

variable {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]

theorem test {X: Ω → ℝ} (h : ∫ (x : Ω), X x ∂P = 0) : ∫ (x : Ω), Complex.ofReal (X x) ∂P = 0 := by
  have h' :  ∫ (x : Ω), Complex.ofReal (X x) ∂P = ∫ (x : Ω), X x ∂P := integral_ofReal
  rw [h']
  simp [h]