awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)).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)).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))

Tactic:
simp_rw [← add_assoc, ← ofReal_add]

Premises used: add_assoc, Complex.ofReal_add
-- 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 _ _ _ _ Real.measurableSpace volume fun (x : ℝ) ↦
        cexp (- -b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑(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))
rw₁ rw₂ :
  ((↑π : ℂ) / -b) ^ (1 / 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)).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))

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))]

Premises used: HMul.hMul, MeasureTheory.integral_add_right_eq_self, HPow.hPow, HAdd.hAdd, GaussianFourier.integral_cexp_neg_mul_sq_add_real_mul_I, Complex.exp, OfNat.ofNat, Neg.neg, Complex.I
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : b.re < 0
c d : ℂ
hb' : b ≠ 0
by_contra :
  ∀
    (H :
      ¬@Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace
          (fun (x : ℝ) ↦ cexp (b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c * (↑x : ℂ) + d)) volume),
    False
⊢ @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ cexp (b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c * (↑x : ℂ) + d)) volume

Tactic:
by_contra H
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : b.re < 0
c d : ℂ
hb' : b ≠ 0
H :
  ¬@Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace
      (fun (x : ℝ) ↦ cexp (b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c * (↑x : ℂ) + d)) volume
⊢ False

Tactic:
simpa [hb', pi_ne_zero, Complex.exp_ne_zero, integral_undef H]
    using integral_cexp_quadratic hb c d

Premises used: Complex.exp_ne_zero, MeasureTheory.integral_undef, integral_cexp_quadratic, Real.pi_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c d : ℂ
⊢ (-b).re < 0

Tactic:
simpa using hb
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c d : ℂ
⊢ (-b).re < 0

Tactic:
have : (-b).re < 0 := by simpa using hb
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c d : ℂ
this : (-b).re < 0
⊢ @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c * (↑x : ℂ) + d)) volume

Tactic:
integrable_cexp_quadratic' this c d

Premises used: integrable_cexp_quadratic'
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c d : ℂ
this : (-b).re < 0
⊢ @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c * (↑x : ℂ) + d)) volume

Tactic:
exact integrable_cexp_quadratic' this c d

Premises used: integrable_cexp_quadratic'
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
t : ℂ
h : ∀ (x : ℝ), cexp (I * t * (↑x : ℂ)) * cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
| (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
      cexp (I * t * (↑x : ℂ)) * cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / b) ^ (1 / 2) * cexp (-HPow.hPow (β := ℕ) t 2 / (4 * b))

Tactic:
enter [1, 2, x]
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
t : ℂ
x : ℝ
h : cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + I * t * (↑x : ℂ) + 0)
| cexp (I * t * (↑x : ℂ)) * cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)

Tactic:
rw [← Complex.exp_add, add_comm, ← add_zero (-b * x ^ 2 + I * t * x)]

Premises used: HMul.hMul, Complex.exp_add, Complex.ofReal, add_comm, HPow.hPow, HAdd.hAdd, add_zero, OfNat.ofNat, Neg.neg, Complex.I
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
t : ℂ
h : ∀ (x : ℝ), cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + I * t * (↑x : ℂ) + 0)
| (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
      cexp (I * t * (↑x : ℂ)) * cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / b) ^ (1 / 2) * cexp (-HPow.hPow (β := ℕ) t 2 / (4 * b))

Tactic:
enter [1, 2, x]; rw [← Complex.exp_add, add_comm, ← add_zero (-b * x ^ 2 + I * t * x)]

Premises used: Complex.exp_add, add_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
t : ℂ
conv :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + I * t * (↑x : ℂ) + 0)) =
    ((↑π : ℂ) / b) ^ (1 / 2) * cexp (-HPow.hPow (β := ℕ) t 2 / (4 * b))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
      cexp (I * t * (↑x : ℂ)) * cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / b) ^ (1 / 2) * cexp (-HPow.hPow (β := ℕ) t 2 / (4 * b))

