awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
refine :
  @HasFiniteIntegral _ ℂ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
    volume
⊢ @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) volume

Tactic:
refine ⟨by fun_prop, ?_⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
rw :
  @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (a : ℝ) ↦ ‖cexp (-b * HPow.hPow (β := ℕ) (↑a : ℂ) 2)‖)
    volume
⊢ @HasFiniteIntegral _ ℂ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
    volume

Tactic:
rw [← hasFiniteIntegral_norm_iff]

Premises used: MeasureTheory.hasFiniteIntegral_norm_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
simp_rw :
  @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (a : ℝ) ↦ rexp (-b.re * HPow.hPow (β := ℕ) a 2)) volume
⊢ @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (a : ℝ) ↦ ‖cexp (-b * HPow.hPow (β := ℕ) (↑a : ℂ) 2)‖)
    volume

Tactic:
simp_rw [norm_cexp_neg_mul_sq]

Premises used: norm_cexp_neg_mul_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
⊢ @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (a : ℝ) ↦ rexp (-b.re * HPow.hPow (β := ℕ) a 2)) volume

Tactic:
(integrable_exp_neg_mul_sq hb).2

Premises used: And.right, integrable_exp_neg_mul_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
⊢ @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (a : ℝ) ↦ rexp (-b.re * HPow.hPow (β := ℕ) a 2)) volume

Tactic:
exact (integrable_exp_neg_mul_sq hb).2

Premises used: And.right, integrable_exp_neg_mul_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
⊢ @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ (↑x : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) volume

Tactic:
⟨(continuous_ofReal.mul (Complex.continuous_exp.comp ?_)).aestronglyMeasurable, ?_⟩

Premises used: Continuous.comp, MeasureTheory.Integrable, Complex.continuous_exp, Continuous.mul, And.intro, Complex.continuous_ofReal, Continuous.aestronglyMeasurable
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
refine_1 : Continuous (Y := ℂ) fun (x : ℝ) ↦ -b * HPow.hPow (β := ℕ) (↑x : ℂ) 2
refine_2 :
  @HasFiniteIntegral _ ℂ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ (↑x : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) volume
⊢ @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ (↑x : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) volume

Tactic:
refine ⟨(continuous_ofReal.mul (Complex.continuous_exp.comp ?_)).aestronglyMeasurable, ?_⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
⊢ Continuous (Y := ℂ) fun (x : ℝ) ↦ -b * HPow.hPow (β := ℕ) (↑x : ℂ) 2

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
⊢ @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ x * rexp (-b.re * HPow.hPow (β := ℕ) x 2))
    volume

Tactic:
have := (integrable_mul_exp_neg_mul_sq hb).hasFiniteIntegral
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
this :
  @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ x * rexp (-b.re * HPow.hPow (β := ℕ) x 2))
    volume
refine_2 :
  ∀
    (this :
      @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace
        (fun (a : ℝ) ↦ ‖a * rexp (-b.re * HPow.hPow (β := ℕ) a 2)‖) volume),
    @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace
      (fun (a : ℝ) ↦ ‖(↑a : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑a : ℂ) 2)‖) volume
⊢ @HasFiniteIntegral _ ℂ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ (↑x : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) volume

Tactic:
rw [← hasFiniteIntegral_norm_iff] at this ⊢

Premises used: MeasureTheory.hasFiniteIntegral_norm_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
this :
  @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (a : ℝ) ↦ ‖a * rexp (-b.re * HPow.hPow (β := ℕ) a 2)‖)
    volume
⊢ @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (a : ℝ) ↦ ‖a * rexp (-b.re * HPow.hPow (β := ℕ) a 2)‖)
    volume

Tactic:
this
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
this :
  @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (a : ℝ) ↦ ‖a * rexp (-b.re * HPow.hPow (β := ℕ) a 2)‖)
    volume
h : ∀ (x : ℝ), ‖(↑x : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)‖ = ‖x * rexp (-b.re * HPow.hPow (β := ℕ) x 2)‖
⊢ @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace
    (fun (a : ℝ) ↦ ‖(↑a : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑a : ℂ) 2)‖) volume

Tactic:
convert! this
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
this :
  @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (a : ℝ) ↦ ‖a * rexp (-b.re * HPow.hPow (β := ℕ) a 2)‖)
    volume
