awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
HI₁ : I₁ = fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
I₂ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
I₄ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)
I₅ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (-(↑T : ℂ) + (↑y : ℂ) * I) 2)
C : ∀ (T : ℝ), I₂ T - I₁ T + I * I₄ T - I * I₅ T = 0
T : ℝ
⊢ I₂ T - I₁ T + I * I₄ T - I * I₅ T = 0

Tactic:
specialize C T
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
HI₁ : I₁ = fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
I₂ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
I₄ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)
I₅ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (-(↑T : ℂ) + (↑y : ℂ) * I) 2)
T : ℝ
C : I₂ T - I₁ T + I * I₄ T - I * I₅ T = 0
⊢ I₂ T - I₁ T + I * I₄ T = I * I₅ T

Tactic:
rw [sub_eq_zero] at C

Premises used: sub_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
HI₁ : I₁ = fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
I₂ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
I₄ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)
I₅ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (-(↑T : ℂ) + (↑y : ℂ) * I) 2)
T : ℝ
C : I₂ T - I₁ T + I * I₄ T = I * I₅ T
h :
  I₁ T =
    I₂ T +
      I *
        HSub.hSub (α := ℂ) (∫ (x : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑x : ℂ) * I) 2))
          (∫ (x : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) - (↑x : ℂ) * I) 2))
h₁ : IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑x : ℂ) * I) 2)) volume 0 c
h₂ : IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) - (↑x : ℂ) * I) 2)) volume 0 c
⊢ I₁ T =
    I₂ T +
      ∫ (y : ℝ) in 0..c,
        I *
          (cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2) -
            cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) - (↑y : ℂ) * I) 2))

Tactic:
rw [intervalIntegral.integral_const_mul, intervalIntegral.integral_sub]

Premises used: intervalIntegral.integral_sub, intervalIntegral.integral_const_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b_1 : ℂ
hb : 0 < b_1.re
c : ℝ
I₁ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b_1 * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
HI₁ : I₁ = fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b_1 * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
I₂ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b_1 * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
I₄ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b_1 * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)
I₅ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b_1 * HPow.hPow (β := ℕ) (-(↑T : ℂ) + (↑y : ℂ) * I) 2)
T : ℝ
C : I₂ T - I₁ T + I * I₄ T = I * I₅ T
a b : ℂ
rw : (a - b * I) * (a - b * I) = HPow.hPow (β := ℕ) (-a + b * I) 2
⊢ HPow.hPow (β := ℕ) (a - b * I) 2 = HPow.hPow (β := ℕ) (-a + b * I) 2

Tactic:
rw [sq]

Premises used: sq
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b_1 : ℂ
hb : 0 < b_1.re
c : ℝ
I₁ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b_1 * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
HI₁ : I₁ = fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b_1 * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
I₂ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b_1 * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
I₄ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b_1 * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)
I₅ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b_1 * HPow.hPow (β := ℕ) (-(↑T : ℂ) + (↑y : ℂ) * I) 2)
T : ℝ
C : I₂ T - I₁ T + I * I₄ T = I * I₅ T
a b : ℂ
⊢ (a - b * I) * (a - b * I) = HPow.hPow (β := ℕ) (-a + b * I) 2

Tactic:
ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
HI₁ : I₁ = fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
I₂ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
I₄ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)
I₅ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (-(↑T : ℂ) + (↑y : ℂ) * I) 2)
T : ℝ
C : I₂ T - I₁ T + I * I₄ T = I * I₅ T
h :
  I₁ T =
    I₂ T +
      I *
        HSub.hSub (α := ℂ) (∫ (x : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑x : ℂ) * I) 2))
          (∫ (x : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (-(↑T : ℂ) + (↑x : ℂ) * I) 2))
⊢ I₁ T =
    I₂ T +
      I *
        HSub.hSub (α := ℂ) (∫ (x : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑x : ℂ) * I) 2))
          (∫ (x : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) - (↑x : ℂ) * I) 2))

