-- Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean
theorem fourierIntegral_half_period_translate {w : V} (hw : w ≠ 0) :
    (∫ v : V, 𝐞 (-⟪v, w⟫) • f (v + i w)) = -∫ v : V, 𝐞 (-⟪v, w⟫) • f v

Proof state:
E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
w : V
hw : w ≠ 0
hiw : inner (i w) w = 1 / 2
this : (fun v => 𝐞 (-inner v w) • f (v + i w)) = fun v => (fun x => -(𝐞 (-inner x w) • f x)) (v + i w)
⊢ ∫ (v : V), 𝐞 (-inner v w) • f (v + i w) = -∫ (v : V), 𝐞 (-inner v w) • f v

Tactic:
rw [this]

Result:
E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
w : V
hw : w ≠ 0
hiw : inner (i w) w = 1 / 2
this : (fun v => 𝐞 (-inner v w) • f (v + i w)) = fun v => (fun x => -(𝐞 (-inner x w) • f x)) (v + i w)
⊢ ∫ (v : V), (fun x => -(𝐞 (-inner x w) • f x)) (v + i w) = -∫ (v : V), 𝐞 (-inner v w) • f v

Proof state:
case h
E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
w : V
hw : w ≠ 0
hiw : inner (i w) w = 1 / 2
v : V
⊢ 𝐞 (-inner v w) • f (v + i w) = (fun x => -(𝐞 (-inner x w) • f x)) (v + i w)

Tactic:
simp_rw [inner_add_left, hiw, Circle.smul_def, Real.fourierChar_apply, neg_add, mul_add,
  ofReal_add, add_mul, exp_add]

Result:
case h
E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
w : V
hw : w ≠ 0
hiw : inner (i w) w = 1 / 2
v : V
⊢ cexp (↑(2 * π * -inner v w) * I) • f (v + (1 / (2 * ‖w‖ ^ 2)) • w) =
    -((cexp (↑(2 * π * -inner v w) * I) * cexp (↑(2 * π * -(1 / 2)) * I)) • f (v + (1 / (2 * ‖w‖ ^ 2)) • w))

Proof state:
E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
w : V
hw : w ≠ 0
hiw : inner (i w) w = 1 / 2
v : V
⊢ 2 * π = π * 2

Tactic:
ring

Result:
no goals

Proof state:
E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
w : V
hw : w ≠ 0
hiw : inner (i w) w = 1 / 2
⊢ ∫ (v : V), 𝐞 (-inner v w) • f (v + i w) = -∫ (v : V), 𝐞 (-inner v w) • f v

Tactic:
have :
  (fun v : V => 𝐞 (-⟪v, w⟫) • f (v + i w)) =
    fun v : V => (fun x : V => -(𝐞 (-⟪x, w⟫) • f x)) (v + i w) := by
  ext1 v
  simp_rw [inner_add_left, hiw, Circle.smul_def, Real.fourierChar_apply, neg_add, mul_add,
    ofReal_add, add_mul, exp_add]
  have : 2 * π * -(1 / 2) = -π := by field_simp; ring
  rw [this, ofReal_neg, neg_mul, exp_neg, exp_pi_mul_I, inv_neg, inv_one, mul_neg_one, neg_smul,
    neg_neg]

Result:
E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
w : V
hw : w ≠ 0
hiw : inner (i w) w = 1 / 2
this : (fun v => 𝐞 (-inner v w) • f (v + i w)) = fun v => (fun x => -(𝐞 (-inner x w) • f x)) (v + i w)
⊢ ∫ (v : V), 𝐞 (-inner v w) • f (v + i w) = -∫ (v : V), 𝐞 (-inner v w) • f v

Proof state:
E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
w : V
hw : w ≠ 0
hiw : inner (i w) w = 1 / 2
v : V
⊢ 2 * π * -(1 / 2) = -π

Tactic:
field_simp

Result:
E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
w : V
hw : w ≠ 0
hiw : inner (i w) w = 1 / 2
v : V
⊢ 2 * π = π * 2