x : ℝ
h : ‖(↑x : ℂ)‖ * ‖cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)‖ = ‖x * rexp (-b.re * HPow.hPow (β := ℕ) x 2)‖
h₁ : ‖(↑x : ℂ)‖ * ‖cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)‖ = ‖x‖ * ‖rexp (-b.re * HPow.hPow (β := ℕ) x 2)‖
h₂ : ‖(↑x : ℂ)‖ * rexp (-b.re * HPow.hPow (β := ℕ) x 2) = ‖x‖ * ‖rexp (-b.re * HPow.hPow (β := ℕ) x 2)‖
h₃ : ‖x‖ * rexp (-b.re * HPow.hPow (β := ℕ) x 2) = ‖x‖ * ‖rexp (-b.re * HPow.hPow (β := ℕ) x 2)‖
h₄ h₅ : ‖x‖ * rexp (-b.re * HPow.hPow (β := ℕ) x 2) = ‖x‖ * rexp (-b.re * HPow.hPow (β := ℕ) x 2)
⊢ ‖(↑x : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)‖ = ‖x * rexp (-b.re * HPow.hPow (β := ℕ) x 2)‖

Tactic:
rw [norm_mul, norm_mul, norm_cexp_neg_mul_sq b, norm_real, norm_of_nonneg (exp_pos _).le]

Premises used: norm_cexp_neg_mul_sq, LT.lt.le, norm_mul, Complex.norm_real, Real.norm_of_nonneg, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
contrapose! : ∀ (hb : b = 0), b.re ≤ 0
⊢ b ≠ 0

Tactic:
contrapose! hb
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
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.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
⊢ b ≠ 0

Tactic:
have hb' : b ≠ 0 := by contrapose! hb; rw [hb, zero_re]
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
x : ℂ
⊢ HasDerivAt (fun (y : ℂ) ↦ -(2 * b)⁻¹ * cexp (-b * HPow.hPow (β := ℕ) y 2))
    (-(2 * b)⁻¹ * (cexp (-b * HPow.hPow (β := ℕ) x 2) * (-b * ((↑2 : ℂ) * x ^ HSub.hSub (α := ℕ) 2 1)))) x

Tactic:
((hasDerivAt_pow 2 x).const_mul (-b)).cexp.const_mul (-(2 * b)⁻¹)

Premises used: HMul.hMul, Inv.inv, HasDerivAt.const_mul, HasDerivAt.cexp, hasDerivAt_pow, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
x : ℂ
h :
  x * cexp (-b * HPow.hPow (β := ℕ) x 2) =
    -(2 * b)⁻¹ * (cexp (-b * HPow.hPow (β := ℕ) x 2) * (-b * ((↑2 : ℂ) * x ^ HSub.hSub (α := ℕ) 2 1)))
⊢ HasDerivAt (fun (x : ℂ) ↦ -(2 * b)⁻¹ * cexp (-b * HPow.hPow (β := ℕ) x 2)) (x * cexp (-b * HPow.hPow (β := ℕ) x 2)) x

Tactic:
convert! ((hasDerivAt_pow 2 x).const_mul (-b)).cexp.const_mul (-(2 * b)⁻¹) using 1

Premises used: HMul.hMul, Inv.inv, HasDerivAt.const_mul, HasDerivAt.cexp, hasDerivAt_pow, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
x : ℂ
⊢ x * cexp (-b * HPow.hPow (β := ℕ) x 2) =
    -(2 * b)⁻¹ * (cexp (-b * HPow.hPow (β := ℕ) x 2) * (-b * ((↑2 : ℂ) * x ^ HSub.hSub (α := ℕ) 2 1)))

Tactic:
field
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
⊢ ∀ (x : ℂ),
    HasDerivAt (fun (x : ℂ) ↦ -(2 * b)⁻¹ * cexp (-b * HPow.hPow (β := ℕ) x 2)) (x * cexp (-b * HPow.hPow (β := ℕ) x 2))
      x

Tactic:
have A : ∀ x : ℂ, HasDerivAt (fun x => -(2 * b)⁻¹ * cexp (-b * x ^ 2))
    (x * cexp (-b * x ^ 2)) x := by
    intro x
    convert! ((hasDerivAt_pow 2 x).const_mul (-b)).cexp.const_mul (-(2 * b)⁻¹) using 1
    field
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
A :
  ∀ (x : ℂ),
    HasDerivAt (fun (x : ℂ) ↦ -(2 * b)⁻¹ * cexp (-b * HPow.hPow (β := ℕ) x 2)) (x * cexp (-b * HPow.hPow (β := ℕ) x 2))
      x