Tactic:
simp_rw [(fun a b => by rw [sq]; ring_nf : ∀ a b : ℂ, (a - b * I) ^ 2 = (-a + b * I) ^ 2)]
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
HI₁ : I₁ = fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
I₂ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
I₄ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)
I₅ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (-(↑T : ℂ) + (↑y : ℂ) * I) 2)
T : ℝ
C : I₂ T - I₁ T + I * I₄ T = I * I₅ T
h : I₁ T = I₂ T + I * (I₄ T - I₅ T)
⊢ I₁ T =
    I₂ T +
      I *
        HSub.hSub (α := ℂ) (∫ (x : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑x : ℂ) * I) 2))
          (∫ (x : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (-(↑T : ℂ) + (↑x : ℂ) * I) 2))

Tactic:
change I₁ T = I₂ T + I * (I₄ T - I₅ T)

Premises used: HSub.hSub, Complex.I
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
HI₁ : I₁ = fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
I₂ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
I₄ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)
I₅ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (-(↑T : ℂ) + (↑y : ℂ) * I) 2)
T : ℝ
C : I₂ T - I₁ T + I * I₄ T = I * I₅ T
h : I₁ T = I₂ T + (I * I₄ T - (I₂ T - I₁ T + I * I₄ T))
⊢ I₁ T = I₂ T + I * (I₄ T - I₅ T)

Tactic:
rw [mul_sub, ← C]

Premises used: mul_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
HI₁ : I₁ = fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
I₂ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
I₄ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)
I₅ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (-(↑T : ℂ) + (↑y : ℂ) * I) 2)
T : ℝ
C : I₂ T - I₁ T + I * I₄ T = I * I₅ T
⊢ I₁ T = I₂ T + (I * I₄ T - (I₂ T - I₁ T + I * I₄ T))

Tactic:
abel
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
HI₁ : I₁ = fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
I₂ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
I₄ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)
I₅ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (-(↑T : ℂ) + (↑y : ℂ) * I) 2)
T : ℝ
C : I₂ T - I₁ T + I * I₄ T = I * I₅ T
h : Continuous (Y := ℂ) fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑x : ℂ) * I) 2)
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑x : ℂ) * I) 2)) volume 0 c

Tactic:
apply Continuous.intervalIntegrable

Premises used: Continuous.intervalIntegrable
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
HI₁ : I₁ = fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
I₂ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
I₄ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)
I₅ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (-(↑T : ℂ) + (↑y : ℂ) * I) 2)
T : ℝ
C : I₂ T - I₁ T + I * I₄ T = I * I₅ T
⊢ Continuous (Y := ℂ) fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑x : ℂ) * I) 2)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
HI₁ : I₁ = fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
I₂ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
I₄ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)
I₅ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (-(↑T : ℂ) + (↑y : ℂ) * I) 2)
T : ℝ
C : I₂ T - I₁ T + I * I₄ T = I * I₅ T
h : Continuous (Y := ℂ) fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) - (↑x : ℂ) * I) 2)
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) - (↑x : ℂ) * I) 2)) volume 0 c

Tactic:
apply Continuous.intervalIntegrable

Premises used: Continuous.intervalIntegrable
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
HI₁ : I₁ = fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
I₂ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
I₄ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)
I₅ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (-(↑T : ℂ) + (↑y : ℂ) * I) 2)
T : ℝ
C : I₂ T - I₁ T + I * I₄ T = I * I₅ T
⊢ Continuous (Y := ℂ) fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) - (↑x : ℂ) * I) 2)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
HI₁ : I₁ = fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
I₂ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
I₄ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)
I₅ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (-(↑T : ℂ) + (↑y : ℂ) * I) 2)
C : ∀ (T : ℝ), I₂ T - I₁ T + I * I₄ T - I * I₅ T = 0
⊢ I₁ = fun (T : ℝ) ↦ I₂ T + verticalIntegral b c T

Tactic:
have : I₁ = fun T : ℝ => I₂ T + verticalIntegral b c T := by
    ext1 T
    specialize C T
    rw [sub_eq_zero] at C
    unfold verticalIntegral
    rw [intervalIntegral.integral_const_mul, intervalIntegral.integral_sub]
    · simp_rw [(fun a b => by rw [sq]; ring_nf : ∀ a b : ℂ, (a - b * I) ^ 2 = (-a + b * I) ^ 2)]
      change I₁ T = I₂ T + I * (I₄ T - I₅ T)
      rw [mul_sub, ← C]
      abel
    all_goals apply Continuous.intervalIntegrable; fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