Tactic:
conv => enter [1, 2, x]; rw [← Complex.exp_add, add_comm, ← add_zero (-b * x ^ 2 + I * t * x)]

Premises used: Complex.exp_add, add_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
t : ℂ
rwa : -b.re < 0
rwa₁ rwa₂ rwa₃ rwa₄ : 0 < b.re
⊢ (-b).re < 0

Tactic:
rwa [neg_re, neg_lt_zero]

Premises used: neg_lt_zero, Complex.neg_re
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
t : ℂ
rw :
  ((↑π : ℂ) / - -b) ^ (1 / 2) * cexp (0 - HPow.hPow (β := ℕ) (I * t) 2 / (4 * -b)) =
    ((↑π : ℂ) / b) ^ (1 / 2) * cexp (-HPow.hPow (β := ℕ) t 2 / (4 * b))
rw₁ :
  ((↑π : ℂ) / b) ^ (1 / 2) * cexp (0 - HPow.hPow (β := ℕ) (I * t) 2 / (4 * -b)) =
    ((↑π : ℂ) / b) ^ (1 / 2) * cexp (-HPow.hPow (β := ℕ) t 2 / (4 * b))
rw₂ :
  ((↑π : ℂ) / b) ^ (1 / 2) * cexp (-(HPow.hPow (β := ℕ) (I * t) 2 / (4 * -b))) =
    ((↑π : ℂ) / b) ^ (1 / 2) * cexp (-HPow.hPow (β := ℕ) t 2 / (4 * b))
rw₃ :
  ((↑π : ℂ) / b) ^ (1 / 2) * cexp (-(HPow.hPow (β := ℕ) (I * t) 2 / -(4 * b))) =
    ((↑π : ℂ) / b) ^ (1 / 2) * cexp (-HPow.hPow (β := ℕ) t 2 / (4 * b))
rw₄ :
  ((↑π : ℂ) / b) ^ (1 / 2) * cexp (- -(HPow.hPow (β := ℕ) (I * t) 2 / (4 * b))) =
    ((↑π : ℂ) / b) ^ (1 / 2) * cexp (-HPow.hPow (β := ℕ) t 2 / (4 * b))
rw₅ :
  ((↑π : ℂ) / b) ^ (1 / 2) * cexp (HPow.hPow (β := ℕ) (I * t) 2 / (4 * b)) =
    ((↑π : ℂ) / b) ^ (1 / 2) * cexp (-HPow.hPow (β := ℕ) t 2 / (4 * b))
rw₆ :
  ((↑π : ℂ) / b) ^ (1 / 2) * cexp (HPow.hPow (β := ℕ) I 2 * HPow.hPow (β := ℕ) t 2 / (4 * b)) =
    ((↑π : ℂ) / b) ^ (1 / 2) * cexp (-HPow.hPow (β := ℕ) t 2 / (4 * b))
rw₇ :
  ((↑π : ℂ) / b) ^ (1 / 2) * cexp (-1 * HPow.hPow (β := ℕ) t 2 / (4 * b)) =
    ((↑π : ℂ) / b) ^ (1 / 2) * cexp (-HPow.hPow (β := ℕ) t 2 / (4 * b))
rw₈ :
  ((↑π : ℂ) / b) ^ (1 / 2) * cexp (-HPow.hPow (β := ℕ) t 2 / (4 * b)) =
    ((↑π : ℂ) / b) ^ (1 / 2) * cexp (-HPow.hPow (β := ℕ) t 2 / (4 * b))
rw₉ rw₁₀ :
  cexp (-HPow.hPow (β := ℕ) t 2 / (4 * b)) * ((↑π : ℂ) / b) ^ (1 / 2) =
    cexp (-HPow.hPow (β := ℕ) t 2 / (4 * b)) * ((↑π : ℂ) / b) ^ (1 / 2)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + I * t * (↑x : ℂ) + 0)) =
    ((↑π : ℂ) / b) ^ (1 / 2) * cexp (-HPow.hPow (β := ℕ) t 2 / (4 * b))