⊢ Tendsto (fun (y : ℝ) ↦ -(2 * b)⁻¹ * cexp (-b * HPow.hPow (β := ℕ) (↑y : ℂ) 2)) atTop (𝓝 (-(2 * b)⁻¹ * 0))

Tactic:
Tendsto.const_mul _ (tendsto_zero_iff_norm_tendsto_zero.mpr ?_)

Premises used: Iff.mpr, Filter.Tendsto.const_mul, tendsto_zero_iff_norm_tendsto_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
A :
  ∀ (x : ℂ),
    HasDerivAt (fun (x : ℂ) ↦ -(2 * b)⁻¹ * cexp (-b * HPow.hPow (β := ℕ) x 2)) (x * cexp (-b * HPow.hPow (β := ℕ) x 2))
      x
refine : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)‖) atTop (𝓝 0)
⊢ Tendsto (fun (y : ℝ) ↦ -(2 * b)⁻¹ * cexp (-b * HPow.hPow (β := ℕ) (↑y : ℂ) 2)) atTop (𝓝 (-(2 * b)⁻¹ * 0))

Tactic:
refine Tendsto.const_mul _ (tendsto_zero_iff_norm_tendsto_zero.mpr ?_)

Premises used: Iff.mpr, Filter.Tendsto.const_mul, tendsto_zero_iff_norm_tendsto_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
A :
  ∀ (x : ℂ),
    HasDerivAt (fun (x : ℂ) ↦ -(2 * b)⁻¹ * cexp (-b * HPow.hPow (β := ℕ) x 2)) (x * cexp (-b * HPow.hPow (β := ℕ) x 2))
      x
simp_rw : Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (-b.re * HPow.hPow (β := ℕ) x 2)) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)‖) atTop (𝓝 0)

Tactic:
simp_rw [norm_cexp_neg_mul_sq b]

Premises used: norm_cexp_neg_mul_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
A :
  ∀ (x : ℂ),
    HasDerivAt (fun (x : ℂ) ↦ -(2 * b)⁻¹ * cexp (-b * HPow.hPow (β := ℕ) x 2)) (x * cexp (-b * HPow.hPow (β := ℕ) x 2))
      x
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (-b.re * HPow.hPow (β := ℕ) x 2)) atTop (𝓝 0)

Tactic:
tendsto_exp_atBot.comp
      ((tendsto_pow_atTop two_ne_zero).const_mul_atTop_of_neg (neg_lt_zero.2 hb))

Premises used: Iff.mpr, neg_lt_zero, Real.exp, Real.tendsto_exp_atBot, two_ne_zero, Filter.Tendsto.const_mul_atTop_of_neg, Filter.Tendsto.comp, Filter.tendsto_pow_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
A :
  ∀ (x : ℂ),
    HasDerivAt (fun (x : ℂ) ↦ -(2 * b)⁻¹ * cexp (-b * HPow.hPow (β := ℕ) x 2)) (x * cexp (-b * HPow.hPow (β := ℕ) x 2))
      x
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (-b.re * HPow.hPow (β := ℕ) x 2)) atTop (𝓝 0)

Tactic:
exact tendsto_exp_atBot.comp
      ((tendsto_pow_atTop two_ne_zero).const_mul_atTop_of_neg (neg_lt_zero.2 hb))

Premises used: Iff.mpr, neg_lt_zero, Real.tendsto_exp_atBot, two_ne_zero, Filter.Tendsto.const_mul_atTop_of_neg, Filter.Tendsto.comp, Filter.tendsto_pow_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
A :
  ∀ (x : ℂ),
    HasDerivAt (fun (x : ℂ) ↦ -(2 * b)⁻¹ * cexp (-b * HPow.hPow (β := ℕ) x 2)) (x * cexp (-b * HPow.hPow (β := ℕ) x 2))
      x
⊢ Tendsto (fun (y : ℝ) ↦ -(2 * b)⁻¹ * cexp (-b * HPow.hPow (β := ℕ) (↑y : ℂ) 2)) atTop (𝓝 (-(2 * b)⁻¹ * 0))