HI₁ : I₁ = fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
I₂ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
I₄ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)
I₅ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (-(↑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
rw :
  Tendsto (fun (T : ℝ) ↦ I₂ T + verticalIntegral b c T) atTop
    (𝓝
      (HAdd.hAdd (α := ℂ)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
          cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
        0))
⊢ Tendsto I₁ atTop (𝓝 (((↑π : ℂ) / b) ^ (1 / 2)))

Tactic:
rw [this, ← add_zero ((π / b : ℂ) ^ (1 / 2 : ℂ)), ← integral_gaussian_complex hb]

Premises used: Real.pi, HDiv.hDiv, Complex.ofReal, HPow.hPow, integral_gaussian_complex, add_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
HI₁ : I₁ = fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
I₂ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
I₄ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)
I₅ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (-(↑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 (fun (T : ℝ) ↦ I₂ T + verticalIntegral b c T) atTop
    (𝓝
      (HAdd.hAdd (α := ℂ)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
          cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
        0))

Tactic:
Tendsto.add ?_ (tendsto_verticalIntegral hb c)

Premises used: GaussianFourier.tendsto_verticalIntegral, Filter.Tendsto.add
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
HI₁ : I₁ = fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
I₂ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
I₄ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)
I₅ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (-(↑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
refine :
  Tendsto I₂ atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)))
⊢ Tendsto (fun (T : ℝ) ↦ I₂ T + verticalIntegral b c T) atTop
    (𝓝
      (HAdd.hAdd (α := ℂ)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
          cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
        0))

Tactic:
refine Tendsto.add ?_ (tendsto_verticalIntegral hb c)

Premises used: GaussianFourier.tendsto_verticalIntegral, Filter.Tendsto.add
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
HI₁ : I₁ = fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
I₂ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
I₄ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)
I₅ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (-(↑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
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)))

Tactic:
intervalIntegral_tendsto_integral (integrable_cexp_neg_mul_sq hb) tendsto_neg_atTop_atBot
      tendsto_id

Premises used: Filter.tendsto_id, Filter.tendsto_neg_atTop_atBot, MeasureTheory.intervalIntegral_tendsto_integral, integrable_cexp_neg_mul_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
HI₁ : I₁ = fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
I₂ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
I₄ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)
I₅ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (-(↑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
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)))

Tactic:
exact
    intervalIntegral_tendsto_integral (integrable_cexp_neg_mul_sq hb) tendsto_neg_atTop_atBot
      tendsto_id

Premises used: Filter.tendsto_id, Filter.tendsto_neg_atTop_atBot, MeasureTheory.intervalIntegral_tendsto_integral, integrable_cexp_neg_mul_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : b.re < 0
c d : ℂ
contrapose! : ∀ (hb : b = 0), 0 ≤ b.re
⊢ b ≠ 0

Tactic:
contrapose! hb
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b c d : ℂ
hb : b = 0
rw : 0 ≤ re 0
rw₁ rw₂ : LE.le (α := ℝ) 0 0
⊢ 0 ≤ b.re

Tactic:
rw [hb, zero_re]

Premises used: Complex.zero_re
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : b.re < 0
c d : ℂ
⊢ b ≠ 0

Tactic:
have hb' : b ≠ 0 := by contrapose! hb; rw [hb, zero_re]
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : b.re < 0
c d : ℂ
hb' : b ≠ 0
x : ℝ
simp_rw :
  cexp (b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c * (↑x : ℂ) + d) =
    cexp (- -b * HPow.hPow (β := ℕ) ((↑x : ℂ) + c / (2 * b)) 2 + (d - HPow.hPow (β := ℕ) c 2 / (4 * b)))
⊢ cexp (b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c * (↑x : ℂ) + d) =
    cexp (- -b * HPow.hPow (β := ℕ) ((↑x : ℂ) + c / (2 * b)) 2) * cexp (d - HPow.hPow (β := ℕ) c 2 / (4 * b))

