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

Proof state:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Tendsto (fun i => ∫ (x : ℝ) in -i..id i, cexp (-b * (↑x + ↑c * I) ^ 2)) atTop (𝓝 ((↑π / b) ^ (1 / 2)))

Tactic:
set I₁ := fun T => ∫ x : ℝ in -T..T, cexp (-b * (x + c * I) ^ 2) with HI₁

Result:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : ℝ → ℂ := fun T => ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
HI₁ : I₁ = fun T => ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
⊢ Tendsto (fun i => ∫ (x : ℝ) in -i..id i, cexp (-b * (↑x + ↑c * I) ^ 2)) atTop (𝓝 ((↑π / b) ^ (1 / 2)))

Proof state:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : ℝ → ℂ := fun T => ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
HI₁ : I₁ = fun T => ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
⊢ Tendsto (fun i => ∫ (x : ℝ) in -i..id i, cexp (-b * (↑x + ↑c * I) ^ 2)) atTop (𝓝 ((↑π / b) ^ (1 / 2)))

Tactic:
let I₂ := fun T : ℝ => ∫ x : ℝ in -T..T, cexp (-b * (x : ℂ) ^ 2)

Result:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : ℝ → ℂ := fun T => ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
HI₁ : I₁ = fun T => ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
I₂ : ℝ → ℂ := fun T => ∫ (x : ℝ) in -T..T, cexp (-b * ↑x ^ 2)
⊢ Tendsto (fun i => ∫ (x : ℝ) in -i..id i, cexp (-b * (↑x + ↑c * I) ^ 2)) atTop (𝓝 ((↑π / b) ^ (1 / 2)))

Proof state:
case h.hf
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : ℝ → ℂ := fun T => ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
HI₁ : I₁ = fun T => ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
I₂ : ℝ → ℂ := fun T => ∫ (x : ℝ) in -T..T, cexp (-b * ↑x ^ 2)
I₄ : ℝ → ℂ := fun T => ∫ (y : ℝ) in 0 ..c, cexp (-b * (↑T + ↑y * I) ^ 2)
I₅ : ℝ → ℂ := fun T => ∫ (y : ℝ) in 0 ..c, cexp (-b * (-↑T + ↑y * I) ^ 2)
T : ℝ
C : I₂ T - I₁ T + I * I₄ T = I * I₅ T
⊢ IntervalIntegrable (fun x => cexp (-b * (↑T + ↑x * I) ^ 2)) volume 0 c

case h.hg
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : ℝ → ℂ := fun T => ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
HI₁ : I₁ = fun T => ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
I₂ : ℝ → ℂ := fun T => ∫ (x : ℝ) in -T..T, cexp (-b * ↑x ^ 2)
I₄ : ℝ → ℂ := fun T => ∫ (y : ℝ) in 0 ..c, cexp (-b * (↑T + ↑y * I) ^ 2)
I₅ : ℝ → ℂ := fun T => ∫ (y : ℝ) in 0 ..c, cexp (-b * (-↑T + ↑y * I) ^ 2)
T : ℝ
C : I₂ T - I₁ T + I * I₄ T = I * I₅ T
⊢ IntervalIntegrable (fun x => cexp (-b * (↑T - ↑x * I) ^ 2)) volume 0 c

Tactic:
all_goals apply Continuous.intervalIntegrable; continuity

Result:
no goals

Proof state:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : ℝ → ℂ := fun T => ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
HI₁ : I₁ = fun T => ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
I₂ : ℝ → ℂ := fun T => ∫ (x : ℝ) in -T..T, cexp (-b * ↑x ^ 2)
I₄ : ℝ → ℂ := fun T => ∫ (y : ℝ) in 0 ..c, cexp (-b * (↑T + ↑y * I) ^ 2)
I₅ : ℝ → ℂ := fun T => ∫ (y : ℝ) in 0 ..c, cexp (-b * (-↑T + ↑y * I) ^ 2)
C : ∀ (T : ℝ), I₂ T - I₁ T + I * I₄ T - I * I₅ T = 0
this : I₁ = fun T => I₂ T + verticalIntegral b c T
⊢ Tendsto I₂ atTop (𝓝 (∫ (x : ℝ), cexp (-b * ↑x ^ 2)))

Tactic:
exact
  intervalIntegral_tendsto_integral (integrable_cexp_neg_mul_sq hb) tendsto_neg_atTop_atBot
    tendsto_id

Result:
no goals

Proof state:
case h
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : ℝ → ℂ := fun T => ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
HI₁ : I₁ = fun T => ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
I₂ : ℝ → ℂ := fun T => ∫ (x : ℝ) in -T..T, cexp (-b * ↑x ^ 2)
I₄ : ℝ → ℂ := fun T => ∫ (y : ℝ) in 0 ..c, cexp (-b * (↑T + ↑y * I) ^ 2)
I₅ : ℝ → ℂ := fun T => ∫ (y : ℝ) in 0 ..c, cexp (-b * (-↑T + ↑y * I) ^ 2)
C : ∀ (T : ℝ), I₂ T - I₁ T + I * I₄ T - I * I₅ T = 0
T : ℝ
⊢ I₁ T = I₂ T + verticalIntegral b c T

