commuting casting with integration

Stream: new members

[Paul Nelson]

Does anyone know how to close this sorry? It says that if an integral involving real quantities vanishes, then so does the corresponding integral of quantities cast to the complex numbers.

import Mathlib.MeasureTheory.Integral.IntervalIntegral

example (a b : ℝ) (f : ℝ → ℝ) (hf : IntervalIntegrable f volume a b)
    (h : ∫ (x : ℝ) in a..b, f x = 0) :
  (∫ (x : ℝ) in a..b, (f x : ℂ)) = 0 := by
  sorry

Here's an unsuccessful attempt:

import Mathlib.MeasureTheory.Integral.IntervalIntegral

example (a b : ℝ) (f : ℝ → ℝ) (hf : IntervalIntegrable f volume a b)
    (h : ∫ (x : ℝ) in a..b, f x = 0) :
  (∫ (x : ℝ) in a..b, (f x : ℂ)) = 0 := by
  have : (∫ (x : ℝ) in a..b, (f x : ℂ)) = ((∫ (x : ℝ) in a..b, f x) : ℂ) := rfl
  rw [this] -- this rw has no effect on the goal state
  sorry

[Kevin Buzzard]

Not at lean right now but my guess is that the have is a syntactic equality? i.e. it doesn't say what you think it says?

[Paul Nelson]

indeed, the "have" just states a tautology

[Paul Nelson]

thing = thing

[Mario Carneiro]

maybe you want to say that an intermediate has type ℝ instead?

[Mario Carneiro]

have : (∫ (x : ℝ) in a..b, f x : ℂ) = (∫ (x : ℝ) in a..b, f x : ℝ) := _ is probably what you wanted to say

[Paul Nelson]

using Mario's suggestion, I closed it just now as follows:

import Mathlib.MeasureTheory.Integral.IntervalIntegral

example (a b : ℝ) (f : ℝ → ℝ) (hf : IntervalIntegrable f volume a b)
    (h : ∫ (x : ℝ) in a..b, f x = 0) :
  (∫ (x : ℝ) in a..b, (f x : ℂ)) = 0 := by
  have : (∫ (x : ℝ) in a..b, f x : ℂ) = (∫ (x : ℝ) in a..b, f x : ℝ) := by
    exact intervalIntegral.integral_ofReal
  rw [this]
  rw [h]
  rfl

I guess one could abbreviate this, but the key was being able to formulate the have correctly, which suggested the appropriate lemma via exact?. Thanks!