Tactic:
have B : Tendsto (fun y : ℝ ↦ -(2 * b)⁻¹ * cexp (-b * (y : ℂ) ^ 2))
    atTop (𝓝 (-(2 * b)⁻¹ * 0)) := by
    refine Tendsto.const_mul _ (tendsto_zero_iff_norm_tendsto_zero.mpr ?_)
    simp_rw [norm_cexp_neg_mul_sq b]
    exact tendsto_exp_atBot.comp
      ((tendsto_pow_atTop two_ne_zero).const_mul_atTop_of_neg (neg_lt_zero.2 hb))
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
A :
  ∀ (x : ℂ),
    HasDerivAt (fun (x : ℂ) ↦ -(2 * b)⁻¹ * cexp (-b * HPow.hPow (β := ℕ) x 2)) (x * cexp (-b * HPow.hPow (β := ℕ) x 2))
      x
B : Tendsto (fun (y : ℝ) ↦ -(2 * b)⁻¹ * cexp (-b * HPow.hPow (β := ℕ) (↑y : ℂ) 2)) atTop (𝓝 (-(2 * b)⁻¹ * 0))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (↑x : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    -(2 * b)⁻¹ * 0 - -(2 * b)⁻¹ * cexp (-b * HPow.hPow (β := ℕ) (↑0 : ℂ) 2)

Tactic:
integral_Ioi_of_hasDerivAt_of_tendsto' (fun x _ => (A ↑x).comp_ofReal)
      (integrable_mul_cexp_neg_mul_sq hb).integrableOn B

Premises used: HasDerivAt.comp_ofReal, MeasureTheory.integral_Ioi_of_hasDerivAt_of_tendsto', Complex.ofReal, MeasureTheory.Integrable.integrableOn, integrable_mul_cexp_neg_mul_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
A :
  ∀ (x : ℂ),
    HasDerivAt (fun (x : ℂ) ↦ -(2 * b)⁻¹ * cexp (-b * HPow.hPow (β := ℕ) x 2)) (x * cexp (-b * HPow.hPow (β := ℕ) x 2))
      x
B : Tendsto (fun (y : ℝ) ↦ -(2 * b)⁻¹ * cexp (-b * HPow.hPow (β := ℕ) (↑y : ℂ) 2)) atTop (𝓝 (-(2 * b)⁻¹ * 0))
h : (2 * b)⁻¹ = -(2 * b)⁻¹ * 0 - -(2 * b)⁻¹ * cexp (-b * HPow.hPow (β := ℕ) (↑0 : ℂ) 2)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (r : ℝ) ↦
      (↑r : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑r : ℂ) 2)) =
    (2 * b)⁻¹

Tactic:
convert!
    integral_Ioi_of_hasDerivAt_of_tendsto' (fun x _ => (A ↑x).comp_ofReal)
      (integrable_mul_cexp_neg_mul_sq hb).integrableOn B using 1

Premises used: HasDerivAt.comp_ofReal, MeasureTheory.integral_Ioi_of_hasDerivAt_of_tendsto', Complex.ofReal, MeasureTheory.Integrable.integrableOn, integrable_mul_cexp_neg_mul_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
A :
  ∀ (x : ℂ),
    HasDerivAt (fun (x : ℂ) ↦ -(2 * b)⁻¹ * cexp (-b * HPow.hPow (β := ℕ) x 2)) (x * cexp (-b * HPow.hPow (β := ℕ) x 2))
      x
B : Tendsto (fun (y : ℝ) ↦ -(2 * b)⁻¹ * cexp (-b * HPow.hPow (β := ℕ) (↑y : ℂ) 2)) atTop (𝓝 (-(2 * b)⁻¹ * 0))
⊢ (2 * b)⁻¹ = -(2 * b)⁻¹ * 0 - -(2 * b)⁻¹ * cexp (-b * HPow.hPow (β := ℕ) (↑0 : ℂ) 2)

Tactic:
simp only [mul_zero, ofReal_zero, zero_pow, Ne,
    not_false_iff, Complex.exp_zero, mul_one, sub_neg_eq_add, zero_add, reduceCtorEq]

