simplify using a let / `intro` an integrated out variable

Stream: new members

[Nicholas Wilson]

If I have

import Mathlib.Data.Real.Basic
import Mathlib.Data.Complex.Basic
import Mathlib.Data.Complex.Exponential
import Mathlib.MeasureTheory.Integral.Bochner
open Complex
theorem odd_ft_sine_ft { a b : ℝ } (f : ℝ→ ℝ  ) :
        (∫ x, ((f x) - (f (-x) )/2)* exp (I*(a + b*I)*x) =
         ∫ x, (f x)* sin ((a + b*I)*x) ):= by
  let s : ℂ := a + b*I

Is there a simple way to apply a rewrite using the named let?
I can try to do have hs : s = a + b*I := by ring (ring is probably overkill but w/e) and then try to rewrite sin ((a + b*I)*x) as sin (s*x) but I need x declared, and intro x like

:= by
  intro x
  -- rest of proof

gives tactic 'introN' failed, insufficient number of binders. What can I do here?

[Mario Carneiro]

rfl is the 'right' way to prove s = a+b*I

[Mario Carneiro]

but you should be able to just rw [show s = a + b*I from rfl] here

[Mario Carneiro]

Also the set tactic should automatically do this substitution, and you can also get the equality via set s := a + b*I with H

[Nicholas Wilson]

set works marvellously, thanks!

[Nicholas Wilson]

Hmm,

set s : ℂ := a + b*I with H
simp [Complex.sin]

the simp seems to have undone the set. The state is now

∫ (x : ℝ), (↑(f x) - ↑(f (-x)) / 2) * cexp (I * (↑a + ↑b * I) * ↑x) =
  ∫ (x : ℝ), ↑(f x) * ((cexp (-((↑a + ↑b * I) * ↑x * I)) - cexp ((↑a + ↑b * I) * ↑x * I)) * I / 2)

[Nicholas Wilson]

whereas before the simp the state is

∫ (x : ℝ), (↑(f x) - ↑(f (-x)) / 2) * cexp (I * s * ↑x) = ∫ (x : ℝ), ↑(f x) * Complex.sin (s * ↑x)

[Nicholas Wilson]

Is there a way to make that set permanent?

[Nicholas Wilson]

Also what is the difference between set s : ℂ := a + b*I with H and set s : ℂ := a + b*I, both seem to have the same effect. I take it h is the default name for the hypothesis that you are trying to prove?

[Mario Carneiro]

you need to set simp (config := {zeta := false}), the next version of lean will have this on by default

[Mario Carneiro]

H there gives you a name for the equality s = a + b*I in case you need it for other reasons

[Mario Carneiro]

if you don't name it I think you don't get this equality at all (but you can still prove it yourself with have H : s = a + b*I := rfl as before)

[Nicholas Wilson]

Thanks that works. I still need a way to name x as the simp has the multiplications of x,s,I in a different order than the exp in the hypothesis.

[Mario Carneiro]

you should probably use simpa instead of simp if you are trying to make the goal expression line up with a hypothesis

[Nicholas Wilson]

simpa (config := {zeta := false}) [Complex.sin] gives tactic 'assumption' failed.
Reading the docs for simpa i presume that is because the goal is not anywhere close to proof yet.