is_R_or_C

Stream: new members

[Julia Ramos Alves]

Dear all, I am having some trouble with the following code:

import analysis.fourier
import measure_theory.integral.interval_integral
import data.real.basic
import analysis.special_functions.integrals

example (f : ℝ → ℂ)
  (hf : ∀ (x : ℝ), f x = ↑x)
  (this : interval_integrable f measure_theory.measure_space.volume (-real.pi)
            real.pi) :
  ∫ (x : ℝ) in -real.pi..real.pi, ↑x.re = 0.re :=
begin
    rw is_R_or_C.re_eq_complex_re,
end

I'm not quite sure that is_R_or_C.re_eq_complex_re is the way to go here, because I didn't fully grasp the concept of is_R_or_C. Could someone help me clear this up?

[Ruben Van de Velde]

You might want to fix these first:

don't know how to synthesize placeholder
context:
f : ℝ → ℂ,
hf : ∀ (x : ℝ), f x = ↑x,
this : interval_integrable f measure_theory.measure_space.volume (-real.pi) real.pi
⊢ Type ?
tmp.lean:10:34
don't know how to synthesize placeholder
context:
f : ℝ → ℂ,
hf : ∀ (x : ℝ), f x = ↑x,
this : interval_integrable f measure_theory.measure_space.volume (-real.pi) real.pi,
x : ℝ
⊢ Sort ?
tmp.lean:10:36
invalid field notation, 're' is not a valid "field" because environment does not contain 'real.re'
  x
which has type
  ℝ
tmp.lean:10:43
invalid field notation, type is not of the form (C ...) where C is a constant
  0
has type
  ?m_1

[Patrick Johnson]

Is it the output of extract_goal? Did you mean ∫ (x : ℝ) in -real.pi..real.pi, x = 0 instead? In that case, simp proves it.

[Moritz Doll]

as Patrick said, there is no reason to use is_R_or_C

[Julia Ramos Alves]

Indeed it was the output of extract goal and simp does work, thank you.