Premises used: reduceCtorEq, Complex.exp_zero, Ne, zero_add, MulZeroClass.mul_zero, Complex.ofReal_zero, mul_one, not_false_iff, zero_pow, sub_neg_eq_add
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
rw :
  Eq (α := ℂ)
    (@integral _ _ _ _ Prod.instMeasurableSpace (Measure.prod volume volume) fun (z : ℝ × ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑z.1 : ℂ) 2) * cexp (-b * HPow.hPow (β := ℕ) (↑z.2 : ℂ) 2))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (p : ℝ × ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2) * cexp (-b * HPow.hPow (β := ℕ) (↑p.2 : ℂ) 2))
⊢ HPow.hPow (α := ℂ) (β := ℕ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      2 =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (p : ℝ × ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2) * cexp (-b * HPow.hPow (β := ℕ) (↑p.2 : ℂ) 2)

Tactic:
rw [pow_two, ← integral_prod_mul]

Premises used: pow_two, MeasureTheory.integral_prod_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ Prod.instMeasurableSpace (Measure.prod volume volume) fun (z : ℝ × ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑z.1 : ℂ) 2) * cexp (-b * HPow.hPow (β := ℕ) (↑z.2 : ℂ) 2))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (p : ℝ × ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2) * cexp (-b * HPow.hPow (β := ℕ) (↑p.2 : ℂ) 2))

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
e_f :
  Eq (α := ℝ × ℝ → ℂ)
    (fun (p : ℝ × ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2) * cexp (-b * HPow.hPow (β := ℕ) (↑p.2 : ℂ) 2))
    fun (p : ℝ × ℝ) ↦ cexp (-b * (HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2 + HPow.hPow (β := ℕ) (↑p.2 : ℂ) 2))
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (p : ℝ × ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2) * cexp (-b * HPow.hPow (β := ℕ) (↑p.2 : ℂ) 2))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (p : ℝ × ℝ) ↦
      cexp (-b * (HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2 + HPow.hPow (β := ℕ) (↑p.2 : ℂ) 2)))

Tactic:
congr
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
e_f :
  ∀ (p : ℝ × ℝ),
    cexp (-b * HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2) * cexp (-b * HPow.hPow (β := ℕ) (↑p.2 : ℂ) 2) =
      cexp (-b * (HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2 + HPow.hPow (β := ℕ) (↑p.2 : ℂ) 2))
⊢ Eq (α := ℝ × ℝ → ℂ)
    (fun (p : ℝ × ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2) * cexp (-b * HPow.hPow (β := ℕ) (↑p.2 : ℂ) 2))
    fun (p : ℝ × ℝ) ↦ cexp (-b * (HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2 + HPow.hPow (β := ℕ) (↑p.2 : ℂ) 2))

Tactic:
ext1 p
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
p : ℝ × ℝ
e_f :
  cexp (-b * HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2 + -b * HPow.hPow (β := ℕ) (↑p.2 : ℂ) 2) =
    cexp (-b * (HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2 + HPow.hPow (β := ℕ) (↑p.2 : ℂ) 2))
e_f₁ e_f₂ :
  cexp (-b * HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2 + -b * HPow.hPow (β := ℕ) (↑p.2 : ℂ) 2) =
    cexp (-b * HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2 + -b * HPow.hPow (β := ℕ) (↑p.2 : ℂ) 2)
⊢ cexp (-b * HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2) * cexp (-b * HPow.hPow (β := ℕ) (↑p.2 : ℂ) 2) =
    cexp (-b * (HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2 + HPow.hPow (β := ℕ) (↑p.2 : ℂ) 2))

Tactic:
rw [← Complex.exp_add, mul_add]

Premises used: Complex.exp_add, mul_add
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
rw :
  Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume polarCoord.target) fun (p : ℝ × ℝ) ↦
      p.1 •
        cexp
          (-b *
            (HPow.hPow (β := ℕ) (↑((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p).1 : ℂ) 2 +
              HPow.hPow (β := ℕ) (↑((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p).2 : ℂ) 2)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume polarCoord.target) fun (p : ℝ × ℝ) ↦
      p.1 •
        cexp
          (-b *
            (HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.cos (↑p.2 : ℂ)) 2 +
              HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.sin (↑p.2 : ℂ)) 2)))
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (p : ℝ × ℝ) ↦
      cexp (-b * (HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2 + HPow.hPow (β := ℕ) (↑p.2 : ℂ) 2)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume polarCoord.target) fun (p : ℝ × ℝ) ↦
      p.1 •
        cexp
          (-b *
            (HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.cos (↑p.2 : ℂ)) 2 +
              HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.sin (↑p.2 : ℂ)) 2)))

