-- Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean
theorem integral_mul_cexp_neg_mul_sq {b : ℂ} (hb : 0 < b.re) :
    ∫ r : ℝ in Ioi 0, (r : ℂ) * cexp (-b * (r : ℂ) ^ 2) = (2 * b)⁻¹

Proof state:
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
x : ℂ
⊢ HasDerivAt (fun x => -(2 * b)⁻¹ * cexp (-b * x ^ 2)) (x * cexp (-b * x ^ 2)) x

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

Result:
case h.e'_9
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
x : ℂ
⊢ x * cexp (-b * x ^ 2) = -(2 * b)⁻¹ * (cexp (-b * x ^ 2) * (-b * (↑2 * x ^ (2 - 1))))

Proof state:
b : ℂ
hb : 0 < b.re
⊢ ∫ (r : ℝ) in Ioi 0, ↑r * cexp (-b * ↑r ^ 2) = (2 * b)⁻¹

Tactic:
have hb' : b ≠ 0 := by contrapose! hb; rw [hb, zero_re]

Result:
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
⊢ ∫ (r : ℝ) in Ioi 0, ↑r * cexp (-b * ↑r ^ 2) = (2 * b)⁻¹

Proof state:
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
A : ∀ (x : ℂ), HasDerivAt (fun x => -(2 * b)⁻¹ * cexp (-b * x ^ 2)) (x * cexp (-b * x ^ 2)) x
B : Tendsto (fun y => -(2 * b)⁻¹ * cexp (-b * ↑y ^ 2)) atTop (𝓝 (-(2 * b)⁻¹ * 0))
⊢ ∫ (r : ℝ) in Ioi 0, ↑r * cexp (-b * ↑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

Result:
case h.e'_3
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
A : ∀ (x : ℂ), HasDerivAt (fun x => -(2 * b)⁻¹ * cexp (-b * x ^ 2)) (x * cexp (-b * x ^ 2)) x
B : Tendsto (fun y => -(2 * b)⁻¹ * cexp (-b * ↑y ^ 2)) atTop (𝓝 (-(2 * b)⁻¹ * 0))
⊢ (2 * b)⁻¹ = -(2 * b)⁻¹ * 0 - -(2 * b)⁻¹ * cexp (-b * ↑0 ^ 2)

Proof state:
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
A : ∀ (x : ℂ), HasDerivAt (fun x => -(2 * b)⁻¹ * cexp (-b * x ^ 2)) (x * cexp (-b * x ^ 2)) x
⊢ Tendsto (fun x => ‖cexp (-b * ↑x ^ 2)‖) atTop (𝓝 0)

Tactic:
simp_rw [norm_cexp_neg_mul_sq b]

Result:
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
A : ∀ (x : ℂ), HasDerivAt (fun x => -(2 * b)⁻¹ * cexp (-b * x ^ 2)) (x * cexp (-b * x ^ 2)) x
⊢ Tendsto (fun x => rexp (-b.re * x ^ 2)) atTop (𝓝 0)

Proof state:
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
A : ∀ (x : ℂ), HasDerivAt (fun x => -(2 * b)⁻¹ * cexp (-b * x ^ 2)) (x * cexp (-b * x ^ 2)) x
⊢ Tendsto (fun x => rexp (-b.re * 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))

Result:
no goals

Proof state:
case h.e'_9
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
x : ℂ
⊢ x * cexp (-(b * x ^ 2)) * (2 * b) = cexp (-(b * x ^ 2)) * (b * (2 * x))

Tactic:
ring

Result:
no goals

Proof state:
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
⊢ ∫ (r : ℝ) in Ioi 0, ↑r * cexp (-b * ↑r ^ 2) = (2 * b)⁻¹

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_simp [hb']
  ring

Result:
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
A : ∀ (x : ℂ), HasDerivAt (fun x => -(2 * b)⁻¹ * cexp (-b * x ^ 2)) (x * cexp (-b * x ^ 2)) x
⊢ ∫ (r : ℝ) in Ioi 0, ↑r * cexp (-b * ↑r ^ 2) = (2 * b)⁻¹

Proof state:
case h.e'_9
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
x : ℂ
⊢ x * cexp (-b * x ^ 2) = -(2 * b)⁻¹ * (cexp (-b * x ^ 2) * (-b * (↑2 * x ^ (2 - 1))))

Tactic:
field_simp [hb']

Result:
case h.e'_9
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
x : ℂ
⊢ x * cexp (-(b * x ^ 2)) * (2 * b) = cexp (-(b * x ^ 2)) * (b * (2 * x))

Proof state:
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
A : ∀ (x : ℂ), HasDerivAt (fun x => -(2 * b)⁻¹ * cexp (-b * x ^ 2)) (x * cexp (-b * x ^ 2)) x
⊢ ∫ (r : ℝ) in Ioi 0, ↑r * cexp (-b * ↑r ^ 2) = (2 * b)⁻¹

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

Result:
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
A : ∀ (x : ℂ), HasDerivAt (fun x => -(2 * b)⁻¹ * cexp (-b * x ^ 2)) (x * cexp (-b * x ^ 2)) x
B : Tendsto (fun y => -(2 * b)⁻¹ * cexp (-b * ↑y ^ 2)) atTop (𝓝 (-(2 * b)⁻¹ * 0))
⊢ ∫ (r : ℝ) in Ioi 0, ↑r * cexp (-b * ↑r ^ 2) = (2 * b)⁻¹

Proof state:
case h.e'_3
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
A : ∀ (x : ℂ), HasDerivAt (fun x => -(2 * b)⁻¹ * cexp (-b * x ^ 2)) (x * cexp (-b * x ^ 2)) x
B : Tendsto (fun y => -(2 * b)⁻¹ * cexp (-b * ↑y ^ 2)) atTop (𝓝 (-(2 * b)⁻¹ * 0))
⊢ (2 * b)⁻¹ = -(2 * b)⁻¹ * 0 - -(2 * b)⁻¹ * cexp (-b * ↑0 ^ 2)

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

Result:
no goals

Proof state:
b : ℂ
hb : b = 0
⊢ b.re ≤ 0

Tactic:
rw [hb, zero_re]

Result:
no goals

Proof state:
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
⊢ ∀ (x : ℂ), HasDerivAt (fun x => -(2 * b)⁻¹ * cexp (-b * x ^ 2)) (x * cexp (-b * x ^ 2)) x

Tactic:
intro x

Result:
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
x : ℂ
⊢ HasDerivAt (fun x => -(2 * b)⁻¹ * cexp (-b * x ^ 2)) (x * cexp (-b * x ^ 2)) x

Proof state:
b : ℂ
hb : 0 < b.re
⊢ b ≠ 0

Tactic:
contrapose! hb

Result:
b : ℂ
hb : b = 0
⊢ b.re ≤ 0

Proof state:
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
A : ∀ (x : ℂ), HasDerivAt (fun x => -(2 * b)⁻¹ * cexp (-b * x ^ 2)) (x * cexp (-b * x ^ 2)) x
⊢ Tendsto (fun y => -(2 * b)⁻¹ * cexp (-b * ↑y ^ 2)) atTop (𝓝 (-(2 * b)⁻¹ * 0))

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

Result:
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
A : ∀ (x : ℂ), HasDerivAt (fun x => -(2 * b)⁻¹ * cexp (-b * x ^ 2)) (x * cexp (-b * x ^ 2)) x
⊢ Tendsto (fun x => ‖cexp (-b * ↑x ^ 2)‖) atTop (𝓝 0)