awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b c d : ℂ
hb : b = 0
⊢ 0 ≤ b.re
have rw : 0 ≤ re 0
Tactic: rw [hb, zero_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b c d : ℂ
hb : b = 0
rw : 0 ≤ re 0
⊢ 0 ≤ b.re
have rw₁ : LE.le (α := ℝ) 0 0
Tactic: rw [hb, zero_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (hypothesis)
Goal:
b : ℂ
hb : b.re < 0
c d : ℂ
⊢ (@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))
have hb' : b ≠ 0
Tactic: have hb' : b ≠ 0 := by contrapose! hb; rw [hb, zero_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
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))
have 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)))
Tactic: simp_rw [← Complex.exp_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
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 + (d - HPow.hPow (β := ℕ) c 2 / (4 * b)))
have 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))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (hypothesis)
Goal:
b : ℂ
hb : b.re < 0
c d : ℂ
hb' : b ≠ 0
⊢ (@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))
have 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))
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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
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))
⊢ (@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))
have 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))
Tactic: simp_rw [h, MeasureTheory.integral_mul_const]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
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))
⊢ (@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))
have 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))
Tactic: rw [← re_add_im (c / (2 * b))]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
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))
⊢ (@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))
have 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))
Tactic: simp_rw [← add_assoc, ← ofReal_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
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))
⊢ (@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))
have 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))
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))]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
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))
⊢ (@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))
have rw₁ : ((↑π : ℂ) / -b) ^ (1 / 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))]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (hypothesis)
Goal:
b : ℂ
hb : b.re < 0
c d : ℂ
⊢ @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ cexp (b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c * (↑x : ℂ) + d)) volume
have hb' : b ≠ 0
Tactic: have hb' : b ≠ 0 := by contrapose! hb; rw [hb, zero_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : b.re < 0
c d : ℂ
hb' : b ≠ 0
⊢ @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ cexp (b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c * (↑x : ℂ) + d)) volume
have by_contra : ∀
  (H :
    ¬@Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace
        (fun (x : ℝ) ↦ cexp (b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c * (↑x : ℂ) + d)) volume),
  False
Tactic: by_contra H
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (hypothesis)
Goal:
b : ℂ
hb : 0 < b.re
c d : ℂ
⊢ @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c * (↑x : ℂ) + d)) volume
have this : (-b).re < 0
Tactic: have : (-b).re < 0 := by simpa using hb
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
t : ℂ
| (@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))
have h : ∀ (x : ℝ), cexp (I * t * (↑x : ℂ)) * cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
Tactic: enter [1, 2, x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
t : ℂ
x : ℝ
| cexp (I * t * (↑x : ℂ)) * cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
have h : cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + I * t * (↑x : ℂ) + 0)
Tactic: rw [← Complex.exp_add, add_comm, ← add_zero (-b * x ^ 2 + I * t * x)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
t : ℂ
| (@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))
have h : ∀ (x : ℝ), cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + I * t * (↑x : ℂ) + 0)
Tactic: enter [1, 2, x]; rw [← Complex.exp_add, add_comm, ← add_zero (-b * x ^ 2 + I * t * x)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
t : ℂ
⊢ (@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))
have 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))
Tactic: conv => enter [1, 2, x]; rw [← Complex.exp_add, add_comm, ← add_zero (-b * x ^ 2 + I * t * x)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
t : ℂ
⊢ (-b).re < 0
have rwa : -b.re < 0
Tactic: rwa [neg_re, neg_lt_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
t : ℂ
⊢ (@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))
have rw : ((↑π : ℂ) / - -b) ^ (1 / 2) * cexp (0 - HPow.hPow (β := ℕ) (I * t) 2 / (4 * -b)) =
  ((↑π : ℂ) / 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
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))
⊢ (@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))
have rw₁ : ((↑π : ℂ) / b) ^ (1 / 2) * cexp (0 - HPow.hPow (β := ℕ) (I * t) 2 / (4 * -b)) =
  ((↑π : ℂ) / 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
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))
⊢ (@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))
have rw₂ : ((↑π : ℂ) / b) ^ (1 / 2) * cexp (-(HPow.hPow (β := ℕ) (I * t) 2 / (4 * -b))) =
  ((↑π : ℂ) / 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
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))
⊢ (@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))
have rw₃ : ((↑π : ℂ) / b) ^ (1 / 2) * cexp (-(HPow.hPow (β := ℕ) (I * t) 2 / -(4 * b))) =
  ((↑π : ℂ) / 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
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))
⊢ (@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))
have rw₄ : ((↑π : ℂ) / b) ^ (1 / 2) * cexp (- -(HPow.hPow (β := ℕ) (I * t) 2 / (4 * b))) =
  ((↑π : ℂ) / 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
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))
⊢ (@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))
have rw₅ : ((↑π : ℂ) / b) ^ (1 / 2) * cexp (HPow.hPow (β := ℕ) (I * t) 2 / (4 * b)) =
  ((↑π : ℂ) / 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
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))
⊢ (@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))
have 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))
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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
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))
⊢ (@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))
have rw₇ : ((↑π : ℂ) / b) ^ (1 / 2) * cexp (-1 * HPow.hPow (β := ℕ) t 2 / (4 * b)) =
  ((↑π : ℂ) / 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
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))
⊢ (@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))
have rw₈ : ((↑π : ℂ) / b) ^ (1 / 2) * cexp (-HPow.hPow (β := ℕ) t 2 / (4 * b)) =
  ((↑π : ℂ) / 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]