Rewrite goal in terms of function

Stream: new members

[Julia Ramos Alves]

Hello all! I have extracted the following example from a proof that I am working on:

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

example (n : ℤ)(hn : n ≠ 0) :
  (2 * ↑real.pi)⁻¹ *
      ∫ (x : ℝ) in
        -real.pi..real.pi,
        ↑x * complex.exp (-complex.I * ↑n * ↑x) =
    (-1) ^ n * complex.I / ↑n :=
begin
  let u: ℝ → ℂ:= λ x, x,
  let v: ℝ → ℂ:= λ x, complex.exp (-complex.I * n * x) * (complex.I/ n),
  let u': ℝ → ℂ := λ x, 1,
  let v': ℝ → ℂ := λ x, complex.exp (-complex.I * n * x),
end

My problem is that I want to be able to write the goal in terms of these defined functions, but since they are not iff or eq, then rw does not work for it, how should I approach this? Is there a way to keep these let statements as they are and do this or do I have to turn them into different statements for it to work?

[Ruben Van de Velde]

change (tactic#change) probably works

[Yaël Dillies]

Use docs#tactic.interactive.set instead of let. Then you can specify a name for the hypothesis that u, v, u', v' are equal to their definition.

[Julia Ramos Alves]

I have tried both of these suggestions but they haven't worked.

[Yaël Dillies]

Can you show me what you tried precisely?

[Julia Ramos Alves]

I wrote

set u: ℝ → ℂ:= λ x, x with hu,
set v: ℝ → ℂ:= λ x, complex.exp (-complex.I * n * x) * (complex.I/ n) with hv,

instead of the previous first two let statements and also tried a few things like rw v, simp_rw v, rw \l hv, change hv.
I don't know exactly how to make it work.

[Yaël Dillies]

Can you copy-paste the full code block?

[Ruben Van de Velde]

Have you read the documentation for change that I linked to?

[Moritz Doll]

I think we have a #xy problem here: the real question is how to do integration by parts. The answer to that is that you need a

have : λ x, has_deriv_at (λ y, complex.exp (-complex.I * n * y) * (complex.I/ n)) complex.exp (-complex.I * n * x) x := sorry

(I haven't checked that code)
the derivative of the coercion:

import analysis.calculus.fderiv
import analysis.complex.basic
import analysis.calculus.deriv

lemma has_fderiv_at_of_real {x : ℝ} : has_fderiv_at (coe : ℝ → ℂ) complex.of_real_clm x :=
continuous_linear_map.has_fderiv_at complex.of_real_clm

lemma has_deriv_at_of_real {x : ℝ} : has_deriv_at (coe : ℝ → ℂ) 1 x :=
has_fderiv_at_of_real.has_deriv_at

and with these things you can apply integration by parts without defining the functions by hand

[Moritz Doll]

btw the last lemma should be in mathlib, right?

[Junyan Xu]

Returning to the original problem, I usually do dsimp only [u] to expand a definition u via let within a proof. These definitions seem to be abbreviations or at least reducible, because rw sees through them (but split_ifs doesn't, for example), however no equational lemma is generated (similar to abbreviation) so you can't rw u (and unfold and dunfold also don't work).