-- 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:
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
⊢ ‖w‖ ^ 2 ≠ 0

Tactic:
rwa [Ne, sq_eq_zero_iff, norm_eq_zero]

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
this✝ : (fun v => 𝐞 (-inner v w) • f (v + i w)) = fun v => (fun x => -(𝐞 (-inner x w) • f x)) (v + i w)
this : ∫ (x : V), -(𝐞 (-inner (x + i w) w) • f (x + i w)) = ∫ (x : V), -(𝐞 (-inner x w) • f x)
⊢ ∫ (v : V), (fun x => -(𝐞 (-inner x w) • f x)) (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)
this : ∫ (x : V), -(𝐞 (-inner (x + i w) w) • f (x + i w)) = ∫ (x : V), -(𝐞 (-inner x w) • f x)
⊢ ∫ (x : V), -(𝐞 (-inner x w) • f x) = -∫ (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
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

Tactic:
have := integral_add_right_eq_self (μ := volume) (fun (x : V) ↦ -(𝐞 (-⟪x, w⟫) • f x))
  ((fun w ↦ (1 / (2 * ‖w‖ ^ (2 : ℕ))) • w) w)

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)
this : ∫ (x : V), -(𝐞 (-inner (x + i w) w) • f (x + i w)) = ∫ (x : V), -(𝐞 (-inner x w) • f x)
⊢ ∫ (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
this : 2 * π * -(1 / 2) = -π
⊢ 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))

Tactic:
rw [this, ofReal_neg, neg_mul, exp_neg, exp_pi_mul_I, inv_neg, inv_one, mul_neg_one, neg_smul,
  neg_neg]

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
⊢ inner (i w) w = 1 / 2

Tactic:
rw [inner_smul_left, inner_self_eq_norm_sq_to_K, RCLike.ofReal_real_eq_id, id,
  RCLike.conj_to_real, ← div_div, div_mul_cancel₀]

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
⊢ ‖w‖ ^ 2 ≠ 0

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)
this : ∫ (x : V), -(𝐞 (-inner (x + i w) w) • f (x + i w)) = ∫ (x : V), -(𝐞 (-inner x w) • f x)
⊢ ∫ (x : V), -(𝐞 (-inner x w) • f x) = -∫ (v : V), 𝐞 (-inner v w) • f v

Tactic:
simp only [neg_smul, integral_neg]

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
⊢ ∫ (v : V), 𝐞 (-inner v w) • f (v + i w) = -∫ (v : V), 𝐞 (-inner v w) • f v

Tactic:
have hiw : ⟪i w, w⟫ = 1 / 2 := by
  rw [inner_smul_left, inner_self_eq_norm_sq_to_K, RCLike.ofReal_real_eq_id, id,
    RCLike.conj_to_real, ← div_div, div_mul_cancel₀]
  rwa [Ne, sq_eq_zero_iff, norm_eq_zero]

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), 𝐞 (-inner v w) • f (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
⊢ 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))

Tactic:
have : 2 * π * -(1 / 2) = -π := by field_simp; ring

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
this : 2 * π * -(1 / 2) = -π
⊢ 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
⊢ (fun v => 𝐞 (-inner v w) • f (v + i w)) = fun v => (fun x => -(𝐞 (-inner x w) • f x)) (v + i w)

Tactic:
ext1 v

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
⊢ 𝐞 (-inner v w) • f (v + i w) = (fun x => -(𝐞 (-inner x w) • f x)) (v + i w)