Tactic:
rw [integral_cexp_quadratic (show (-b).re < 0 by rwa [neg_re, neg_lt_zero]), neg_neg, zero_sub,
    mul_neg, div_neg, neg_neg, mul_pow, I_sq, neg_one_mul, mul_comm]

Premises used: neg_one_mul, neg_neg, integral_cexp_quadratic, div_neg, Complex.I_sq, mul_comm, mul_pow, zero_sub, mul_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℂ
contrapose! : ∀ (hb : b = 0), b.re ≤ 0
⊢ b ≠ 0

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

Tactic:
rw [hb, zero_re]

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

Tactic:
haveI : b ≠ 0 := by contrapose! hb; rw [hb, zero_re]
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℂ
this : b ≠ 0
⊢ (-(↑π : ℂ) * b).re < 0

Tactic:
simpa only [neg_mul, neg_re, re_ofReal_mul, neg_lt_zero] using mul_pos pi_pos hb

Premises used: Real.pi_pos, neg_lt_zero, mul_pos, Complex.neg_re, neg_mul, Complex.re_ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℂ
this : b ≠ 0
⊢ (-(↑π : ℂ) * b).re < 0

Tactic:
have h : (-↑π * b).re < 0 := by
    simpa only [neg_mul, neg_re, re_ofReal_mul, neg_lt_zero] using mul_pos pi_pos hb
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℂ
this : b ≠ 0
h : (-(↑π : ℂ) * b).re < 0
h₁ :
  ∀ (t : ℝ),
    𝓕 (E := (x : ℝ) → ℂ)
        (fun (x : ℝ) ↦ cexp (-(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 2 * (↑π : ℂ) * c * (↑x : ℂ))) t =
      1 / b ^ (1 / 2) * cexp (-(↑π : ℂ) / b * HPow.hPow (β := ℕ) ((↑t : ℂ) + I * c) 2)
⊢ (𝓕 (E := (x : ℝ) → ℂ) fun (x : ℝ) ↦
      cexp (-(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 2 * (↑π : ℂ) * c * (↑x : ℂ))) =
    fun (t : ℝ) ↦ 1 / b ^ (1 / 2) * cexp (-(↑π : ℂ) / b * HPow.hPow (β := ℕ) ((↑t : ℂ) + I * c) 2)

Tactic:
ext1 t
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℂ
this : b ≠ 0
h : (-(↑π : ℂ) * b).re < 0
t : ℝ
h₁ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
      cexp
        ((↑(-2 * π * v * t) : ℂ) * I + -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑v : ℂ) 2 + 2 * (↑π : ℂ) * c * (↑v : ℂ))) =
    1 / b ^ (1 / 2) * cexp (-(↑π : ℂ) / b * HPow.hPow (β := ℕ) ((↑t : ℂ) + I * c) 2)