Tactic:
specialize C T

Result:
case h
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : ℝ → ℂ := fun T => ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
HI₁ : I₁ = fun T => ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
I₂ : ℝ → ℂ := fun T => ∫ (x : ℝ) in -T..T, cexp (-b * ↑x ^ 2)
I₄ : ℝ → ℂ := fun T => ∫ (y : ℝ) in 0 ..c, cexp (-b * (↑T + ↑y * I) ^ 2)
I₅ : ℝ → ℂ := fun T => ∫ (y : ℝ) in 0 ..c, cexp (-b * (-↑T + ↑y * I) ^ 2)
T : ℝ
C : I₂ T - I₁ T + I * I₄ T - I * I₅ T = 0
⊢ I₁ T = I₂ T + verticalIntegral b c T

Proof state:
case h
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : ℝ → ℂ := fun T => ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
HI₁ : I₁ = fun T => ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
I₂ : ℝ → ℂ := fun T => ∫ (x : ℝ) in -T..T, cexp (-b * ↑x ^ 2)
I₄ : ℝ → ℂ := fun T => ∫ (y : ℝ) in 0 ..c, cexp (-b * (↑T + ↑y * I) ^ 2)
I₅ : ℝ → ℂ := fun T => ∫ (y : ℝ) in 0 ..c, cexp (-b * (-↑T + ↑y * I) ^ 2)
T : ℝ
C : I₂ T - I₁ T + I * I₄ T = I * I₅ T
⊢ I₁ T = I₂ T + ∫ (y : ℝ) in 0 ..c, I * (cexp (-b * (↑T + ↑y * I) ^ 2) - cexp (-b * (↑T - ↑y * I) ^ 2))

Tactic:
rw [integral_const_mul, intervalIntegral.integral_sub]

Result:
case h
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : ℝ → ℂ := fun T => ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
HI₁ : I₁ = fun T => ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
I₂ : ℝ → ℂ := fun T => ∫ (x : ℝ) in -T..T, cexp (-b * ↑x ^ 2)
I₄ : ℝ → ℂ := fun T => ∫ (y : ℝ) in 0 ..c, cexp (-b * (↑T + ↑y * I) ^ 2)
I₅ : ℝ → ℂ := fun T => ∫ (y : ℝ) in 0 ..c, cexp (-b * (-↑T + ↑y * I) ^ 2)
T : ℝ
C : I₂ T - I₁ T + I * I₄ T = I * I₅ T
⊢ I₁ T =
    I₂ T + I * ((∫ (x : ℝ) in 0 ..c, cexp (-b * (↑T + ↑x * I) ^ 2)) - ∫ (x : ℝ) in 0 ..c, cexp (-b * (↑T - ↑x * I) ^ 2))

case h.hf
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : ℝ → ℂ := fun T => ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
HI₁ : I₁ = fun T => ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
I₂ : ℝ → ℂ := fun T => ∫ (x : ℝ) in -T..T, cexp (-b * ↑x ^ 2)
I₄ : ℝ → ℂ := fun T => ∫ (y : ℝ) in 0 ..c, cexp (-b * (↑T + ↑y * I) ^ 2)
I₅ : ℝ → ℂ := fun T => ∫ (y : ℝ) in 0 ..c, cexp (-b * (-↑T + ↑y * I) ^ 2)
T : ℝ
C : I₂ T - I₁ T + I * I₄ T = I * I₅ T
⊢ IntervalIntegrable (fun x => cexp (-b * (↑T + ↑x * I) ^ 2)) volume 0 c

case h.hg
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : ℝ → ℂ := fun T => ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
HI₁ : I₁ = fun T => ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
I₂ : ℝ → ℂ := fun T => ∫ (x : ℝ) in -T..T, cexp (-b * ↑x ^ 2)
I₄ : ℝ → ℂ := fun T => ∫ (y : ℝ) in 0 ..c, cexp (-b * (↑T + ↑y * I) ^ 2)
I₅ : ℝ → ℂ := fun T => ∫ (y : ℝ) in 0 ..c, cexp (-b * (-↑T + ↑y * I) ^ 2)
T : ℝ
C : I₂ T - I₁ T + I * I₄ T = I * I₅ T
⊢ IntervalIntegrable (fun x => cexp (-b * (↑T - ↑x * I) ^ 2)) volume 0 c

Proof state:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : ℝ → ℂ := fun T => ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
HI₁ : I₁ = fun T => ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
I₂ : ℝ → ℂ := fun T => ∫ (x : ℝ) in -T..T, cexp (-b * ↑x ^ 2)
I₄ : ℝ → ℂ := fun T => ∫ (y : ℝ) in 0 ..c, cexp (-b * (↑T + ↑y * I) ^ 2)
I₅ : ℝ → ℂ := fun T => ∫ (y : ℝ) in 0 ..c, cexp (-b * (-↑T + ↑y * I) ^ 2)
T : ℝ
⊢ Differentiable ℂ fun z => z ^ 2

Tactic:
exact differentiable_pow 2

Result:
no goals