-- Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean
theorem _root_.integral_cexp_quadratic (hb : b.re < 0) (c d : ℂ) :
    ∫ x : ℝ, cexp (b * x ^ 2 + c * x + d) = (π / -b) ^ (1 / 2 : ℂ) * cexp (d - c^2 / (4 * b))

Proof state:
case e_z
b : ℂ
hb : b.re < 0
c d : ℂ
hb' : b ≠ 0
x : ℝ
⊢ (b * ↑x ^ 2 + c * ↑x + d) * ((2 * b) ^ 2 * (4 * b)) =
    b * (↑x * (2 * b) + c) ^ 2 * (4 * b) + (d * (4 * b) - c ^ 2) * (2 * b) ^ 2

Tactic:
ring_nf

Result:
no goals

Proof state:
b : ℂ
hb : b.re < 0
c d : ℂ
hb' : b ≠ 0
h : ∀ (x : ℝ), cexp (b * ↑x ^ 2 + c * ↑x + d) = cexp (- -b * (↑x + c / (2 * b)) ^ 2) * cexp (d - c ^ 2 / (4 * b))
⊢ (∫ (a : ℝ), cexp (- -b * (↑a + c / (2 * b)) ^ 2)) * cexp (d - c ^ 2 / (4 * b)) =
    (↑π / -b) ^ (1 / 2) * cexp (d - c ^ 2 / (4 * b))

Tactic:
rw [← re_add_im (c / (2 * b))]

Result:
b : ℂ
hb : b.re < 0
c d : ℂ
hb' : b ≠ 0
h : ∀ (x : ℝ), cexp (b * ↑x ^ 2 + c * ↑x + d) = cexp (- -b * (↑x + c / (2 * b)) ^ 2) * cexp (d - c ^ 2 / (4 * b))
⊢ (∫ (a : ℝ), cexp (- -b * (↑a + (↑(c / (2 * b)).re + ↑(c / (2 * b)).im * I)) ^ 2)) * cexp (d - c ^ 2 / (4 * b)) =
    (↑π / -b) ^ (1 / 2) * cexp (d - c ^ 2 / (4 * b))

Proof state:
case e_z
b : ℂ
hb : b.re < 0
c d : ℂ
hb' : b ≠ 0
x : ℝ
⊢ b * ↑x ^ 2 + c * ↑x + d = - -b * (↑x + c / (2 * b)) ^ 2 + (d - c ^ 2 / (4 * b))

Tactic:
field_simp

Result:
case e_z
b : ℂ
hb : b.re < 0
c d : ℂ
hb' : b ≠ 0
x : ℝ
⊢ (b * ↑x ^ 2 + c * ↑x + d) * ((2 * b) ^ 2 * (4 * b)) =
    b * (↑x * (2 * b) + c) ^ 2 * (4 * b) + (d * (4 * b) - c ^ 2) * (2 * b) ^ 2

Proof state:
b : ℂ
hb : b.re < 0
c d : ℂ
⊢ b ≠ 0

Tactic:
contrapose! hb

Result:
b c d : ℂ
hb : b = 0
⊢ 0 ≤ b.re

Proof state:
b : ℂ
hb : b.re < 0
c d : ℂ
hb' : b ≠ 0
h : ∀ (x : ℝ), cexp (b * ↑x ^ 2 + c * ↑x + d) = cexp (- -b * (↑x + c / (2 * b)) ^ 2) * cexp (d - c ^ 2 / (4 * b))
⊢ (∫ (a : ℝ), cexp (- -b * (↑a + (↑(c / (2 * b)).re + ↑(c / (2 * b)).im * I)) ^ 2)) * cexp (d - c ^ 2 / (4 * b)) =
    (↑π / -b) ^ (1 / 2) * cexp (d - c ^ 2 / (4 * b))

Tactic:
simp_rw [← add_assoc, ← ofReal_add]

Result:
b : ℂ
hb : b.re < 0
c d : ℂ
hb' : b ≠ 0
h : ∀ (x : ℝ), cexp (b * ↑x ^ 2 + c * ↑x + d) = cexp (- -b * (↑x + c / (2 * b)) ^ 2) * cexp (d - c ^ 2 / (4 * b))
⊢ (∫ (a : ℝ), cexp (- -b * (↑(a + (c / (2 * b)).re) + ↑(c / (2 * b)).im * I) ^ 2)) * cexp (d - c ^ 2 / (4 * b)) =
    (↑π / -b) ^ (1 / 2) * cexp (d - c ^ 2 / (4 * b))

Proof state:
b : ℂ
hb : b.re < 0
c d : ℂ
hb' : b ≠ 0
h : ∀ (x : ℝ), cexp (b * ↑x ^ 2 + c * ↑x + d) = cexp (- -b * (↑x + c / (2 * b)) ^ 2) * cexp (d - c ^ 2 / (4 * b))
⊢ (∫ (a : ℝ), cexp (- -b * (↑(a + (c / (2 * b)).re) + ↑(c / (2 * b)).im * I) ^ 2)) * cexp (d - c ^ 2 / (4 * b)) =
    (↑π / -b) ^ (1 / 2) * cexp (d - c ^ 2 / (4 * b))