⊢ 𝓕 (E := (x : ℝ) → ℂ)
      (fun (x : ℝ) ↦ cexp (-(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 2 * (↑π : ℂ) * c * (↑x : ℂ))) t =
    1 / b ^ (1 / 2) * cexp (-(↑π : ℂ) / b * HPow.hPow (β := ℕ) ((↑t : ℂ) + I * c) 2)

Tactic:
simp_rw [fourier_real_eq_integral_exp_smul, smul_eq_mul, ← Complex.exp_add, ← add_assoc]

Premises used: Real.fourier_real_eq_integral_exp_smul, Complex.exp_add, add_assoc, smul_eq_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℂ
this : b ≠ 0
h : (-(↑π : ℂ) * b).re < 0
t x : ℝ
push_cast :
  -2 * (↑π : ℂ) * (↑x : ℂ) * (↑t : ℂ) * I + -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 +
      2 * (↑π : ℂ) * c * (↑x : ℂ) =
    -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (-2 * (↑π : ℂ) * I * (↑t : ℂ) + 2 * (↑π : ℂ) * c) * (↑x : ℂ) + 0
⊢ (↑(-2 * π * x * t) : ℂ) * I + -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 2 * (↑π : ℂ) * c * (↑x : ℂ) =
    -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (-2 * (↑π : ℂ) * I * (↑t : ℂ) + 2 * (↑π : ℂ) * c) * (↑x : ℂ) + 0

Tactic:
push_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℂ
this : b ≠ 0
h : (-(↑π : ℂ) * b).re < 0
t x : ℝ
⊢ -2 * (↑π : ℂ) * (↑x : ℂ) * (↑t : ℂ) * I + -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 +
      2 * (↑π : ℂ) * c * (↑x : ℂ) =
    -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (-2 * (↑π : ℂ) * I * (↑t : ℂ) + 2 * (↑π : ℂ) * c) * (↑x : ℂ) + 0

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℂ
this : b ≠ 0
h : (-(↑π : ℂ) * b).re < 0
t : ℝ
⊢ ∀ (x : ℝ),
    (↑(-2 * π * x * t) : ℂ) * I + -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 2 * (↑π : ℂ) * c * (↑x : ℂ) =
      -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (-2 * (↑π : ℂ) * I * (↑t : ℂ) + 2 * (↑π : ℂ) * c) * (↑x : ℂ) + 0

Tactic:
have (x : ℝ) : ↑(-2 * π * x * t) * I + -π * b * x ^ 2 + 2 * π * c * x =
    -π * b * x ^ 2 + (-2 * π * I * t + 2 * π * c) * x + 0 := by push_cast; ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℂ
this_1 : b ≠ 0
h : (-(↑π : ℂ) * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    (↑(-2 * π * x * t) : ℂ) * I + -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 2 * (↑π : ℂ) * c * (↑x : ℂ) =
      -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (-2 * (↑π : ℂ) * I * (↑t : ℂ) + 2 * (↑π : ℂ) * c) * (↑x : ℂ) + 0
h₁ :
  ((↑π : ℂ) / ((↑π : ℂ) * b)) ^ (1 / 2) *
      cexp (0 - HPow.hPow (β := ℕ) (-(2 * (↑π : ℂ) * I * (↑t : ℂ)) + 2 * (↑π : ℂ) * c) 2 / (4 * -((↑π : ℂ) * b))) =
    1 / b ^ (1 / 2) * cexp (-(↑π : ℂ) / b * HPow.hPow (β := ℕ) ((↑t : ℂ) + I * c) 2)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
      cexp
        ((↑(-2 * π * v * t) : ℂ) * I + -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑v : ℂ) 2 + 2 * (↑π : ℂ) * c * (↑v : ℂ))) =
    1 / b ^ (1 / 2) * cexp (-(↑π : ℂ) / b * HPow.hPow (β := ℕ) ((↑t : ℂ) + I * c) 2)

Tactic:
simp_rw [this, integral_cexp_quadratic h, neg_mul, neg_neg]