Tactic:
rw [← integral_comp_polarCoord_symm]

Premises used: integral_comp_polarCoord_symm
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume polarCoord.target) fun (p : ℝ × ℝ) ↦
      p.1 •
        cexp
          (-b *
            (HPow.hPow (β := ℕ) (↑((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p).1 : ℂ) 2 +
              HPow.hPow (β := ℕ) (↑((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p).2 : ℂ) 2)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume polarCoord.target) fun (p : ℝ × ℝ) ↦
      p.1 •
        cexp
          (-b *
            (HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.cos (↑p.2 : ℂ)) 2 +
              HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.sin (↑p.2 : ℂ)) 2)))

Tactic:
simp only [polarCoord_symm_apply, ofReal_mul, ofReal_cos, ofReal_sin]

Premises used: polarCoord_symm_apply, Complex.ofReal_cos, Complex.ofReal_sin, Complex.ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
rw :
  Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume polarCoord.target) fun (p : ℝ × ℝ) ↦
      p.1 •
        cexp
          (-b *
            (HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.cos (↑p.2 : ℂ)) 2 +
              HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.sin (↑p.2 : ℂ)) 2)))
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.restrict (Measure.prod volume volume) (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (z : ℝ × ℝ) ↦
      (↑z.1 : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑z.1 : ℂ) 2) * 1)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume polarCoord.target) fun (p : ℝ × ℝ) ↦
      p.1 •
        cexp
          (-b *
            (HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.cos (↑p.2 : ℂ)) 2 +
              HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.sin (↑p.2 : ℂ)) 2))) =
    HMul.hMul (α := ℂ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (r : ℝ) ↦
        (↑r : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑r : ℂ) 2))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo (-π) π)) fun (θ : ℝ) ↦ 1)

Tactic:
rw [← setIntegral_prod_mul]

Premises used: MeasureTheory.setIntegral_prod_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
e_f :
  ∀ (p : ℝ × ℝ),
    p.1 •
        cexp
          (-b *
            (HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.cos (↑p.2 : ℂ)) 2 +
              HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.sin (↑p.2 : ℂ)) 2)) =
      (↑p.1 : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2) * 1
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume polarCoord.target) fun (p : ℝ × ℝ) ↦
      p.1 •
        cexp
          (-b *
            (HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.cos (↑p.2 : ℂ)) 2 +
              HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.sin (↑p.2 : ℂ)) 2)))
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.restrict (Measure.prod volume volume) (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (z : ℝ × ℝ) ↦
      (↑z.1 : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑z.1 : ℂ) 2) * 1)

Tactic:
congr with p : 1
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
p : ℝ × ℝ
e_f :
  p.1 •
      cexp
        (-b *
          (HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.cos (↑p.2 : ℂ)) 2 +
            HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.sin (↑p.2 : ℂ)) 2)) =
    (↑p.1 : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2)
⊢ p.1 •
      cexp
        (-b *
          (HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.cos (↑p.2 : ℂ)) 2 +
            HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.sin (↑p.2 : ℂ)) 2)) =
    (↑p.1 : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2) * 1

Tactic:
rw [mul_one]

Premises used: mul_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
p : ℝ × ℝ
e_f :
  HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.cos (↑p.2 : ℂ)) 2 +
      HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.sin (↑p.2 : ℂ)) 2 =
    HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2
⊢ p.1 •
      cexp
        (-b *
          (HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.cos (↑p.2 : ℂ)) 2 +
            HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.sin (↑p.2 : ℂ)) 2)) =
    (↑p.1 : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2)

Tactic:
congr
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
p : ℝ × ℝ
rw :
  (HPow.hPow (β := ℕ) (Complex.sin (↑p.2 : ℂ)) 2 + HPow.hPow (β := ℕ) (Complex.cos (↑p.2 : ℂ)) 2) *
    HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2
| HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2

Tactic:
rw [← one_mul ((p.1 : ℂ) ^ 2), ← sin_sq_add_cos_sq (p.2 : ℂ)]

Premises used: Complex.ofReal, Prod.fst, Complex.sin_sq_add_cos_sq, HPow.hPow, OfNat.ofNat, Prod.snd, one_mul