Tactic:
simp_rw [← Complex.exp_add]

Premises used: Complex.exp_add
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : b.re < 0
c d : ℂ
hb' : b ≠ 0
x : ℝ
e_z :
  b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c * (↑x : ℂ) + d =
    - -b * HPow.hPow (β := ℕ) ((↑x : ℂ) + c / (2 * b)) 2 + (d - HPow.hPow (β := ℕ) c 2 / (4 * b))
⊢ cexp (b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c * (↑x : ℂ) + d) =
    cexp (- -b * HPow.hPow (β := ℕ) ((↑x : ℂ) + c / (2 * b)) 2 + (d - HPow.hPow (β := ℕ) c 2 / (4 * b)))

Tactic:
congr 1
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : b.re < 0
c d : ℂ
hb' : b ≠ 0
x : ℝ
⊢ b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c * (↑x : ℂ) + d =
    - -b * HPow.hPow (β := ℕ) ((↑x : ℂ) + c / (2 * b)) 2 + (d - HPow.hPow (β := ℕ) c 2 / (4 * b))

Tactic:
field
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : b.re < 0
c d : ℂ
hb' : b ≠ 0
⊢ ∀ (x : ℝ),
    cexp (b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c * (↑x : ℂ) + d) =
      cexp (- -b * HPow.hPow (β := ℕ) ((↑x : ℂ) + c / (2 * b)) 2) * cexp (d - HPow.hPow (β := ℕ) 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
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : b.re < 0
c d : ℂ
hb' : b ≠ 0
h :
  ∀ (x : ℝ),
    cexp (b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c * (↑x : ℂ) + d) =
      cexp (- -b * HPow.hPow (β := ℕ) ((↑x : ℂ) + c / (2 * b)) 2) * cexp (d - HPow.hPow (β := ℕ) c 2 / (4 * b))
simp_rw :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : ℝ) ↦
        cexp (- -b * HPow.hPow (β := ℕ) ((↑a : ℂ) + c / (2 * b)) 2)) *
      cexp (d - HPow.hPow (β := ℕ) c 2 / (4 * b)) =
    ((↑π : ℂ) / -b) ^ (1 / 2) * cexp (d - HPow.hPow (β := ℕ) c 2 / (4 * b))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
      cexp (b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c * (↑x : ℂ) + d)) =
    ((↑π : ℂ) / -b) ^ (1 / 2) * cexp (d - HPow.hPow (β := ℕ) c 2 / (4 * b))

Tactic:
simp_rw [h, MeasureTheory.integral_mul_const]

Premises used: MeasureTheory.integral_mul_const
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : b.re < 0
c d : ℂ
hb' : b ≠ 0
h :
  ∀ (x : ℝ),
    cexp (b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c * (↑x : ℂ) + d) =
      cexp (- -b * HPow.hPow (β := ℕ) ((↑x : ℂ) + c / (2 * b)) 2) * cexp (d - HPow.hPow (β := ℕ) c 2 / (4 * b))
rw :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : ℝ) ↦
        cexp (- -b * HPow.hPow (β := ℕ) ((↑a : ℂ) + ((↑(c / (2 * b)).re : ℂ) + (↑(c / (2 * b)).im : ℂ) * I)) 2)) *
      cexp (d - HPow.hPow (β := ℕ) c 2 / (4 * b)) =
    ((↑π : ℂ) / -b) ^ (1 / 2) * cexp (d - HPow.hPow (β := ℕ) c 2 / (4 * b))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : ℝ) ↦
        cexp (- -b * HPow.hPow (β := ℕ) ((↑a : ℂ) + c / (2 * b)) 2)) *
      cexp (d - HPow.hPow (β := ℕ) c 2 / (4 * b)) =
    ((↑π : ℂ) / -b) ^ (1 / 2) * cexp (d - HPow.hPow (β := ℕ) c 2 / (4 * b))

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

Premises used: HMul.hMul, HDiv.hDiv, Complex.re_add_im, OfNat.ofNat