Premises used: neg_neg, integral_cexp_quadratic, neg_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℂ
this_1 : b ≠ 0
h : (-(↑π : ℂ) * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    (↑(-2 * π * x * t) : ℂ) * I + -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 2 * (↑π : ℂ) * c * (↑x : ℂ) =
      -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (-2 * (↑π : ℂ) * I * (↑t : ℂ) + 2 * (↑π : ℂ) * c) * (↑x : ℂ) + 0
h₁ : ((↑π : ℂ) / ((↑π : ℂ) * b)) ^ (1 / 2) = 1 / b ^ (1 / 2)
h₂ :
  0 - HPow.hPow (β := ℕ) (-(2 * (↑π : ℂ) * I * (↑t : ℂ)) + 2 * (↑π : ℂ) * c) 2 / (4 * -((↑π : ℂ) * b)) =
    -(↑π : ℂ) / b * HPow.hPow (β := ℕ) ((↑t : ℂ) + I * c) 2
⊢ ((↑π : ℂ) / ((↑π : ℂ) * b)) ^ (1 / 2) *
      cexp (0 - HPow.hPow (β := ℕ) (-(2 * (↑π : ℂ) * I * (↑t : ℂ)) + 2 * (↑π : ℂ) * c) 2 / (4 * -((↑π : ℂ) * b))) =
    1 / b ^ (1 / 2) * cexp (-(↑π : ℂ) / b * HPow.hPow (β := ℕ) ((↑t : ℂ) + I * c) 2)

Tactic:
congr 2
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℂ
this_1 : b ≠ 0
h : (-(↑π : ℂ) * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    (↑(-2 * π * x * t) : ℂ) * I + -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 2 * (↑π : ℂ) * c * (↑x : ℂ) =
      -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (-2 * (↑π : ℂ) * I * (↑t : ℂ) + 2 * (↑π : ℂ) * c) * (↑x : ℂ) + 0
h₁ : b.arg ≠ π
⊢ ((↑π : ℂ) / ((↑π : ℂ) * b)) ^ (1 / 2) = 1 / b ^ (1 / 2)

Tactic:
rw [← div_div, div_self <| ofReal_ne_zero.mpr pi_ne_zero, one_div, inv_cpow, ← one_div]

Premises used: Iff.mpr, Complex.ofReal_ne_zero, Complex.inv_cpow, one_div, div_div, div_self, Real.pi_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℂ
this_1 : b ≠ 0
h : (-(↑π : ℂ) * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    (↑(-2 * π * x * t) : ℂ) * I + -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 2 * (↑π : ℂ) * c * (↑x : ℂ) =
      -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (-2 * (↑π : ℂ) * I * (↑t : ℂ) + 2 * (↑π : ℂ) * c) * (↑x : ℂ) + 0
h₁ : 0 ≤ b.re ∨ ¬b.im = 0
⊢ b.arg ≠ π

Tactic:
rw [Ne, arg_eq_pi_iff, not_and_or, not_lt]

Premises used: Ne, not_lt, not_and_or, Complex.arg_eq_pi_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℂ
this_1 : b ≠ 0
h : (-(↑π : ℂ) * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    (↑(-2 * π * x * t) : ℂ) * I + -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 2 * (↑π : ℂ) * c * (↑x : ℂ) =
      -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (-2 * (↑π : ℂ) * I * (↑t : ℂ) + 2 * (↑π : ℂ) * c) * (↑x : ℂ) + 0
⊢ 0 ≤ b.re ∨ ¬b.im = 0

Tactic:
Or.inl hb.le

Premises used: LT.lt.le, Or.inl
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℂ
this_1 : b ≠ 0
h : (-(↑π : ℂ) * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    (↑(-2 * π * x * t) : ℂ) * I + -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 2 * (↑π : ℂ) * c * (↑x : ℂ) =
      -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (-2 * (↑π : ℂ) * I * (↑t : ℂ) + 2 * (↑π : ℂ) * c) * (↑x : ℂ) + 0
⊢ 0 ≤ b.re ∨ ¬b.im = 0

Tactic:
exact Or.inl hb.le

Premises used: LT.lt.le, Or.inl
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℂ
this_1 : b ≠ 0
h : (-(↑π : ℂ) * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    (↑(-2 * π * x * t) : ℂ) * I + -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 2 * (↑π : ℂ) * c * (↑x : ℂ) =
      -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (-2 * (↑π : ℂ) * I * (↑t : ℂ) + 2 * (↑π : ℂ) * c) * (↑x : ℂ) + 0
h₁ :
  HMul.hMul (α := ℂ) 0 4 * b -
      -(HPow.hPow (α := ℂ) (β := ℕ) 2 2 * (↑π : ℂ) * HPow.hPow (β := ℕ) (-(I * (↑t : ℂ)) + c) 2) =
    -((↑π : ℂ) * 4 * HPow.hPow (β := ℕ) ((↑t : ℂ) + I * c) 2)
⊢ 0 - HPow.hPow (β := ℕ) (-(2 * (↑π : ℂ) * I * (↑t : ℂ)) + 2 * (↑π : ℂ) * c) 2 / (4 * -((↑π : ℂ) * b)) =
    -(↑π : ℂ) / b * HPow.hPow (β := ℕ) ((↑t : ℂ) + I * c) 2

Tactic:
field_simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℂ
this_1 : b ≠ 0
h : (-(↑π : ℂ) * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    (↑(-2 * π * x * t) : ℂ) * I + -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 2 * (↑π : ℂ) * c * (↑x : ℂ) =
      -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (-2 * (↑π : ℂ) * I * (↑t : ℂ) + 2 * (↑π : ℂ) * c) * (↑x : ℂ) + 0
h₁ :
  -((↑π : ℂ) * I * (↑t : ℂ) * c * 8) + (↑π : ℂ) * HPow.hPow (β := ℕ) I 2 * HPow.hPow (β := ℕ) (↑t : ℂ) 2 * 4 +
      (↑π : ℂ) * HPow.hPow (β := ℕ) c 2 * 4 =
    -((↑π : ℂ) * I * (↑t : ℂ) * c * 8) - (↑π : ℂ) * HPow.hPow (β := ℕ) I 2 * HPow.hPow (β := ℕ) c 2 * 4 -
      (↑π : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 * 4
⊢ HMul.hMul (α := ℂ) 0 4 * b -
      -(HPow.hPow (α := ℂ) (β := ℕ) 2 2 * (↑π : ℂ) * HPow.hPow (β := ℕ) (-(I * (↑t : ℂ)) + c) 2) =
    -((↑π : ℂ) * 4 * HPow.hPow (β := ℕ) ((↑t : ℂ) + I * c) 2)

Tactic:
ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℂ
this_1 : b ≠ 0
h : (-(↑π : ℂ) * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    (↑(-2 * π * x * t) : ℂ) * I + -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 2 * (↑π : ℂ) * c * (↑x : ℂ) =
      -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (-2 * (↑π : ℂ) * I * (↑t : ℂ) + 2 * (↑π : ℂ) * c) * (↑x : ℂ) + 0
h₁ :
  -((↑π : ℂ) * I * (↑t : ℂ) * c * 8) + (↑π : ℂ) * -1 * HPow.hPow (β := ℕ) (↑t : ℂ) 2 * 4 +
      (↑π : ℂ) * HPow.hPow (β := ℕ) c 2 * 4 =
    -((↑π : ℂ) * I * (↑t : ℂ) * c * 8) - (↑π : ℂ) * -1 * HPow.hPow (β := ℕ) c 2 * 4 -
      (↑π : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 * 4
⊢ -((↑π : ℂ) * I * (↑t : ℂ) * c * 8) + (↑π : ℂ) * HPow.hPow (β := ℕ) I 2 * HPow.hPow (β := ℕ) (↑t : ℂ) 2 * 4 +
      (↑π : ℂ) * HPow.hPow (β := ℕ) c 2 * 4 =
    -((↑π : ℂ) * I * (↑t : ℂ) * c * 8) - (↑π : ℂ) * HPow.hPow (β := ℕ) I 2 * HPow.hPow (β := ℕ) c 2 * 4 -
      (↑π : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 * 4

Tactic:
simp only [I_sq]

Premises used: Complex.I_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℂ
this_1 : b ≠ 0
h : (-(↑π : ℂ) * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    (↑(-2 * π * x * t) : ℂ) * I + -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 2 * (↑π : ℂ) * c * (↑x : ℂ) =
      -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (-2 * (↑π : ℂ) * I * (↑t : ℂ) + 2 * (↑π : ℂ) * c) * (↑x : ℂ) + 0
⊢ -((↑π : ℂ) * I * (↑t : ℂ) * c * 8) + (↑π : ℂ) * -1 * HPow.hPow (β := ℕ) (↑t : ℂ) 2 * 4 +
      (↑π : ℂ) * HPow.hPow (β := ℕ) c 2 * 4 =
    -((↑π : ℂ) * I * (↑t : ℂ) * c * 8) - (↑π : ℂ) * -1 * HPow.hPow (β := ℕ) c 2 * 4 -
      (↑π : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 * 4

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
⊢ (𝓕 (E := (x : ℝ) → ℂ) fun (x : ℝ) ↦ cexp (-(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) = fun (t : ℝ) ↦
    1 / b ^ (1 / 2) * cexp (-(↑π : ℂ) / b * HPow.hPow (β := ℕ) (↑t : ℂ) 2)

Tactic:
simpa only [mul_zero, zero_mul, add_zero] using fourier_gaussian_pi' hb 0

Premises used: fourier_gaussian_pi', MulZeroClass.zero_mul, MulZeroClass.mul_zero, add_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
ι : Type u_2
inst : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
simp_rw :
  @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (v : ι → ℝ) ↦ ∏ x : ι, cexp (-b x * HPow.hPow (β := ℕ) (↑(v x) : ℂ) 2 + c x * (↑(v x) : ℂ))) volume
⊢ @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (v : ι → ℝ) ↦
      cexp (HAdd.hAdd (α := ℂ) (-∑ i : ι, b i * HPow.hPow (β := ℕ) (↑(v i) : ℂ) 2) (∑ i : ι, c i * (↑(v i) : ℂ))))
    volume

Tactic:
simp_rw [← Finset.sum_neg_distrib, ← Finset.sum_add_distrib, Complex.exp_sum, ← neg_mul]

Premises used: Finset.sum_add_distrib, neg_mul, Complex.exp_sum, Finset.sum_neg_distrib
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
ι : Type u_2
inst : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
apply :
  ∀ (i : ι),
    @Integrable ℂ _ _ ℝ MeasureSpace.toMeasurableSpace
      ((fun (i : ι) (v : ℝ) ↦ cexp (-b i * HPow.hPow (β := ℕ) (↑v : ℂ) 2 + c i * (↑v : ℂ))) i) volume
⊢ @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (v : ι → ℝ) ↦ ∏ x : ι, cexp (-b x * HPow.hPow (β := ℕ) (↑(v x) : ℂ) 2 + c x * (↑(v x) : ℂ))) volume

Tactic:
apply Integrable.fintype_prod (f := fun i (v : ℝ) ↦ cexp (-b i * v ^ 2 + c i * v)) (fun i ↦ ?_)

Premises used: MeasureTheory.Integrable.fintype_prod
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
ι : Type u_2
inst : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
i : ι
⊢ @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ cexp (-b i * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c i * (↑x : ℂ) + 0)) volume

Tactic:
integrable_cexp_quadratic (hb i) (c i) 0

Premises used: integrable_cexp_quadratic, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
ι : Type u_2
inst : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
i : ι
h :
  ∀ (x : ℝ),
    -b i * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c i * (↑x : ℂ) = -b i * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c i * (↑x : ℂ) + 0
⊢ @Integrable ℂ _ _ ℝ MeasureSpace.toMeasurableSpace
    ((fun (i : ι) (v : ℝ) ↦ cexp (-b i * HPow.hPow (β := ℕ) (↑v : ℂ) 2 + c i * (↑v : ℂ))) i) volume

Tactic:
convert! integrable_cexp_quadratic (hb i) (c i) 0 using 3 with x

Premises used: integrable_cexp_quadratic, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
ι : Type u_2
inst : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
i : ι
x : ℝ
⊢ -b i * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c i * (↑x : ℂ) = -b i * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c i * (↑x : ℂ) + 0

Tactic:
simp only [add_zero]

Premises used: add_zero