-- Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean
theorem _root_.fourierIntegral_gaussian_innerProductSpace' (hb : 0 < b.re) (x w : V) :
    𝓕 (fun v ↦ cexp (- b * ‖v‖^2 + 2 * π * Complex.I * ⟪x, v⟫)) w =
      (π / b) ^ (Module.finrank ℝ V / 2 : ℂ) * cexp (-π ^ 2 * ‖x - w‖ ^ 2 / b)

Proof state:
case h.e'_2.h.e'_7.h.e_z
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
x w v : V
⊢ -(2 * ↑π * ↑(inner w v) * I) + (-(b * ↑‖v‖ ^ 2) + 2 * ↑π * I * ↑(inner x v)) =
    -(b * ↑‖v‖ ^ 2) + 2 * ↑π * I * (↑(inner x v) - ↑(inner w v))

Tactic:
ring

Result:
no goals

Proof state:
case h.e'_3.h.e'_6.h.e'_1
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
x w : V
this : b ≠ 0
⊢ ↑π ^ 2 * ↑‖x - w‖ ^ 2 * (4 * b) = 2 ^ 2 * ↑π ^ 2 * ↑‖x - w‖ ^ 2 * b

Tactic:
ring

Result:
no goals

Proof state:
case h.e'_3.h.e'_6.h.e'_1
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
x w : V
⊢ -(↑π ^ 2 * ↑‖x - w‖ ^ 2) / b = (2 * ↑π * I) ^ 2 * ↑‖x - w‖ ^ 2 / (4 * b)

Tactic:
have : b ≠ 0 := by contrapose! hb; rw [hb, zero_re]

Result:
case h.e'_3.h.e'_6.h.e'_1
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
x w : V
this : b ≠ 0
⊢ -(↑π ^ 2 * ↑‖x - w‖ ^ 2) / b = (2 * ↑π * I) ^ 2 * ↑‖x - w‖ ^ 2 / (4 * b)

Proof state:
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
x w : V
hb : b = 0
⊢ b.re ≤ 0

Tactic:
rw [hb, zero_re]

Result:
no goals

Proof state:
case h.e'_2.h.e'_7.h
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
x w v : V
⊢ cexp (-(2 * ↑π * ↑(inner w v) * I) + (-(b * ↑‖v‖ ^ 2) + 2 * ↑π * I * ↑(inner x v))) =
    cexp (-b * ↑‖v‖ ^ 2 + 2 * ↑π * I * ↑(inner (x - w) v))

Tactic:
congr 1

Result:
case h.e'_2.h.e'_7.h.e_z
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
x w v : V
⊢ -(2 * ↑π * ↑(inner w v) * I) + (-(b * ↑‖v‖ ^ 2) + 2 * ↑π * I * ↑(inner x v)) =
    -b * ↑‖v‖ ^ 2 + 2 * ↑π * I * ↑(inner (x - w) v)

Proof state:
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
x w : V
⊢ 𝓕 (fun v => cexp (-b * ↑‖v‖ ^ 2 + 2 * ↑π * I * ↑(inner x v))) w =
    (↑π / b) ^ (↑(Module.finrank ℝ V) / 2) * cexp (-↑π ^ 2 * ↑‖x - w‖ ^ 2 / b)

Tactic:
simp only [neg_mul, fourierIntegral_eq', ofReal_neg, ofReal_mul, ofReal_ofNat,
  smul_eq_mul, ← Complex.exp_add, real_inner_comm w]

Result:
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
x w : V
⊢ ∫ (v : V), cexp (-(2 * ↑π * ↑(inner w v) * I) + (-(b * ↑‖v‖ ^ 2) + 2 * ↑π * I * ↑(inner x v))) =
    (↑π / b) ^ (↑(Module.finrank ℝ V) / 2) * cexp (-(↑π ^ 2 * ↑‖x - w‖ ^ 2) / b)

Proof state:
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
x w : V
⊢ ∫ (v : V), cexp (-(2 * ↑π * ↑(inner w v) * I) + (-(b * ↑‖v‖ ^ 2) + 2 * ↑π * I * ↑(inner x v))) =
    (↑π / b) ^ (↑(Module.finrank ℝ V) / 2) * cexp (-(↑π ^ 2 * ↑‖x - w‖ ^ 2) / b)

Tactic:
convert integral_cexp_neg_mul_sq_norm_add hb (2 * π * Complex.I) (x - w) using 3 with v

Result:
case h.e'_2.h.e'_7.h
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
x w v : V
⊢ cexp (-(2 * ↑π * ↑(inner w v) * I) + (-(b * ↑‖v‖ ^ 2) + 2 * ↑π * I * ↑(inner x v))) =
    cexp (-b * ↑‖v‖ ^ 2 + 2 * ↑π * I * ↑(inner (x - w) v))

case h.e'_3.h.e'_6.h.e'_1
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
x w : V
⊢ -(↑π ^ 2 * ↑‖x - w‖ ^ 2) / b = (2 * ↑π * I) ^ 2 * ↑‖x - w‖ ^ 2 / (4 * b)

Proof state:
case h.e'_2.h.e'_7.h.e_z
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
x w v : V
⊢ -(2 * ↑π * ↑(inner w v) * I) + (-(b * ↑‖v‖ ^ 2) + 2 * ↑π * I * ↑(inner x v)) =
    -b * ↑‖v‖ ^ 2 + 2 * ↑π * I * ↑(inner (x - w) v)

Tactic:
simp [inner_sub_left]

Result:
case h.e'_2.h.e'_7.h.e_z
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
x w v : V
⊢ -(2 * ↑π * ↑(inner w v) * I) + (-(b * ↑‖v‖ ^ 2) + 2 * ↑π * I * ↑(inner x v)) =
    -(b * ↑‖v‖ ^ 2) + 2 * ↑π * I * (↑(inner x v) - ↑(inner w v))

Proof state:
case h.e'_3.h.e'_6.h.e'_1
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
x w : V
this : b ≠ 0
⊢ -(↑π ^ 2 * ↑‖x - w‖ ^ 2) / b = (2 * ↑π * I) ^ 2 * ↑‖x - w‖ ^ 2 / (4 * b)

Tactic:
field_simp [mul_pow]

Result:
case h.e'_3.h.e'_6.h.e'_1
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
x w : V
this : b ≠ 0
⊢ ↑π ^ 2 * ↑‖x - w‖ ^ 2 * (4 * b) = 2 ^ 2 * ↑π ^ 2 * ↑‖x - w‖ ^ 2 * b

Proof state:
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
x w : V
⊢ b ≠ 0

Tactic:
contrapose! hb

Result:
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
x w : V
hb : b = 0
⊢ b.re ≤ 0