Tactic:
rw [integral_add_right_eq_self fun a : ℝ ↦ cexp (- -b * (↑a + ↑(c / (2 * b)).im * I) ^ 2),
  integral_cexp_neg_mul_sq_add_real_mul_I ((neg_re b).symm ▸ (neg_pos.mpr hb))]

Result:
no goals

Proof state:
b : ℂ
hb : b.re < 0
c d : ℂ
⊢ ∫ (x : ℝ), cexp (b * ↑x ^ 2 + c * ↑x + d) = (↑π / -b) ^ (1 / 2) * cexp (d - c ^ 2 / (4 * b))

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

Result:
b : ℂ
hb : b.re < 0
c d : ℂ
hb' : b ≠ 0
⊢ ∫ (x : ℝ), cexp (b * ↑x ^ 2 + c * ↑x + d) = (↑π / -b) ^ (1 / 2) * cexp (d - c ^ 2 / (4 * b))

Proof state:
b : ℂ
hb : b.re < 0
c d : ℂ
hb' : b ≠ 0
h : ∀ (x : ℝ), cexp (b * ↑x ^ 2 + c * ↑x + d) = cexp (- -b * (↑x + c / (2 * b)) ^ 2) * cexp (d - c ^ 2 / (4 * b))
⊢ ∫ (x : ℝ), cexp (b * ↑x ^ 2 + c * ↑x + d) = (↑π / -b) ^ (1 / 2) * cexp (d - c ^ 2 / (4 * b))

Tactic:
simp_rw [h, integral_mul_right]

Result:
b : ℂ
hb : b.re < 0
c d : ℂ
hb' : b ≠ 0
h : ∀ (x : ℝ), cexp (b * ↑x ^ 2 + c * ↑x + d) = cexp (- -b * (↑x + c / (2 * b)) ^ 2) * cexp (d - c ^ 2 / (4 * b))
⊢ (∫ (a : ℝ), cexp (- -b * (↑a + c / (2 * b)) ^ 2)) * cexp (d - c ^ 2 / (4 * b)) =
    (↑π / -b) ^ (1 / 2) * cexp (d - c ^ 2 / (4 * b))

Proof state:
b : ℂ
hb : b.re < 0
c d : ℂ
hb' : b ≠ 0
⊢ ∫ (x : ℝ), cexp (b * ↑x ^ 2 + c * ↑x + d) = (↑π / -b) ^ (1 / 2) * cexp (d - c ^ 2 / (4 * b))

Tactic:
have h (x : ℝ) : cexp (b * x ^ 2 + c * x + d) =
    cexp (- -b * (x + c / (2 * b)) ^ 2) * cexp (d - c ^ 2 / (4 * b)) := by
  simp_rw [← Complex.exp_add]
  congr 1
  field_simp
  ring_nf

Result:
b : ℂ
hb : b.re < 0
c d : ℂ
hb' : b ≠ 0
h : ∀ (x : ℝ), cexp (b * ↑x ^ 2 + c * ↑x + d) = cexp (- -b * (↑x + c / (2 * b)) ^ 2) * cexp (d - c ^ 2 / (4 * b))
⊢ ∫ (x : ℝ), cexp (b * ↑x ^ 2 + c * ↑x + d) = (↑π / -b) ^ (1 / 2) * cexp (d - c ^ 2 / (4 * b))

Proof state:
b c d : ℂ
hb : b = 0
⊢ 0 ≤ b.re

Tactic:
rw [hb, zero_re]

Result:
no goals

Proof state:
b : ℂ
hb : b.re < 0
c d : ℂ
hb' : b ≠ 0
x : ℝ
⊢ cexp (b * ↑x ^ 2 + c * ↑x + d) = cexp (- -b * (↑x + c / (2 * b)) ^ 2) * cexp (d - c ^ 2 / (4 * b))

Tactic:
simp_rw [← Complex.exp_add]

Result:
b : ℂ
hb : b.re < 0
c d : ℂ
hb' : b ≠ 0
x : ℝ
⊢ cexp (b * ↑x ^ 2 + c * ↑x + d) = cexp (- -b * (↑x + c / (2 * b)) ^ 2 + (d - c ^ 2 / (4 * b)))

Proof state:
b : ℂ
hb : b.re < 0
c d : ℂ
hb' : b ≠ 0
x : ℝ
⊢ cexp (b * ↑x ^ 2 + c * ↑x + d) = cexp (- -b * (↑x + c / (2 * b)) ^ 2 + (d - c ^ 2 / (4 * b)))

Tactic:
congr 1

Result:
case e_z
b : ℂ
hb : b.re < 0
c d : ℂ
hb' : b ≠ 0
x : ℝ
⊢ b * ↑x ^ 2 + c * ↑x + d = - -b * (↑x + c / (2 * b)) ^ 2 + (d - c ^ 2 / (4 * b))